michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/init/logic): add new simp rules

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-22 17:04:25 -08:00
parent 56282a11f6
commit d240b06ba2
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/init/logic.lean
View file

@ -361,6 +361,11 @@ iff_false_intro (λ H,
have H' : ¬a, from (λ Ha, (iff.mp H Ha) Ha), have H' : ¬a, from (λ Ha, (iff.mp H Ha) Ha),
H' (iff.mpr H H')) H' (iff.mpr H H'))
theorem not_iff_self [simp] (a : Prop) : (¬a ↔ a) ↔ false :=
iff_false_intro (λ H,
have H' : ¬a, from (λ Ha, (iff.mpr H Ha) Ha),
H' (iff.mp H H'))
theorem true_iff_false [simp] : (true ↔ false) ↔ false := theorem true_iff_false [simp] : (true ↔ false) ↔ false :=
iff_false_intro (λ H, iff.mp H trivial) iff_false_intro (λ H, iff.mp H trivial)
@ -406,6 +411,12 @@ iff_false_intro and.right
theorem false_and [simp] (a : Prop) : false ∧ a ↔ false := theorem false_and [simp] (a : Prop) : false ∧ a ↔ false :=
iff_false_intro and.left iff_false_intro and.left
theorem not_and_self [simp] (a : Prop) : (¬a ∧ a) ↔ false :=
iff_false_intro (λ H, and.elim H (λ H₁ H₂, absurd H₂ H₁))
theorem and_not_self [simp] (a : Prop) : (a ∧ ¬a) ↔ false :=
iff_false_intro (λ H, and.elim H (λ H₁ H₂, absurd H₁ H₂))
theorem and_self [simp] (a : Prop) : a ∧ a ↔ a := theorem and_self [simp] (a : Prop) : a ∧ a ↔ a :=
iff.intro and.left (assume H, and.intro H H) iff.intro and.left (assume H, and.intro H H)