diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index dc0c3ff3a..f87ca61b1 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -183,7 +183,7 @@ induction_on l definition mem.is_decidable [instance] (H : decidable_eq T) (x : T) (l : list T) : decidable (x ∈ l) := rec_on l - (decidable.inr (iff.false_elim !mem.nil)) + (decidable.inr (not_of_iff_false !mem.nil)) (take (h : T) (l : list T) (iH : decidable (x ∈ l)), show decidable (x ∈ h::l), from decidable.rec_on iH diff --git a/library/init/logic.lean b/library/init/logic.lean index 25edd80a6..6a2a03326 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -53,15 +53,18 @@ namespace eq notation H1 ▸ H2 := subst H1 H2 end ops - variable {p : Prop} - open ops +end eq - theorem true_elim (H : p = true) : p := +section + variable {p : Prop} + open eq.ops + + theorem of_eq_true (H : p = true) : p := H⁻¹ ▸ trivial - theorem false_elim (H : p = false) : ¬p := + theorem not_of_eq_false (H : p = false) : ¬p := assume Hp, H ▸ Hp -end eq +end calc_subst eq.subst calc_refl eq.refl @@ -140,11 +143,11 @@ namespace heq theorem of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b := trans (of_eq H₁) H₂ - - theorem true_elim {a : Prop} (H : a == true) : a := - eq.true_elim (heq.to_eq H) end heq +theorem of_heq_true {a : Prop} (H : a == true) : a := +of_eq_true (heq.to_eq H) + calc_trans heq.trans calc_trans heq.of_heq_of_eq calc_trans heq.of_eq_of_heq @@ -158,16 +161,8 @@ notation a ∧ b := and a b variables {a b c d : Prop} -namespace and - theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c := - rec H₂ H₁ - - definition not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := - assume H : a ∧ b, absurd (elim_left H) Hna - - definition not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) := - assume H : a ∧ b, absurd (elim_right H) Hnb -end and +theorem and.elim (H₁ : a ∧ b) (H₂ : a → b → c) : c := +and.rec H₂ H₁ -- or -- -- @@ -183,11 +178,6 @@ namespace or theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c := rec H₂ H₃ H₁ - - definition not_intro (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := - assume H : a ∨ b, or.rec_on H - (assume Ha, absurd Ha Hna) - (assume Hb, absurd Hb Hnb) end or -- iff @@ -233,17 +223,17 @@ namespace iff (assume Hb, elim_right H Hb) (assume Ha, elim_left H Ha) - theorem true_elim (H : a ↔ true) : a := - mp (symm H) trivial - - theorem false_elim (H : a ↔ false) : ¬a := - assume Ha : a, mp H Ha - open eq.ops theorem of_eq {a b : Prop} (H : a = b) : a ↔ b := iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) end iff +theorem of_iff_true (H : a ↔ true) : a := +iff.mp (iff.symm H) trivial + +theorem not_of_iff_false (H : a ↔ false) : ¬a := +assume Ha : a, iff.mp H Ha + calc_refl iff.refl calc_trans iff.trans @@ -307,15 +297,15 @@ section rec_on Hp (assume Hp : p, rec_on Hq (assume Hq : q, inl (and.intro Hp Hq)) - (assume Hnq : ¬q, inr (and.not_right p Hnq))) - (assume Hnp : ¬p, inr (and.not_left q Hnp)) + (assume Hnq : ¬q, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hq Hnq)))) + (assume Hnp : ¬p, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hp Hnp))) definition or.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ∨ q) := rec_on Hp (assume Hp : p, inl (or.inl Hp)) (assume Hnp : ¬p, rec_on Hq (assume Hq : q, inl (or.inr Hq)) - (assume Hnq : ¬q, inr (or.not_intro Hnp Hnq))) + (assume Hnq : ¬q, inr (assume H : p ∨ q, or.elim H (assume Hp, absurd Hp Hnp) (assume Hq, absurd Hq Hnq)))) definition not.decidable [instance] (Hp : decidable p) : decidable (¬p) := rec_on Hp @@ -390,32 +380,6 @@ decidable.rec (λ Hnc : ¬c, eq.refl (@ite c (decidable.inr Hnc) A t t)) H -definition if_true {A : Type} (t e : A) : (if true then t else e) = t := -if_pos trivial - -definition if_false {A : Type} (t e : A) : (if false then t else e) = e := -if_neg not_false - -theorem if_cond_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A) - : (if c₁ then t else e) = (if c₂ then t else e) := -decidable.rec_on H₁ - (λ Hc₁ : c₁, decidable.rec_on H₂ - (λ Hc₂ : c₂, if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹) - (λ Hnc₂ : ¬c₂, absurd (iff.elim_left Heq Hc₁) Hnc₂)) - (λ Hnc₁ : ¬c₁, decidable.rec_on H₂ - (λ Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁) - (λ Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹)) - -theorem if_congr_aux {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] {A : Type} {t₁ t₂ e₁ e₂ : A} - (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : - (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) := -Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁) - -theorem if_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : - (if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) := -have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc), -if_congr_aux Hc Ht He - -- We use "dependent" if-then-else to be able to communicate the if-then-else condition -- to the branches definition dite (c : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A := diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index cbdc55a5e..6a729c661 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.lean @@ -23,8 +23,8 @@ cases P H1 H2 a -- this supercedes the em in decidable theorem em (a : Prop) : a ∨ ¬a := or.elim (prop_complete a) - (assume Ht : a = true, or.inl (eq.true_elim Ht)) - (assume Hf : a = false, or.inr (eq.false_elim Hf)) + (assume Ht : a = true, or.inl (of_eq_true Ht)) + (assume Hf : a = false, or.inr (not_of_eq_false Hf)) theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true := cases (λ x, x = false ∨ x = true) @@ -36,9 +36,9 @@ theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b := or.elim (prop_complete a) (assume Hat, or.elim (prop_complete b) (assume Hbt, Hat ⬝ Hbt⁻¹) - (assume Hbf, false_elim (Hbf ▸ (Hab (eq.true_elim Hat))))) + (assume Hbf, false_elim (Hbf ▸ (Hab (of_eq_true Hat))))) (assume Haf, or.elim (prop_complete b) - (assume Hbt, false_elim (Haf ▸ (Hba (eq.true_elim Hbt)))) + (assume Hbt, false_elim (Haf ▸ (Hba (of_eq_true Hbt)))) (assume Hbf, Haf ⬝ Hbf⁻¹)) theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b := diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 51ddd8976..c51cd6b0e 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -39,6 +39,12 @@ assume not_em : ¬(a ∨ ¬a), -- --- namespace and + definition not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := + assume H : a ∧ b, absurd (elim_left H) Hna + + definition not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) := + assume H : a ∧ b, absurd (elim_right H) Hnb + theorem swap (H : a ∧ b) : b ∧ a := intro (elim_right H) (elim_left H) @@ -68,6 +74,11 @@ end and -- -- namespace or + definition not_intro (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := + assume H : a ∨ b, or.rec_on H + (assume Ha, absurd Ha Hna) + (assume Hb, absurd Hb Hnb) + theorem imp_or (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d := elim H₁ (assume Ha : a, inl (H₂ Ha)) @@ -136,3 +147,37 @@ 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) + +-- if-then-else +-- ------------ +section + open eq.ops + + variables {A : Type} {c₁ c₂ : Prop} + + definition if_true (t e : A) : (if true then t else e) = t := + if_pos trivial + + definition if_false (t e : A) : (if false then t else e) = e := + if_neg not_false + + theorem if_cond_congr [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) (t e : A) + : (if c₁ then t else e) = (if c₂ then t else e) := + decidable.rec_on H₁ + (λ Hc₁ : c₁, decidable.rec_on H₂ + (λ Hc₂ : c₂, if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹) + (λ Hnc₂ : ¬c₂, absurd (iff.elim_left Heq Hc₁) Hnc₂)) + (λ Hnc₁ : ¬c₁, decidable.rec_on H₂ + (λ Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁) + (λ Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹)) + + theorem if_congr_aux [H₁ : decidable c₁] [H₂ : decidable c₂] {t₁ t₂ e₁ e₂ : A} + (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : + (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) := + Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁) + + theorem if_congr [H₁ : decidable c₁] {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : + (if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) := + have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc), + if_congr_aux Hc Ht He +end diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 7dfd7754c..530ce4687 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -143,7 +143,7 @@ theorem false_eq_true : (false ↔ true) ↔ false := not_false_iff_true ▸ (a_iff_not_a false) theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a := -iff.intro (assume H, iff.true_elim H) (assume H, iff_true_intro H) +iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H) theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a := -iff.intro (assume H, iff.false_elim H) (assume H, iff_false_intro H) +iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H) diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out index 72f2e1c2c..8d73bf38f 100644 --- a/tests/lean/interactive/findp.input.expected.out +++ b/tests/lean/interactive/findp.input.expected.out @@ -9,13 +9,12 @@ false.cases_on|Π (C : Type), false → C false.decidable|decidable false false.induction_on|∀ (C : Prop), false → C true_ne_false|¬ true = false -eq.false_elim|?p = false → ¬ ?p not_of_is_false|is_false ?c → ¬ ?c +not_of_iff_false|?a ↔ false → ¬ ?a p_ne_false|?p → ?p ≠ false is_false|Π (c : Prop) [H : decidable c], Prop +not_of_eq_false|?p = false → ¬ ?p decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2 not_false|¬ false of_not_is_false|¬ is_false ?c → ?c -if_false|∀ (t e : ?A), ite false t e = e -iff.false_elim|?a ↔ false → ¬ ?a -- ENDFINDP diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index 618b874c9..b2584fb7e 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -23,10 +23,10 @@ definition is_zero (x : nat) := nat.rec true (λ n r, false) x theorem is_zero_zero : is_zero zero -:= eq.true_elim (refl _) +:= of_eq_true (refl _) theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x) -:= eq.false_elim (refl _) +:= not_of_eq_false (refl _) theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n) := nat.rec diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean index 3b69f4f19..7926d24b6 100644 --- a/tests/lean/run/is_nil.lean +++ b/tests/lean/run/is_nil.lean @@ -11,7 +11,7 @@ definition is_nil {A : Type} (l : list A) : Prop := list.rec true (fun h t r, false) l theorem is_nil_nil (A : Type) : is_nil (@nil A) -:= eq.true_elim (refl true) +:= of_eq_true (refl true) theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil := not_intro (assume H : cons a l = nil,