feat(library/standard): add or_comm, and_comm, ... theorems, cleanup notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
66ba3c8a0b
commit
e817260c6d
4 changed files with 127 additions and 102 deletions
|
|
@ -16,7 +16,7 @@ theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a
|
|||
:= calc cast H a = cast (refl A) a : cast_proof_irrel H (refl A) a
|
||||
... = a : cast_refl a
|
||||
|
||||
definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b
|
||||
definition heq {A B : Type} (a : A) (b : B) := ∃H, cast H a = b
|
||||
|
||||
infixl `==`:50 := heq
|
||||
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ theorem case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
|
|||
(assume Ht : a = true, subst (symm Ht) H1)
|
||||
(assume Hf : a = false, subst (symm Hf) H2)
|
||||
|
||||
theorem em (a : Bool) : a ∨ ¬ a
|
||||
theorem em (a : Bool) : a ∨ ¬a
|
||||
:= or_elim (boolcomplete a)
|
||||
(assume Ht : a = true, or_intro_left (¬ a) (eqt_elim Ht))
|
||||
(assume Hf : a = false, or_intro_right a (eqf_elim Hf))
|
||||
|
|
@ -21,37 +21,37 @@ theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true
|
|||
(or_intro_left (false = true) (refl false))
|
||||
a
|
||||
|
||||
theorem not_true : (¬ true) = false
|
||||
:= have aux : ¬ (¬ true) = true, from
|
||||
not_intro (assume H : (¬ true) = true,
|
||||
theorem not_true : (¬true) = false
|
||||
:= have aux : ¬ (¬true) = true, from
|
||||
not_intro (assume H : (¬true) = true,
|
||||
absurd_not_true (subst (symm H) trivial)),
|
||||
resolve_right (boolcomplete (¬ true)) aux
|
||||
resolve_right (boolcomplete (¬true)) aux
|
||||
|
||||
theorem not_false : (¬ false) = true
|
||||
:= have aux : ¬ (¬ false) = false, from
|
||||
not_intro (assume H : (¬ false) = false,
|
||||
theorem not_false : (¬false) = true
|
||||
:= have aux : ¬ (¬false) = false, from
|
||||
not_intro (assume H : (¬false) = false,
|
||||
subst H not_false_trivial),
|
||||
resolve_right (boolcomplete_swapped (¬ false)) aux
|
||||
|
||||
theorem not_not_eq (a : Bool) : (¬ ¬ a) = a
|
||||
:= case (λ x, (¬ ¬ x) = x)
|
||||
(calc (¬ ¬ true) = (¬ false) : { not_true }
|
||||
... = true : not_false)
|
||||
(calc (¬ ¬ false) = (¬ true) : { not_false }
|
||||
... = false : not_true)
|
||||
theorem not_not_eq (a : Bool) : (¬¬a) = a
|
||||
:= case (λ x, (¬¬x) = x)
|
||||
(calc (¬¬true) = (¬false) : { not_true }
|
||||
... = true : not_false)
|
||||
(calc (¬¬false) = (¬true) : { not_false }
|
||||
... = false : not_true)
|
||||
a
|
||||
|
||||
theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
|
||||
theorem not_not_elim {a : Bool} (H : ¬¬a) : a
|
||||
:= (not_not_eq a) ◂ H
|
||||
|
||||
theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
|
||||
:= or_elim (boolcomplete a)
|
||||
(λ Hat : a = true, or_elim (boolcomplete b)
|
||||
(λ Hbt : b = true, trans Hat (symm Hbt))
|
||||
(λ Hbf : b = false, false_elim (a = b) (subst Hbf (Hab (eqt_elim Hat)))))
|
||||
(λ Haf : a = false, or_elim (boolcomplete b)
|
||||
(λ Hbt : b = true, false_elim (a = b) (subst Haf (Hba (eqt_elim Hbt))))
|
||||
(λ Hbf : b = false, trans Haf (symm Hbf)))
|
||||
(assume Hat, or_elim (boolcomplete b)
|
||||
(assume Hbt, trans Hat (symm Hbt))
|
||||
(assume Hbf, false_elim (a = b) (subst Hbf (Hab (eqt_elim Hat)))))
|
||||
(assume Haf, or_elim (boolcomplete b)
|
||||
(assume Hbt, false_elim (a = b) (subst Haf (Hba (eqt_elim Hbt))))
|
||||
(assume Hbf, trans Haf (symm Hbf)))
|
||||
|
||||
theorem iff_to_eq {a b : Bool} (H : a ↔ b) : a = b
|
||||
:= iff_elim (assume H1 H2, boolext H1 H2) H
|
||||
|
|
@ -65,12 +65,12 @@ theorem eqt_intro {a : Bool} (H : a) : a = true
|
|||
:= boolext (assume H1 : a, trivial)
|
||||
(assume H2 : true, H)
|
||||
|
||||
theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
|
||||
theorem eqf_intro {a : Bool} (H : ¬a) : a = false
|
||||
:= boolext (assume H1 : a, absurd H1 H)
|
||||
(assume H2 : false, false_elim a H2)
|
||||
|
||||
theorem by_contradiction {a : Bool} (H : ¬ a → false) : a
|
||||
:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
|
||||
theorem by_contradiction {a : Bool} (H : ¬a → false) : a
|
||||
:= or_elim (em a) (assume H1 : a, H1) (assume H1 : ¬a, false_elim a (H H1))
|
||||
|
||||
theorem a_neq_a {A : Type} (a : A) : (a ≠ a) = false
|
||||
:= boolext (assume H, a_neq_a_elim H)
|
||||
|
|
@ -108,20 +108,18 @@ theorem not_and (a b : Bool) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b)
|
|||
|
||||
theorem imp_or (a b : Bool) : (a → b) = (¬ a ∨ b)
|
||||
:= boolext
|
||||
(assume H : a → b,
|
||||
(or_elim (em a)
|
||||
(λ Ha : a, or_intro_right (¬ a) (H Ha))
|
||||
(λ Hna : ¬ a, or_intro_left b Hna)))
|
||||
(assume H : ¬ a ∨ b,
|
||||
assume Ha : a,
|
||||
resolve_right H ((symm (not_not_eq a)) ◂ Ha))
|
||||
(assume H : a → b, (or_elim (em a)
|
||||
(assume Ha : a, or_intro_right (¬ a) (H Ha))
|
||||
(assume Hna : ¬ a, or_intro_left b Hna)))
|
||||
(assume (H : ¬ a ∨ b) (Ha : a),
|
||||
resolve_right H ((symm (not_not_eq a)) ◂ Ha))
|
||||
|
||||
theorem not_implies (a b : Bool) : (¬ (a → b)) = (a ∧ ¬ b)
|
||||
:= calc (¬ (a → b)) = (¬ (¬ a ∨ b)) : {imp_or a b}
|
||||
... = (¬ ¬ a ∧ ¬ b) : not_or (¬ a) b
|
||||
... = (a ∧ ¬ b) : {not_not_eq a}
|
||||
theorem not_implies (a b : Bool) : (¬ (a → b)) = (a ∧ ¬b)
|
||||
:= calc (¬ (a → b)) = (¬(¬a ∨ b)) : {imp_or a b}
|
||||
... = (¬¬a ∧ ¬b) : not_or (¬ a) b
|
||||
... = (a ∧ ¬b) : {not_not_eq a}
|
||||
|
||||
theorem a_eq_not_a (a : Bool) : (a = ¬ a) = false
|
||||
theorem a_eq_not_a (a : Bool) : (a = ¬a) = false
|
||||
:= boolext
|
||||
(assume H, or_elim (em a)
|
||||
(assume Ha, absurd Ha (subst H Ha))
|
||||
|
|
@ -135,27 +133,23 @@ theorem false_eq_true : (false = true) = false
|
|||
:= subst not_false (a_eq_not_a false)
|
||||
|
||||
theorem a_eq_true (a : Bool) : (a = true) = a
|
||||
:= boolext
|
||||
(assume H, eqt_elim H)
|
||||
(assume H, eqt_intro H)
|
||||
:= boolext (assume H, eqt_elim H) (assume H, eqt_intro H)
|
||||
|
||||
theorem a_eq_false (a : Bool) : (a = false) = (¬ a)
|
||||
:= boolext
|
||||
(assume H, eqf_elim H)
|
||||
(assume H, eqf_intro H)
|
||||
theorem a_eq_false (a : Bool) : (a = false) = ¬a
|
||||
:= boolext (assume H, eqf_elim H) (assume H, eqf_intro H)
|
||||
|
||||
theorem not_exists_forall {A : Type} {P : A → Bool} (H : ¬ ∃ x, P x) : ∀ x, ¬ P x
|
||||
theorem not_exists_forall {A : Type} {P : A → Bool} (H : ¬∃x, P x) : ∀x, ¬P x
|
||||
:= take x, or_elim (em (P x))
|
||||
(assume Hp : P x, absurd_elim (¬ P x) (exists_intro x Hp) H)
|
||||
(assume Hn : ¬ P x, Hn)
|
||||
(assume Hp : P x, absurd_elim (¬P x) (exists_intro x Hp) H)
|
||||
(assume Hn : ¬P x, Hn)
|
||||
|
||||
theorem not_forall_exists {A : Type} {P : A → Bool} (H : ¬ ∀ x, P x) : ∃ x, ¬ P x
|
||||
:= by_contradiction (assume H1 : ¬ ∃ x, ¬ P x,
|
||||
have H2 : ∀ x, ¬ ¬ P x, from not_exists_forall H1,
|
||||
have H3 : ∀ x, P x, from take x, not_not_elim (H2 x),
|
||||
theorem not_forall_exists {A : Type} {P : A → Bool} (H : ¬∀x, P x) : ∃x, ¬P x
|
||||
:= by_contradiction (assume H1 : ¬∃ x, ¬P x,
|
||||
have H2 : ∀x, ¬¬P x, from not_exists_forall H1,
|
||||
have H3 : ∀x, P x, from take x, not_not_elim (H2 x),
|
||||
absurd H3 H)
|
||||
|
||||
theorem peirce (a b : Bool) : ((a → b) → a) → a
|
||||
:= assume H, by_contradiction (λ Hna : ¬ a,
|
||||
have Hnna : ¬ ¬ a, from not_implies_left (mt H Hna),
|
||||
:= assume H, by_contradiction (assume Hna : ¬a,
|
||||
have Hnna : ¬¬a, from not_implies_left (mt H Hna),
|
||||
absurd (not_not_elim Hnna) Hna)
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
-- Authors: Leonardo de Moura, Jeremy Avigad
|
||||
definition Bool [inline] := Type.{0}
|
||||
|
||||
inductive false : Bool :=
|
||||
|
|
@ -18,34 +18,34 @@ prefix `¬`:40 := not
|
|||
notation `assume` binders `,` r:(scoped f, f) := r
|
||||
notation `take` binders `,` r:(scoped f, f) := r
|
||||
|
||||
theorem not_intro {a : Bool} (H : a → false) : ¬ a
|
||||
theorem not_intro {a : Bool} (H : a → false) : ¬a
|
||||
:= H
|
||||
|
||||
theorem not_elim {a : Bool} (H1 : ¬ a) (H2 : a) : false
|
||||
theorem not_elim {a : Bool} (H1 : ¬a) (H2 : a) : false
|
||||
:= H1 H2
|
||||
|
||||
theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
|
||||
theorem absurd {a : Bool} (H1 : a) (H2 : ¬a) : false
|
||||
:= H2 H1
|
||||
|
||||
theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
|
||||
theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬b) : ¬a
|
||||
:= assume Ha : a, absurd (H1 Ha) H2
|
||||
|
||||
theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
|
||||
:= assume Hnb : ¬ b, mt H Hnb
|
||||
:= assume Hnb : ¬b, mt H Hnb
|
||||
|
||||
theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
|
||||
theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬a) : b
|
||||
:= false_elim b (absurd H1 H2)
|
||||
|
||||
theorem absurd_not_true (H : ¬ true) : false
|
||||
theorem absurd_not_true (H : ¬true) : false
|
||||
:= absurd trivial H
|
||||
|
||||
theorem not_false_trivial : ¬ false
|
||||
theorem not_false_trivial : ¬false
|
||||
:= assume H : false, H
|
||||
|
||||
theorem not_implies_left {a b : Bool} (H : ¬ (a → b)) : ¬ ¬ a
|
||||
:= assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna) H
|
||||
theorem not_implies_left {a b : Bool} (H : ¬(a → b)) : ¬¬a
|
||||
:= assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H
|
||||
|
||||
theorem not_implies_right {a b : Bool} (H : ¬ (a → b)) : ¬ b
|
||||
theorem not_implies_right {a b : Bool} (H : ¬(a → b)) : ¬b
|
||||
:= assume Hb : b, absurd (assume Ha : a, Hb) H
|
||||
|
||||
inductive and (a b : Bool) : Bool :=
|
||||
|
|
@ -58,10 +58,13 @@ theorem and_elim {a b c : Bool} (H1 : a → b → c) (H2 : a ∧ b) : c
|
|||
:= and_rec H1 H2
|
||||
|
||||
theorem and_elim_left {a b : Bool} (H : a ∧ b) : a
|
||||
:= and_rec (λ a b, a) H
|
||||
:= and_rec (λa b, a) H
|
||||
|
||||
theorem and_elim_right {a b : Bool} (H : a ∧ b) : b
|
||||
:= and_rec (λ a b, b) H
|
||||
:= and_rec (λa b, b) H
|
||||
|
||||
theorem and_swap {a b : Bool} (H : a ∧ b) : b ∧ a
|
||||
:= and_intro (and_elim_right H) (and_elim_left H)
|
||||
|
||||
inductive or (a b : Bool) : Bool :=
|
||||
| or_intro_left : a → or a b
|
||||
|
|
@ -73,13 +76,13 @@ infixr `∨`:30 := or
|
|||
theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
|
||||
:= or_rec H2 H3 H1
|
||||
|
||||
theorem resolve_right {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
|
||||
theorem resolve_right {a b : Bool} (H1 : a ∨ b) (H2 : ¬a) : b
|
||||
:= or_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb)
|
||||
|
||||
theorem resolve_left {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a
|
||||
theorem resolve_left {a b : Bool} (H1 : a ∨ b) (H2 : ¬b) : a
|
||||
:= or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
|
||||
|
||||
theorem or_flip {a b : Bool} (H : a ∨ b) : b ∨ a
|
||||
theorem or_swap {a b : Bool} (H : a ∨ b) : b ∨ a
|
||||
:= or_elim H (assume Ha, or_intro_right b Ha) (assume Hb, or_intro_left a Hb)
|
||||
|
||||
inductive eq {A : Type} (a : A) : A → Bool :=
|
||||
|
|
@ -97,7 +100,7 @@ calc_subst subst
|
|||
calc_refl refl
|
||||
calc_trans trans
|
||||
|
||||
theorem true_ne_false : ¬ true = false
|
||||
theorem true_ne_false : ¬true = false
|
||||
:= assume H : true = false,
|
||||
subst H trivial
|
||||
|
||||
|
|
@ -113,10 +116,10 @@ theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a =
|
|||
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
|
||||
:= subst H1 (subst H2 (refl (f a)))
|
||||
|
||||
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀ x, f x = g x
|
||||
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x
|
||||
:= take x, congr1 H x
|
||||
|
||||
theorem not_congr {a b : Bool} (H : a = b) : (¬ a) = (¬ b)
|
||||
theorem not_congr {a b : Bool} (H : a = b) : (¬a) = (¬b)
|
||||
:= congr2 not H
|
||||
|
||||
theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b
|
||||
|
|
@ -131,7 +134,7 @@ theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a
|
|||
theorem eqt_elim {a : Bool} (H : a = true) : a
|
||||
:= (symm H) ◂ trivial
|
||||
|
||||
theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
|
||||
theorem eqf_elim {a : Bool} (H : a = false) : ¬a
|
||||
:= not_intro (assume Ha : a, H ◂ Ha)
|
||||
|
||||
theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c
|
||||
|
|
@ -143,7 +146,7 @@ theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
|
|||
theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
|
||||
:= assume Ha, H2 (H1 ◂ Ha)
|
||||
|
||||
definition ne {A : Type} (a b : A) := ¬ (a = b)
|
||||
definition ne {A : Type} (a b : A) := ¬(a = b)
|
||||
infix `≠`:50 := ne
|
||||
|
||||
theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b
|
||||
|
|
@ -171,7 +174,7 @@ calc_trans eq_ne_trans
|
|||
calc_trans ne_eq_trans
|
||||
|
||||
definition iff (a b : Bool) := (a → b) ∧ (b → a)
|
||||
infix `↔`:50 := iff
|
||||
infix `↔`:25 := iff
|
||||
|
||||
theorem iff_intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a ↔ b
|
||||
:= and_intro H1 H2
|
||||
|
|
@ -194,34 +197,62 @@ theorem iff_mp_right {a b : Bool} (H1 : a ↔ b) (H2 : b) : a
|
|||
theorem eq_to_iff {a b : Bool} (H : a = b) : a ↔ b
|
||||
:= iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb)
|
||||
|
||||
theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a
|
||||
:= iff_intro (λH, and_swap H) (λH, and_swap H)
|
||||
|
||||
theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)
|
||||
:= iff_intro
|
||||
(assume H, and_intro
|
||||
(and_elim_left (and_elim_left H))
|
||||
(and_intro (and_elim_right (and_elim_left H)) (and_elim_right H)))
|
||||
(assume H, and_intro
|
||||
(and_intro (and_elim_left H) (and_elim_left (and_elim_right H)))
|
||||
(and_elim_right (and_elim_right H)))
|
||||
|
||||
theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a
|
||||
:= iff_intro (λH, or_swap H) (λH, or_swap H)
|
||||
|
||||
theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c)
|
||||
:= iff_intro
|
||||
(assume H, or_elim H
|
||||
(assume H1, or_elim H1
|
||||
(assume Ha, or_intro_left _ Ha)
|
||||
(assume Hb, or_intro_right a (or_intro_left c Hb)))
|
||||
(assume Hc, or_intro_right a (or_intro_right b Hc)))
|
||||
(assume H, or_elim H
|
||||
(assume Ha, (or_intro_left c (or_intro_left b Ha)))
|
||||
(assume H1, or_elim H1
|
||||
(assume Hb, or_intro_left c (or_intro_right a Hb))
|
||||
(assume Hc, or_intro_right _ Hc)))
|
||||
|
||||
inductive Exists {A : Type} (P : A → Bool) : Bool :=
|
||||
| exists_intro : ∀ (a : A), P a → Exists P
|
||||
|
||||
notation `∃` binders `,` r:(scoped P, Exists P) := r
|
||||
|
||||
theorem exists_elim {A : Type} {P : A → Bool} {B : Bool} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) : B
|
||||
theorem exists_elim {A : Type} {p : A → Bool} {B : Bool} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B
|
||||
:= Exists_rec H2 H1
|
||||
|
||||
theorem exists_not_forall {A : Type} {P : A → Bool} (H : ∃ x, P x) : ¬ ∀ x, ¬ P x
|
||||
:= assume H1 : ∀ x, ¬ P x,
|
||||
obtain (w : A) (Hw : P w), from H,
|
||||
theorem exists_not_forall {A : Type} {p : A → Bool} (H : ∃x, p x) : ¬∀x, ¬p x
|
||||
:= assume H1 : ∀x, ¬p x,
|
||||
obtain (w : A) (Hw : p w), from H,
|
||||
absurd Hw (H1 w)
|
||||
|
||||
theorem forall_not_exists {A : Type} {P : A → Bool} (H2 : ∀ x, P x) : ¬ ∃ x, ¬ P x
|
||||
:= assume H1 : ∃ x, ¬ P x,
|
||||
obtain (w : A) (Hw : ¬ P w), from H1,
|
||||
theorem forall_not_exists {A : Type} {p : A → Bool} (H2 : ∀x, p x) : ¬∃x, ¬p x
|
||||
:= assume H1 : ∃x, ¬p x,
|
||||
obtain (w : A) (Hw : ¬p w), from H1,
|
||||
absurd (H2 w) Hw
|
||||
|
||||
definition exists_unique {A : Type} (p : A → Bool) := ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y
|
||||
definition exists_unique {A : Type} (p : A → Bool) := ∃x, p x ∧ ∀y, y ≠ x → ¬ p y
|
||||
|
||||
notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
|
||||
|
||||
theorem exists_unique_intro {A : Type} {p : A → Bool} (w : A) (H1 : p w) (H2 : ∀ y, y ≠ w → ¬ p y) : ∃! x, p x
|
||||
theorem exists_unique_intro {A : Type} {p : A → Bool} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬ p y) : ∃!x, p x
|
||||
:= exists_intro w (and_intro H1 H2)
|
||||
|
||||
theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃! x, p x) (H1 : ∀ x, p x → (∀ y, y ≠ x → ¬ p y) → b) : b
|
||||
theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬ p y) → b) : b
|
||||
:= obtain w Hw, from H2,
|
||||
H1 w (and_elim_left Hw) (and_elim_right Hw)
|
||||
H1 w (and_elim_left Hw) (and_elim_right Hw)
|
||||
|
||||
inductive inhabited (A : Type) : Bool :=
|
||||
| inhabited_intro : A → inhabited A
|
||||
|
|
@ -233,7 +264,7 @@ theorem inhabited_Bool [instance] : inhabited Bool
|
|||
:= inhabited_intro true
|
||||
|
||||
theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
|
||||
:= inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
|
||||
:= inhabited_elim H (take b, inhabited_intro (λa, b))
|
||||
|
||||
theorem inhabited_exists {A : Type} {P : A → Bool} (H : ∃ x, P x) : inhabited A
|
||||
theorem inhabited_exists {A : Type} {p : A → Bool} (H : ∃x, p x) : inhabited A
|
||||
:= obtain w Hw, from H, inhabited_intro w
|
||||
|
|
|
|||
|
|
@ -7,24 +7,24 @@ import logic classical
|
|||
-- We are essentially saying that a relation R is well-founded
|
||||
-- if every non-empty "set" P, has a R-minimal element
|
||||
definition wf {A : Type} (R : A → A → Bool) : Bool
|
||||
:= ∀ P, (∃ w, P w) → ∃ min, P min ∧ ∀ b, R b min → ¬ P b
|
||||
:= ∀P, (∃w, P w) → ∃min, P min ∧ ∀b, R b min → ¬P b
|
||||
|
||||
-- Well-founded induction theorem
|
||||
theorem wf_induction {A : Type} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x)
|
||||
: ∀ x, P x
|
||||
:= by_contradiction (assume N : ¬ ∀ x, P x,
|
||||
obtain (w : A) (Hw : ¬ P w), from not_forall_exists N,
|
||||
theorem wf_induction {A : Type} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀x, (∀y, R y x → P y) → P x)
|
||||
: ∀x, P x
|
||||
:= by_contradiction (assume N : ¬∀x, P x,
|
||||
obtain (w : A) (Hw : ¬P w), from not_forall_exists N,
|
||||
-- The main "trick" is to define Q x as ¬ P x.
|
||||
-- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r)
|
||||
let Q [inline] := λ x, ¬ P x in
|
||||
have Qw : ∃ w, Q w, from exists_intro w Hw,
|
||||
have Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b, from Hwf Q Qw,
|
||||
obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b), from Qwf,
|
||||
let Q [inline] x := ¬P x in
|
||||
have Qw : ∃w, Q w, from exists_intro w Hw,
|
||||
have Qwf : ∃min, Q min ∧ ∀b, R b min → ¬Q b, from Hwf Q Qw,
|
||||
obtain (r : A) (Hr : Q r ∧ ∀b, R b r → ¬Q b), from Qwf,
|
||||
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
|
||||
have s1 : ∀ b, R b r → P b, from
|
||||
have s1 : ∀b, R b r → P b, from
|
||||
take b : A, assume H : R b r,
|
||||
-- We are using Hr to derive ¬ ¬ P b
|
||||
not_not_elim (and_elim_right Hr b H),
|
||||
have s2 : P r, from iH r s1,
|
||||
have s3 : ¬ P r, from and_elim_left Hr,
|
||||
show false, from absurd s2 s3)
|
||||
have s2 : P r, from iH r s1,
|
||||
have s3 : ¬P r, from and_elim_left Hr,
|
||||
absurd s2 s3)
|
||||
|
|
|
|||
Loading…
Reference in a new issue