From e76e445ecea4aef3f183a00adf219807d9fb9248 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 5 Apr 2015 12:15:21 -0400 Subject: [PATCH] feat(library/logic/connectives.lean): add calculation rules for true and false, and move exists unique to quantifiers --- library/logic/connectives.lean | 91 ++++++++++++++++++++++++++++------ library/logic/quantifiers.lean | 16 ++++++ 2 files changed, 93 insertions(+), 14 deletions(-) diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 2810ff2dfe..cfce06b3e1 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -10,6 +10,11 @@ The propositional connectives. See also init.datatypes and init.logic. variables {a b c d : Prop} +/- false -/ + +theorem false.elim {c : Prop} (H : false) : c := +false.rec c H + /- implies -/ definition imp (a b : Prop) : Prop := a → b @@ -17,10 +22,16 @@ definition imp (a b : Prop) : Prop := a → b theorem mt (H1 : a → b) (H2 : ¬b) : ¬a := assume Ha : a, absurd (H1 Ha) H2 -/- false -/ +theorem imp_true (a : Prop) : (a → true) ↔ true := +iff.intro (assume H, trivial) (assume H H1, trivial) -theorem false.elim {c : Prop} (H : false) : c := -false.rec c H +theorem true_imp (a : Prop) : (true → a) ↔ a := +iff.intro (assume H, H trivial) (assume H H1, H) + +theorem imp_false (a : Prop) : (a → false) ↔ ¬ a := iff.rfl + +theorem false_imp (a : Prop) : (false → a) ↔ true := +iff.intro (assume H, trivial) (assume H H1, false.elim H1) /- not -/ @@ -43,6 +54,12 @@ have Hnp : ¬a, from assume Hp : a, absurd (or.inl Hp) not_em, absurd (or.inr Hnp) not_em +theorem not_true : ¬ true ↔ false := +iff.intro (assume H, H trivial) (assume H, false.elim H) + +theorem not_false_iff : ¬ false ↔ true := +iff.intro (assume H, trivial) (assume H H1, H1) + /- and -/ definition not_and_of_not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := @@ -75,6 +92,21 @@ iff.intro (and.intro (and.elim_left H) (and.elim_left (and.elim_right H))) (and.elim_right (and.elim_right H))) +theorem and_true (a : Prop) : a ∧ true ↔ a := +iff.intro (assume H, and.left H) (assume H, and.intro H trivial) + +theorem true_and (a : Prop) : true ∧ a ↔ a := +iff.intro (assume H, and.right H) (assume H, and.intro trivial H) + +theorem and_false (a : Prop) : a ∧ false ↔ false := +iff.intro (assume H, and.right H) (assume H, false.elim H) + +theorem false_and (a : Prop) : false ∧ a ↔ false := +iff.intro (assume H, and.left H) (assume H, false.elim H) + +theorem and_self (a : Prop) : a ∧ a ↔ a := +iff.intro (assume H, and.left H) (assume H, and.intro H H) + /- or -/ definition not_or (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := @@ -125,26 +157,57 @@ iff.intro (assume Hb, or.inl (or.inr Hb)) (assume Hc, or.inr Hc))) +theorem or_true (a : Prop) : a ∨ true ↔ true := +iff.intro (assume H, trivial) (assume H, or.inr H) + +theorem true_or (a : Prop) : true ∨ a ↔ true := +iff.intro (assume H, trivial) (assume H, or.inl H) + +theorem or_false (a : Prop) : a ∨ false ↔ a := +iff.intro + (assume H, or.elim H (assume H1 : a, H1) (assume H1 : false, false.elim H1)) + (assume H, or.inl H) + +theorem false_or (a : Prop) : false ∨ a ↔ a := +iff.intro + (assume H, or.elim H (assume H1 : false, false.elim H1) (assume H1 : a, H1)) + (assume H, or.inr H) + +theorem or_self (a : Prop) : a ∨ a ↔ a := +iff.intro + (assume H, or.elim H (assume H1, H1) (assume H1, H1)) + (assume H, or.inl H) + /- iff -/ definition iff.def : (a ↔ b) = ((a → b) ∧ (b → a)) := !eq.refl -/- exists_unique -/ +theorem iff_true (a : Prop) : (a ↔ true) ↔ a := +iff.intro + (assume H, iff.mp' H trivial) + (assume H, iff.intro (assume H1, trivial) (assume H1, H)) -definition exists_unique {A : Type} (p : A → Prop) := -∃x, p x ∧ ∀y, p y → y = x +theorem true_iff (a : Prop) : (true ↔ a) ↔ a := +iff.intro + (assume H, iff.mp H trivial) + (assume H, iff.intro (assume H1, H) (assume H1, trivial)) -notation `∃!` binders `,` r:(scoped P, exists_unique P) := r +theorem iff_false (a : Prop) : (a ↔ false) ↔ ¬ a := +iff.intro + (assume H, and.left H) + (assume H, and.intro H (assume H1, false.elim H1)) -theorem exists_unique.intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : - ∃!x, p x := -exists.intro w (and.intro H1 H2) +theorem false_iff (a : Prop) : (false ↔ a) ↔ ¬ a := +iff.intro + (assume H, and.right H) + (assume H, and.intro (assume H1, false.elim H1) H) -theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop} - (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b := -obtain w Hw, from H2, -H1 w (and.elim_left Hw) (and.elim_right Hw) +theorem iff_true_of_self (Ha : a) : a ↔ true := +iff.intro (assume H, trivial) (assume H, Ha) + +theorem iff_self (a : Prop) : (a ↔ a) ↔ true := +iff_true_of_self !iff.refl /- if-then-else -/ diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index d05f5f2380..f9eeb3a19e 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -83,3 +83,19 @@ section obtain (w : A) (Hw : w = a ∧ P w), from h, absurd (and.rec_on Hw (λ h₁ h₂, h₁ ▸ h₂)) npa)) end + +/- exists_unique -/ + +definition exists_unique {A : Type} (p : A → Prop) := +∃x, p x ∧ ∀y, p y → y = x + +notation `∃!` binders `,` r:(scoped P, exists_unique P) := r + +theorem exists_unique.intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : + ∃!x, p x := +exists.intro w (and.intro H1 H2) + +theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop} + (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b := +obtain w Hw, from H2, +H1 w (and.elim_left Hw) (and.elim_right Hw)