From d240b06ba240d1dbe92ddbdda4e6e6624e8de08c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Nov 2015 17:04:25 -0800 Subject: [PATCH] feat(library/init/logic): add new simp rules --- library/init/logic.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/library/init/logic.lean b/library/init/logic.lean index ff2a93fae..a82c8ee29 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -361,6 +361,11 @@ iff_false_intro (λ H, have H' : ¬a, from (λ Ha, (iff.mp H Ha) Ha), 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 := 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 := 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 := iff.intro and.left (assume H, and.intro H H)