refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
df8b88dca2
commit
105c29b51e
30 changed files with 922 additions and 930 deletions
|
@ -148,8 +148,8 @@ example, =symm= is the symmetry theorem.
|
|||
import nat
|
||||
using nat
|
||||
|
||||
theorem nat_trans3 (a b c d : nat) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d
|
||||
:= trans (trans H1 (symm H2)) H3
|
||||
theorem nat_trans3 (a b c d : nat) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
trans (trans H1 (symm H2)) H3
|
||||
|
||||
-- Example using nat_trans3
|
||||
variables x y z w : nat
|
||||
|
@ -177,8 +177,8 @@ implicit arguments.
|
|||
import nat
|
||||
using nat
|
||||
|
||||
theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d
|
||||
:= trans (trans H1 (symm H2)) H3
|
||||
theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
trans (trans H1 (symm H2)) H3
|
||||
|
||||
-- Example using nat_trans3
|
||||
variables x y z w : nat
|
||||
|
@ -267,8 +267,7 @@ explicitly.
|
|||
#+BEGIN_SRC lean
|
||||
import logic
|
||||
|
||||
definition id.{l} {A : Type.{l}} (a : A) : A
|
||||
:= a
|
||||
definition id.{l} {A : Type.{l}} (a : A) : A := a
|
||||
|
||||
check id true
|
||||
#+END_SRC
|
||||
|
@ -423,8 +422,7 @@ are equal using just =refl=. Here is a simple example.
|
|||
import nat
|
||||
using nat
|
||||
|
||||
theorem def_eq_th (a : nat) : ((λ x : nat, x + 1) a) = a + 1
|
||||
:= refl (a+1)
|
||||
theorem def_eq_th (a : nat) : ((λ x : nat, x + 1) a) = a + 1 := refl (a+1)
|
||||
#+END_SRC
|
||||
|
||||
** Provable equality
|
||||
|
@ -698,8 +696,8 @@ for =∃ a : nat, a = w= using
|
|||
import nat
|
||||
using nat
|
||||
|
||||
theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d
|
||||
:= trans (trans H1 (symm H2)) H3
|
||||
theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
|
||||
trans (trans H1 (symm H2)) H3
|
||||
|
||||
variables x y z w : nat
|
||||
axiom Hxy : x = y
|
||||
|
@ -757,13 +755,13 @@ of two even numbers is an even number.
|
|||
using nat
|
||||
|
||||
definition even (a : nat) := ∃ b, a = 2*b
|
||||
theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b)
|
||||
:= exists_elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1),
|
||||
exists_elim H2 (fun (w2 : nat) (Hw2 : b = 2*w2),
|
||||
exists_intro (w1 + w2)
|
||||
(calc a + b = 2*w1 + b : {Hw1}
|
||||
... = 2*w1 + 2*w2 : {Hw2}
|
||||
... = 2*(w1 + w2) : symm (mul_add_distr_right 2 w1 w2))))
|
||||
theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
|
||||
exists_elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1),
|
||||
exists_elim H2 (fun (w2 : nat) (Hw2 : b = 2*w2),
|
||||
exists_intro (w1 + w2)
|
||||
(calc a + b = 2*w1 + b : {Hw1}
|
||||
... = 2*w1 + 2*w2 : {Hw2}
|
||||
... = 2*(w1 + w2) : symm (mul_add_distr_right 2 w1 w2))))
|
||||
|
||||
#+END_SRC
|
||||
|
||||
|
@ -777,12 +775,12 @@ With this macro we can write the example above in a more natural way
|
|||
import nat
|
||||
using nat
|
||||
definition even (a : nat) := ∃ b, a = 2*b
|
||||
theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b)
|
||||
:= obtain (w1 : nat) (Hw1 : a = 2*w1), from H1,
|
||||
obtain (w2 : nat) (Hw2 : b = 2*w2), from H2,
|
||||
exists_intro (w1 + w2)
|
||||
(calc a + b = 2*w1 + b : {Hw1}
|
||||
... = 2*w1 + 2*w2 : {Hw2}
|
||||
... = 2*(w1 + w2) : symm (mul_add_distr_right 2 w1 w2))
|
||||
theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
|
||||
obtain (w1 : nat) (Hw1 : a = 2*w1), from H1,
|
||||
obtain (w2 : nat) (Hw2 : b = 2*w2), from H2,
|
||||
exists_intro (w1 + w2)
|
||||
(calc a + b = 2*w1 + b : {Hw1}
|
||||
... = 2*w1 + 2*w2 : {Hw2}
|
||||
... = 2*(w1 + w2) : symm (mul_add_distr_right 2 w1 w2))
|
||||
#+END_SRC
|
||||
|
||||
|
|
|
@ -4,212 +4,212 @@
|
|||
import logic
|
||||
|
||||
-- 2. The Minimal Implicational Calculus
|
||||
theorem thm1 {A B : Prop} : A → B → A
|
||||
:= assume Ha Hb, Ha
|
||||
theorem thm1 {A B : Prop} : A → B → A :=
|
||||
assume Ha Hb, Ha
|
||||
|
||||
theorem thm2 {A B C : Prop} : (A → B) → (A → B → C) → (A → C)
|
||||
:= assume Hab Habc Ha,
|
||||
Habc Ha (Hab Ha)
|
||||
theorem thm2 {A B C : Prop} : (A → B) → (A → B → C) → (A → C) :=
|
||||
assume Hab Habc Ha,
|
||||
Habc Ha (Hab Ha)
|
||||
|
||||
theorem thm3 {A B C : Prop} : (A → B) → (B → C) → (A → C)
|
||||
:= assume Hab Hbc Ha,
|
||||
Hbc (Hab Ha)
|
||||
theorem thm3 {A B C : Prop} : (A → B) → (B → C) → (A → C) :=
|
||||
assume Hab Hbc Ha,
|
||||
Hbc (Hab Ha)
|
||||
|
||||
-- 3. False Propositions and Negation
|
||||
theorem thm4 {P Q : Prop} : ¬P → P → Q
|
||||
:= assume Hnp Hp,
|
||||
absurd_elim Q Hp Hnp
|
||||
theorem thm4 {P Q : Prop} : ¬P → P → Q :=
|
||||
assume Hnp Hp,
|
||||
absurd_elim Q Hp Hnp
|
||||
|
||||
theorem thm5 {P : Prop} : P → ¬¬P
|
||||
:= assume (Hp : P) (HnP : ¬P),
|
||||
absurd Hp HnP
|
||||
theorem thm5 {P : Prop} : P → ¬¬P :=
|
||||
assume (Hp : P) (HnP : ¬P),
|
||||
absurd Hp HnP
|
||||
|
||||
theorem thm6 {P Q : Prop} : (P → Q) → (¬Q → ¬P)
|
||||
:= assume (Hpq : P → Q) (Hnq : ¬Q) (Hp : P),
|
||||
have Hq : Q, from Hpq Hp,
|
||||
show false, from absurd Hq Hnq
|
||||
theorem thm6 {P Q : Prop} : (P → Q) → (¬Q → ¬P) :=
|
||||
assume (Hpq : P → Q) (Hnq : ¬Q) (Hp : P),
|
||||
have Hq : Q, from Hpq Hp,
|
||||
show false, from absurd Hq Hnq
|
||||
|
||||
theorem thm7 {P Q : Prop} : (P → ¬P) → (P → Q)
|
||||
:= assume Hpnp Hp,
|
||||
absurd_elim Q Hp (Hpnp Hp)
|
||||
theorem thm7 {P Q : Prop} : (P → ¬P) → (P → Q) :=
|
||||
assume Hpnp Hp,
|
||||
absurd_elim Q Hp (Hpnp Hp)
|
||||
|
||||
theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q)
|
||||
:= assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q),
|
||||
-- Rermak we don't even need the hypothesis Hp
|
||||
have H : P → Q, from assume H', Hq,
|
||||
absurd H Hn
|
||||
theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q) :=
|
||||
assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q),
|
||||
-- Rermak we don't even need the hypothesis Hp
|
||||
have H : P → Q, from assume H', Hq,
|
||||
absurd H Hn
|
||||
|
||||
-- 4. Conjunction and Disjunction
|
||||
theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P)
|
||||
:= assume (em : P ∨ ¬P) (Hnn : ¬¬P),
|
||||
or_elim em
|
||||
(assume Hp, Hp)
|
||||
(assume Hn, absurd_elim P Hn Hnn)
|
||||
theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P) :=
|
||||
assume (em : P ∨ ¬P) (Hnn : ¬¬P),
|
||||
or_elim em
|
||||
(assume Hp, Hp)
|
||||
(assume Hn, absurd_elim P Hn Hnn)
|
||||
|
||||
theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P)
|
||||
:= assume Hnem : ¬(P ∨ ¬P),
|
||||
have Hnp : ¬P, from
|
||||
assume Hp : P,
|
||||
have Hem : P ∨ ¬P, from or_inl Hp,
|
||||
absurd Hem Hnem,
|
||||
have Hem : P ∨ ¬P, from or_inr Hnp,
|
||||
absurd Hem Hnem
|
||||
theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P) :=
|
||||
assume Hnem : ¬(P ∨ ¬P),
|
||||
have Hnp : ¬P, from
|
||||
assume Hp : P,
|
||||
have Hem : P ∨ ¬P, from or_inl Hp,
|
||||
absurd Hem Hnem,
|
||||
have Hem : P ∨ ¬P, from or_inr Hnp,
|
||||
absurd Hem Hnem
|
||||
|
||||
theorem thm11 {P Q : Prop} : ¬P ∨ ¬Q → ¬(P ∧ Q)
|
||||
:= assume (H : ¬P ∨ ¬Q) (Hn : P ∧ Q),
|
||||
or_elim H
|
||||
(assume Hnp : ¬P, absurd (and_elim_left Hn) Hnp)
|
||||
(assume Hnq : ¬Q, absurd (and_elim_right Hn) Hnq)
|
||||
theorem thm11 {P Q : Prop} : ¬P ∨ ¬Q → ¬(P ∧ Q) :=
|
||||
assume (H : ¬P ∨ ¬Q) (Hn : P ∧ Q),
|
||||
or_elim H
|
||||
(assume Hnp : ¬P, absurd (and_elim_left Hn) Hnp)
|
||||
(assume Hnq : ¬Q, absurd (and_elim_right Hn) Hnq)
|
||||
|
||||
theorem thm12 {P Q : Prop} : ¬(P ∨ Q) → ¬P ∧ ¬Q
|
||||
:= assume H : ¬(P ∨ Q),
|
||||
have Hnp : ¬P, from assume Hp : P, absurd (or_inl Hp) H,
|
||||
have Hnq : ¬Q, from assume Hq : Q, absurd (or_inr Hq) H,
|
||||
and_intro Hnp Hnq
|
||||
theorem thm12 {P Q : Prop} : ¬(P ∨ Q) → ¬P ∧ ¬Q :=
|
||||
assume H : ¬(P ∨ Q),
|
||||
have Hnp : ¬P, from assume Hp : P, absurd (or_inl Hp) H,
|
||||
have Hnq : ¬Q, from assume Hq : Q, absurd (or_inr Hq) H,
|
||||
and_intro Hnp Hnq
|
||||
|
||||
theorem thm13 {P Q : Prop} : ¬P ∧ ¬Q → ¬(P ∨ Q)
|
||||
:= assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q),
|
||||
or_elim Hn
|
||||
(assume Hp : P, absurd Hp (and_elim_left H))
|
||||
(assume Hq : Q, absurd Hq (and_elim_right H))
|
||||
theorem thm13 {P Q : Prop} : ¬P ∧ ¬Q → ¬(P ∨ Q) :=
|
||||
assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q),
|
||||
or_elim Hn
|
||||
(assume Hp : P, absurd Hp (and_elim_left H))
|
||||
(assume Hq : Q, absurd Hq (and_elim_right H))
|
||||
|
||||
theorem thm14 {P Q : Prop} : ¬P ∨ Q → P → Q
|
||||
:= assume (Hor : ¬P ∨ Q) (Hp : P),
|
||||
or_elim Hor
|
||||
(assume Hnp : ¬P, absurd_elim Q Hp Hnp)
|
||||
(assume Hq : Q, Hq)
|
||||
theorem thm14 {P Q : Prop} : ¬P ∨ Q → P → Q :=
|
||||
assume (Hor : ¬P ∨ Q) (Hp : P),
|
||||
or_elim Hor
|
||||
(assume Hnp : ¬P, absurd_elim Q Hp Hnp)
|
||||
(assume Hq : Q, Hq)
|
||||
|
||||
theorem thm15 {P Q : Prop} : (P → Q) → ¬¬(¬P ∨ Q)
|
||||
:= assume (Hpq : P → Q) (Hn : ¬(¬P ∨ Q)),
|
||||
have H1 : ¬¬P ∧ ¬Q, from thm12 Hn,
|
||||
have Hnp : ¬P, from mt Hpq (and_elim_right H1),
|
||||
absurd Hnp (and_elim_left H1)
|
||||
theorem thm15 {P Q : Prop} : (P → Q) → ¬¬(¬P ∨ Q) :=
|
||||
assume (Hpq : P → Q) (Hn : ¬(¬P ∨ Q)),
|
||||
have H1 : ¬¬P ∧ ¬Q, from thm12 Hn,
|
||||
have Hnp : ¬P, from mt Hpq (and_elim_right H1),
|
||||
absurd Hnp (and_elim_left H1)
|
||||
|
||||
theorem thm16 {P Q : Prop} : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)) → ¬P ∨ Q
|
||||
:= assume H : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)),
|
||||
have Hpq : P → Q, from and_elim_left H,
|
||||
or_elim (and_elim_right H)
|
||||
(assume Hem1 : P ∨ ¬P, or_elim Hem1
|
||||
(assume Hp : P, or_inr (Hpq Hp))
|
||||
(assume Hnp : ¬P, or_inl Hnp))
|
||||
(assume Hem2 : Q ∨ ¬Q, or_elim Hem2
|
||||
(assume Hq : Q, or_inr Hq)
|
||||
(assume Hnq : ¬Q, or_inl (mt Hpq Hnq)))
|
||||
theorem thm16 {P Q : Prop} : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)) → ¬P ∨ Q :=
|
||||
assume H : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)),
|
||||
have Hpq : P → Q, from and_elim_left H,
|
||||
or_elim (and_elim_right H)
|
||||
(assume Hem1 : P ∨ ¬P, or_elim Hem1
|
||||
(assume Hp : P, or_inr (Hpq Hp))
|
||||
(assume Hnp : ¬P, or_inl Hnp))
|
||||
(assume Hem2 : Q ∨ ¬Q, or_elim Hem2
|
||||
(assume Hq : Q, or_inr Hq)
|
||||
(assume Hnq : ¬Q, or_inl (mt Hpq Hnq)))
|
||||
|
||||
-- 5. First-Order Logic: All and Exists
|
||||
section
|
||||
parameters {T : Type} {C : Prop} {P : T → Prop}
|
||||
theorem thm17a : (C → ∀x, P x) → (∀x, C → P x)
|
||||
:= assume H : C → ∀x, P x,
|
||||
take x : T, assume Hc : C,
|
||||
H Hc x
|
||||
theorem thm17a : (C → ∀x, P x) → (∀x, C → P x) :=
|
||||
assume H : C → ∀x, P x,
|
||||
take x : T, assume Hc : C,
|
||||
H Hc x
|
||||
|
||||
theorem thm17b : (∀x, C → P x) → (C → ∀x, P x)
|
||||
:= assume (H : ∀x, C → P x) (Hc : C),
|
||||
take x : T,
|
||||
H x Hc
|
||||
theorem thm17b : (∀x, C → P x) → (C → ∀x, P x) :=
|
||||
assume (H : ∀x, C → P x) (Hc : C),
|
||||
take x : T,
|
||||
H x Hc
|
||||
|
||||
theorem thm18a : ((∃x, P x) → C) → (∀x, P x → C)
|
||||
:= assume H : (∃x, P x) → C,
|
||||
take x, assume Hp : P x,
|
||||
have Hex : ∃x, P x, from exists_intro x Hp,
|
||||
H Hex
|
||||
theorem thm18a : ((∃x, P x) → C) → (∀x, P x → C) :=
|
||||
assume H : (∃x, P x) → C,
|
||||
take x, assume Hp : P x,
|
||||
have Hex : ∃x, P x, from exists_intro x Hp,
|
||||
H Hex
|
||||
|
||||
theorem thm18b : (∀x, P x → C) → (∃x, P x) → C
|
||||
:= assume (H1 : ∀x, P x → C) (H2 : ∃x, P x),
|
||||
obtain (w : T) (Hw : P w), from H2,
|
||||
H1 w Hw
|
||||
theorem thm18b : (∀x, P x → C) → (∃x, P x) → C :=
|
||||
assume (H1 : ∀x, P x → C) (H2 : ∃x, P x),
|
||||
obtain (w : T) (Hw : P w), from H2,
|
||||
H1 w Hw
|
||||
|
||||
theorem thm19a : (C ∨ ¬C) → (∃x : T, true) → (C → (∃x, P x)) → (∃x, C → P x)
|
||||
:= assume (Hem : C ∨ ¬C) (Hin : ∃x : T, true) (H1 : C → ∃x, P x),
|
||||
or_elim Hem
|
||||
(assume Hc : C,
|
||||
theorem thm19a : (C ∨ ¬C) → (∃x : T, true) → (C → (∃x, P x)) → (∃x, C → P x) :=
|
||||
assume (Hem : C ∨ ¬C) (Hin : ∃x : T, true) (H1 : C → ∃x, P x),
|
||||
or_elim Hem
|
||||
(assume Hc : C,
|
||||
obtain (w : T) (Hw : P w), from H1 Hc,
|
||||
have Hr : C → P w, from assume Hc, Hw,
|
||||
exists_intro w Hr)
|
||||
(assume Hnc : ¬C,
|
||||
(assume Hnc : ¬C,
|
||||
obtain (w : T) (Hw : true), from Hin,
|
||||
have Hr : C → P w, from assume Hc, absurd_elim (P w) Hc Hnc,
|
||||
exists_intro w Hr)
|
||||
|
||||
theorem thm19b : (∃x, C → P x) → C → (∃x, P x)
|
||||
:= assume (H : ∃x, C → P x) (Hc : C),
|
||||
obtain (w : T) (Hw : C → P w), from H,
|
||||
exists_intro w (Hw Hc)
|
||||
theorem thm19b : (∃x, C → P x) → C → (∃x, P x) :=
|
||||
assume (H : ∃x, C → P x) (Hc : C),
|
||||
obtain (w : T) (Hw : C → P w), from H,
|
||||
exists_intro w (Hw Hc)
|
||||
|
||||
theorem thm20a : (C ∨ ¬C) → (∃x : T, true) → ((¬∀x, P x) → ∃x, ¬P x) → ((∀x, P x) → C) → (∃x, P x → C)
|
||||
:= assume Hem Hin Hnf H,
|
||||
or_elim Hem
|
||||
(assume Hc : C,
|
||||
theorem thm20a : (C ∨ ¬C) → (∃x : T, true) → ((¬∀x, P x) → ∃x, ¬P x) → ((∀x, P x) → C) → (∃x, P x → C) :=
|
||||
assume Hem Hin Hnf H,
|
||||
or_elim Hem
|
||||
(assume Hc : C,
|
||||
obtain (w : T) (Hw : true), from Hin,
|
||||
exists_intro w (assume H : P w, Hc))
|
||||
(assume Hnc : ¬C,
|
||||
(assume Hnc : ¬C,
|
||||
have H1 : ¬(∀x, P x), from mt H Hnc,
|
||||
have H2 : ∃x, ¬P x, from Hnf H1,
|
||||
obtain (w : T) (Hw : ¬P w), from H2,
|
||||
exists_intro w (assume H : P w, absurd_elim C H Hw))
|
||||
|
||||
theorem thm20b : (∃x, P x → C) → (∀ x, P x) → C
|
||||
:= assume Hex Hall,
|
||||
obtain (w : T) (Hw : P w → C), from Hex,
|
||||
Hw (Hall w)
|
||||
theorem thm20b : (∃x, P x → C) → (∀ x, P x) → C :=
|
||||
assume Hex Hall,
|
||||
obtain (w : T) (Hw : P w → C), from Hex,
|
||||
Hw (Hall w)
|
||||
|
||||
theorem thm21a : (∃x : T, true) → ((∃x, P x) ∨ C) → (∃x, P x ∨ C)
|
||||
:= assume Hin H,
|
||||
or_elim H
|
||||
(assume Hex : ∃x, P x,
|
||||
obtain (w : T) (Hw : P w), from Hex,
|
||||
exists_intro w (or_inl Hw))
|
||||
(assume Hc : C,
|
||||
obtain (w : T) (Hw : true), from Hin,
|
||||
exists_intro w (or_inr Hc))
|
||||
theorem thm21a : (∃x : T, true) → ((∃x, P x) ∨ C) → (∃x, P x ∨ C) :=
|
||||
assume Hin H,
|
||||
or_elim H
|
||||
(assume Hex : ∃x, P x,
|
||||
obtain (w : T) (Hw : P w), from Hex,
|
||||
exists_intro w (or_inl Hw))
|
||||
(assume Hc : C,
|
||||
obtain (w : T) (Hw : true), from Hin,
|
||||
exists_intro w (or_inr Hc))
|
||||
|
||||
theorem thm21b : (∃x, P x ∨ C) → ((∃x, P x) ∨ C)
|
||||
:= assume H,
|
||||
obtain (w : T) (Hw : P w ∨ C), from H,
|
||||
or_elim Hw
|
||||
(assume H : P w, or_inl (exists_intro w H))
|
||||
(assume Hc : C, or_inr Hc)
|
||||
theorem thm21b : (∃x, P x ∨ C) → ((∃x, P x) ∨ C) :=
|
||||
assume H,
|
||||
obtain (w : T) (Hw : P w ∨ C), from H,
|
||||
or_elim Hw
|
||||
(assume H : P w, or_inl (exists_intro w H))
|
||||
(assume Hc : C, or_inr Hc)
|
||||
|
||||
theorem thm22a : (∀x, P x) ∨ C → ∀x, P x ∨ C
|
||||
:= assume H, take x,
|
||||
or_elim H
|
||||
(assume Hl, or_inl (Hl x))
|
||||
(assume Hr, or_inr Hr)
|
||||
theorem thm22a : (∀x, P x) ∨ C → ∀x, P x ∨ C :=
|
||||
assume H, take x,
|
||||
or_elim H
|
||||
(assume Hl, or_inl (Hl x))
|
||||
(assume Hr, or_inr Hr)
|
||||
|
||||
theorem thm22b : (C ∨ ¬C) → (∀x, P x ∨ C) → ((∀x, P x) ∨ C)
|
||||
:= assume Hem H1,
|
||||
or_elim Hem
|
||||
(assume Hc : C, or_inr Hc)
|
||||
(assume Hnc : ¬C,
|
||||
theorem thm22b : (C ∨ ¬C) → (∀x, P x ∨ C) → ((∀x, P x) ∨ C) :=
|
||||
assume Hem H1,
|
||||
or_elim Hem
|
||||
(assume Hc : C, or_inr Hc)
|
||||
(assume Hnc : ¬C,
|
||||
have Hx : ∀x, P x, from
|
||||
take x,
|
||||
have H1 : P x ∨ C, from H1 x,
|
||||
resolve_left H1 Hnc,
|
||||
or_inl Hx)
|
||||
|
||||
theorem thm23a : (∃x, P x) ∧ C → (∃x, P x ∧ C)
|
||||
:= assume H,
|
||||
have Hex : ∃x, P x, from and_elim_left H,
|
||||
have Hc : C, from and_elim_right H,
|
||||
obtain (w : T) (Hw : P w), from Hex,
|
||||
exists_intro w (and_intro Hw Hc)
|
||||
theorem thm23a : (∃x, P x) ∧ C → (∃x, P x ∧ C) :=
|
||||
assume H,
|
||||
have Hex : ∃x, P x, from and_elim_left H,
|
||||
have Hc : C, from and_elim_right H,
|
||||
obtain (w : T) (Hw : P w), from Hex,
|
||||
exists_intro w (and_intro Hw Hc)
|
||||
|
||||
theorem thm23b : (∃x, P x ∧ C) → (∃x, P x) ∧ C
|
||||
:= assume H,
|
||||
obtain (w : T) (Hw : P w ∧ C), from H,
|
||||
have Hex : ∃x, P x, from exists_intro w (and_elim_left Hw),
|
||||
and_intro Hex (and_elim_right Hw)
|
||||
theorem thm23b : (∃x, P x ∧ C) → (∃x, P x) ∧ C :=
|
||||
assume H,
|
||||
obtain (w : T) (Hw : P w ∧ C), from H,
|
||||
have Hex : ∃x, P x, from exists_intro w (and_elim_left Hw),
|
||||
and_intro Hex (and_elim_right Hw)
|
||||
|
||||
theorem thm24a : (∀x, P x) ∧ C → (∀x, P x ∧ C)
|
||||
:= assume H, take x,
|
||||
and_intro (and_elim_left H x) (and_elim_right H)
|
||||
theorem thm24a : (∀x, P x) ∧ C → (∀x, P x ∧ C) :=
|
||||
assume H, take x,
|
||||
and_intro (and_elim_left H x) (and_elim_right H)
|
||||
|
||||
theorem thm24b : (∃x : T, true) → (∀x, P x ∧ C) → (∀x, P x) ∧ C
|
||||
:= assume Hin H,
|
||||
obtain (w : T) (Hw : true), from Hin,
|
||||
have Hc : C, from and_elim_right (H w),
|
||||
have Hx : ∀x, P x, from take x, and_elim_left (H x),
|
||||
and_intro Hx Hc
|
||||
theorem thm24b : (∃x : T, true) → (∀x, P x ∧ C) → (∀x, P x) ∧ C :=
|
||||
assume Hin H,
|
||||
obtain (w : T) (Hw : true), from Hin,
|
||||
have Hc : C, from and_elim_right (H w),
|
||||
have Hx : ∀x, P x, from take x, and_elim_left (H x),
|
||||
and_intro Hx Hc
|
||||
|
||||
end -- of section
|
||||
|
|
|
@ -21,16 +21,16 @@ section
|
|||
hypothesis H_comm : commutative f
|
||||
hypothesis H_assoc : associative f
|
||||
|
||||
theorem left_comm : ∀a b c, a*(b*c) = b*(a*c)
|
||||
:= take a b c, calc
|
||||
a*(b*c) = (a*b)*c : (H_assoc _ _ _)⁻¹
|
||||
... = (b*a)*c : {H_comm _ _}
|
||||
... = b*(a*c) : H_assoc _ _ _
|
||||
theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
|
||||
take a b c, calc
|
||||
a*(b*c) = (a*b)*c : (H_assoc _ _ _)⁻¹
|
||||
... = (b*a)*c : {H_comm _ _}
|
||||
... = b*(a*c) : H_assoc _ _ _
|
||||
|
||||
theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b
|
||||
:= take a b c, calc
|
||||
(a*b)*c = a*(b*c) : H_assoc _ _ _
|
||||
... = a*(c*b) : {H_comm _ _}
|
||||
... = (a*c)*b : (H_assoc _ _ _)⁻¹
|
||||
theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
|
||||
take a b c, calc
|
||||
(a*b)*c = a*(b*c) : H_assoc _ _ _
|
||||
... = a*(c*b) : {H_comm _ _}
|
||||
... = (a*c)*b : (H_assoc _ _ _)⁻¹
|
||||
end
|
||||
end
|
||||
|
|
|
@ -6,138 +6,135 @@ using eq_proofs decidable
|
|||
|
||||
namespace bool
|
||||
inductive bool : Type :=
|
||||
| b0 : bool
|
||||
| b1 : bool
|
||||
notation `'0`:max := b0
|
||||
notation `'1`:max := b1
|
||||
| ff : bool
|
||||
| tt : bool
|
||||
|
||||
theorem induction_on {p : bool → Prop} (b : bool) (H0 : p '0) (H1 : p '1) : p b
|
||||
:= bool_rec H0 H1 b
|
||||
theorem induction_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
|
||||
bool_rec H0 H1 b
|
||||
|
||||
theorem inhabited_bool [instance] : inhabited bool
|
||||
:= inhabited_intro b0
|
||||
theorem inhabited_bool [instance] : inhabited bool :=
|
||||
inhabited_intro ff
|
||||
|
||||
definition cond {A : Type} (b : bool) (t e : A)
|
||||
:= bool_rec e t b
|
||||
definition cond {A : Type} (b : bool) (t e : A) :=
|
||||
bool_rec e t b
|
||||
|
||||
theorem dichotomy (b : bool) : b = '0 ∨ b = '1
|
||||
:= induction_on b (or_inl (refl '0)) (or_inr (refl '1))
|
||||
theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
|
||||
induction_on b (or_inl (refl ff)) (or_inr (refl tt))
|
||||
|
||||
theorem cond_b0 {A : Type} (t e : A) : cond '0 t e = e
|
||||
:= refl (cond '0 t e)
|
||||
theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
|
||||
refl (cond ff t e)
|
||||
|
||||
theorem cond_b1 {A : Type} (t e : A) : cond '1 t e = t
|
||||
:= refl (cond '1 t e)
|
||||
theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
|
||||
refl (cond tt t e)
|
||||
|
||||
theorem b0_ne_b1 : ¬ '0 = '1
|
||||
:= assume H : '0 = '1, absurd
|
||||
(calc true = cond '1 true false : (cond_b1 _ _)⁻¹
|
||||
... = cond '0 true false : {H⁻¹}
|
||||
... = false : cond_b0 _ _)
|
||||
true_ne_false
|
||||
theorem ff_ne_tt : ¬ ff = tt :=
|
||||
assume H : ff = tt, absurd
|
||||
(calc true = cond tt true false : (cond_tt _ _)⁻¹
|
||||
... = cond ff true false : {H⁻¹}
|
||||
... = false : cond_ff _ _)
|
||||
true_ne_false
|
||||
|
||||
theorem decidable_eq [instance] (a b : bool) : decidable (a = b)
|
||||
:= bool_rec
|
||||
(bool_rec (inl (refl '0)) (inr b0_ne_b1) b)
|
||||
(bool_rec (inr (ne_symm b0_ne_b1)) (inl (refl '1)) b)
|
||||
a
|
||||
theorem decidable_eq [instance] (a b : bool) : decidable (a = b) :=
|
||||
bool_rec
|
||||
(bool_rec (inl (refl ff)) (inr ff_ne_tt) b)
|
||||
(bool_rec (inr (ne_symm ff_ne_tt)) (inl (refl tt)) b)
|
||||
a
|
||||
|
||||
definition bor (a b : bool)
|
||||
:= bool_rec (bool_rec '0 '1 b) '1 a
|
||||
definition bor (a b : bool) :=
|
||||
bool_rec (bool_rec ff tt b) tt a
|
||||
|
||||
theorem bor_b1_left (a : bool) : bor '1 a = '1
|
||||
:= refl (bor '1 a)
|
||||
theorem bor_tt_left (a : bool) : bor tt a = tt :=
|
||||
refl (bor tt a)
|
||||
|
||||
infixl `||`:65 := bor
|
||||
|
||||
theorem bor_b1_right (a : bool) : a || '1 = '1
|
||||
:= induction_on a (refl ('0 || '1)) (refl ('1 || '1))
|
||||
theorem bor_tt_right (a : bool) : a || tt = tt :=
|
||||
induction_on a (refl (ff || tt)) (refl (tt || tt))
|
||||
|
||||
theorem bor_b0_left (a : bool) : '0 || a = a
|
||||
:= induction_on a (refl ('0 || '0)) (refl ('0 || '1))
|
||||
theorem bor_ff_left (a : bool) : ff || a = a :=
|
||||
induction_on a (refl (ff || ff)) (refl (ff || tt))
|
||||
|
||||
theorem bor_b0_right (a : bool) : a || '0 = a
|
||||
:= induction_on a (refl ('0 || '0)) (refl ('1 || '0))
|
||||
theorem bor_ff_right (a : bool) : a || ff = a :=
|
||||
induction_on a (refl (ff || ff)) (refl (tt || ff))
|
||||
|
||||
theorem bor_id (a : bool) : a || a = a
|
||||
:= induction_on a (refl ('0 || '0)) (refl ('1 || '1))
|
||||
theorem bor_id (a : bool) : a || a = a :=
|
||||
induction_on a (refl (ff || ff)) (refl (tt || tt))
|
||||
|
||||
theorem bor_comm (a b : bool) : a || b = b || a
|
||||
:= induction_on a
|
||||
(induction_on b (refl ('0 || '0)) (refl ('0 || '1)))
|
||||
(induction_on b (refl ('1 || '0)) (refl ('1 || '1)))
|
||||
theorem bor_comm (a b : bool) : a || b = b || a :=
|
||||
induction_on a
|
||||
(induction_on b (refl (ff || ff)) (refl (ff || tt)))
|
||||
(induction_on b (refl (tt || ff)) (refl (tt || tt)))
|
||||
|
||||
theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c)
|
||||
:= induction_on a
|
||||
(calc ('0 || b) || c = b || c : {bor_b0_left b}
|
||||
... = '0 || (b || c) : bor_b0_left (b || c)⁻¹)
|
||||
(calc ('1 || b) || c = '1 || c : {bor_b1_left b}
|
||||
... = '1 : bor_b1_left c
|
||||
... = '1 || (b || c) : bor_b1_left (b || c)⁻¹)
|
||||
theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
|
||||
induction_on a
|
||||
(calc (ff || b) || c = b || c : {bor_ff_left b}
|
||||
... = ff || (b || c) : bor_ff_left (b || c)⁻¹)
|
||||
(calc (tt || b) || c = tt || c : {bor_tt_left b}
|
||||
... = tt : bor_tt_left c
|
||||
... = tt || (b || c) : bor_tt_left (b || c)⁻¹)
|
||||
|
||||
theorem bor_to_or {a b : bool} : a || b = '1 → a = '1 ∨ b = '1
|
||||
:= bool_rec
|
||||
(assume H : '0 || b = '1,
|
||||
have Hb : b = '1, from (bor_b0_left b) ▸ H,
|
||||
or_inr Hb)
|
||||
(assume H, or_inl (refl '1))
|
||||
a
|
||||
theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
|
||||
bool_rec
|
||||
(assume H : ff || b = tt,
|
||||
have Hb : b = tt, from (bor_ff_left b) ▸ H,
|
||||
or_inr Hb)
|
||||
(assume H, or_inl (refl tt))
|
||||
a
|
||||
|
||||
definition band (a b : bool)
|
||||
:= bool_rec '0 (bool_rec '0 '1 b) a
|
||||
definition band (a b : bool) :=
|
||||
bool_rec ff (bool_rec ff tt b) a
|
||||
|
||||
infixl `&&`:75 := band
|
||||
|
||||
theorem band_b0_left (a : bool) : '0 && a = '0
|
||||
:= refl ('0 && a)
|
||||
theorem band_ff_left (a : bool) : ff && a = ff :=
|
||||
refl (ff && a)
|
||||
|
||||
theorem band_b1_left (a : bool) : '1 && a = a
|
||||
:= induction_on a (refl ('1 && '0)) (refl ('1 && '1))
|
||||
theorem band_tt_left (a : bool) : tt && a = a :=
|
||||
induction_on a (refl (tt && ff)) (refl (tt && tt))
|
||||
|
||||
theorem band_b0_right (a : bool) : a && '0 = '0
|
||||
:= induction_on a (refl ('0 && '0)) (refl ('1 && '0))
|
||||
theorem band_ff_right (a : bool) : a && ff = ff :=
|
||||
induction_on a (refl (ff && ff)) (refl (tt && ff))
|
||||
|
||||
theorem band_b1_right (a : bool) : a && '1 = a
|
||||
:= induction_on a (refl ('0 && '1)) (refl ('1 && '1))
|
||||
theorem band_tt_right (a : bool) : a && tt = a :=
|
||||
induction_on a (refl (ff && tt)) (refl (tt && tt))
|
||||
|
||||
theorem band_id (a : bool) : a && a = a
|
||||
:= induction_on a (refl ('0 && '0)) (refl ('1 && '1))
|
||||
theorem band_id (a : bool) : a && a = a :=
|
||||
induction_on a (refl (ff && ff)) (refl (tt && tt))
|
||||
|
||||
theorem band_comm (a b : bool) : a && b = b && a
|
||||
:= induction_on a
|
||||
(induction_on b (refl ('0 && '0)) (refl ('0 && '1)))
|
||||
(induction_on b (refl ('1 && '0)) (refl ('1 && '1)))
|
||||
theorem band_comm (a b : bool) : a && b = b && a :=
|
||||
induction_on a
|
||||
(induction_on b (refl (ff && ff)) (refl (ff && tt)))
|
||||
(induction_on b (refl (tt && ff)) (refl (tt && tt)))
|
||||
|
||||
theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c)
|
||||
:= induction_on a
|
||||
(calc ('0 && b) && c = '0 && c : {band_b0_left b}
|
||||
... = '0 : band_b0_left c
|
||||
... = '0 && (b && c) : band_b0_left (b && c)⁻¹)
|
||||
(calc ('1 && b) && c = b && c : {band_b1_left b}
|
||||
... = '1 && (b && c) : band_b1_left (b && c)⁻¹)
|
||||
theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
|
||||
induction_on a
|
||||
(calc (ff && b) && c = ff && c : {band_ff_left b}
|
||||
... = ff : band_ff_left c
|
||||
... = ff && (b && c) : band_ff_left (b && c)⁻¹)
|
||||
(calc (tt && b) && c = b && c : {band_tt_left b}
|
||||
... = tt && (b && c) : band_tt_left (b && c)⁻¹)
|
||||
|
||||
theorem band_eq_b1_elim_left {a b : bool} (H : a && b = '1) : a = '1
|
||||
:= or_elim (dichotomy a)
|
||||
(assume H0 : a = '0,
|
||||
absurd_elim (a = '1)
|
||||
(calc '0 = '0 && b : (band_b0_left _)⁻¹
|
||||
... = a && b : {H0⁻¹}
|
||||
... = '1 : H)
|
||||
b0_ne_b1)
|
||||
(assume H1 : a = '1, H1)
|
||||
theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
|
||||
or_elim (dichotomy a)
|
||||
(assume H0 : a = ff,
|
||||
absurd_elim (a = tt)
|
||||
(calc ff = ff && b : (band_ff_left _)⁻¹
|
||||
... = a && b : {H0⁻¹}
|
||||
... = tt : H)
|
||||
ff_ne_tt)
|
||||
(assume H1 : a = tt, H1)
|
||||
|
||||
theorem band_eq_b1_elim_right {a b : bool} (H : a && b = '1) : b = '1
|
||||
:= band_eq_b1_elim_left (trans (band_comm b a) H)
|
||||
theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
|
||||
band_eq_tt_elim_left (trans (band_comm b a) H)
|
||||
|
||||
definition bnot (a : bool) := bool_rec '1 '0 a
|
||||
definition bnot (a : bool) := bool_rec tt ff a
|
||||
|
||||
prefix `!`:85 := bnot
|
||||
|
||||
theorem bnot_bnot (a : bool) : !!a = a
|
||||
:= induction_on a (refl (!!'0)) (refl (!!'1))
|
||||
theorem bnot_bnot (a : bool) : !!a = a :=
|
||||
induction_on a (refl (!!ff)) (refl (!!tt))
|
||||
|
||||
theorem bnot_false : !'0 = '1
|
||||
:= refl _
|
||||
theorem bnot_false : !ff = tt := refl _
|
||||
|
||||
theorem bnot_true : !'1 = '0
|
||||
:= refl _
|
||||
theorem bnot_true : !tt = ff := refl _
|
||||
end
|
|
@ -4,111 +4,113 @@
|
|||
import logic
|
||||
using eq_proofs
|
||||
|
||||
definition cast {A B : Type} (H : A = B) (a : A) : B
|
||||
:= eq_rec a H
|
||||
definition cast {A B : Type} (H : A = B) (a : A) : B :=
|
||||
eq_rec a H
|
||||
|
||||
theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a
|
||||
:= refl (cast (refl A) a)
|
||||
theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a :=
|
||||
refl (cast (refl A) a)
|
||||
|
||||
theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a
|
||||
:= refl (cast H1 a)
|
||||
theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a :=
|
||||
refl (cast H1 a)
|
||||
|
||||
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
|
||||
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
|
||||
|
||||
theorem heq_elim {A B : Type} {C : Prop} {a : A} {b : B} (H1 : a == b) (H2 : ∀ (Hab : A = B), cast Hab a = b → C) : C
|
||||
:= obtain w Hw, from H1, H2 w Hw
|
||||
theorem heq_elim {A B : Type} {C : Prop} {a : A} {b : B} (H1 : a == b) (H2 : ∀ (Hab : A = B), cast Hab a = b → C) : C :=
|
||||
obtain w Hw, from H1, H2 w Hw
|
||||
|
||||
theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
|
||||
:= obtain w Hw, from H, w
|
||||
theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B :=
|
||||
obtain w Hw, from H, w
|
||||
|
||||
theorem eq_to_heq {A : Type} {a b : A} (H : a = b) : a == b
|
||||
:= exists_intro (refl A) (cast_refl a ⬝ H)
|
||||
theorem eq_to_heq {A : Type} {a b : A} (H : a = b) : a == b :=
|
||||
exists_intro (refl A) (cast_refl a ⬝ H)
|
||||
|
||||
theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b
|
||||
:= obtain (w : A = A) (Hw : cast w a = b), from H,
|
||||
calc a = cast w a : (cast_eq w a)⁻¹
|
||||
... = b : Hw
|
||||
theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b :=
|
||||
obtain (w : A = A) (Hw : cast w a = b), from H,
|
||||
calc a = cast w a : (cast_eq w a)⁻¹
|
||||
... = b : Hw
|
||||
|
||||
theorem hrefl {A : Type} (a : A) : a == a
|
||||
:= eq_to_heq (refl a)
|
||||
theorem hrefl {A : Type} (a : A) : a == a :=
|
||||
eq_to_heq (refl a)
|
||||
|
||||
theorem heqt_elim {a : Prop} (H : a == true) : a
|
||||
:= eqt_elim (heq_to_eq H)
|
||||
theorem heqt_elim {a : Prop} (H : a == true) : a :=
|
||||
eqt_elim (heq_to_eq H)
|
||||
|
||||
opaque_hint (hiding cast)
|
||||
|
||||
theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Prop} (H1 : a == b) (H2 : P A a) : P B b
|
||||
:= have Haux1 : ∀ H : A = A, P A (cast H a), from
|
||||
assume H : A = A, (cast_eq H a)⁻¹ ▸ H2,
|
||||
obtain (Heq : A = B) (Hw : cast Heq a = b), from H1,
|
||||
have Haux2 : P B (cast Heq a), from subst Heq Haux1 Heq,
|
||||
Hw ▸ Haux2
|
||||
theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Prop} (H1 : a == b) (H2 : P A a) : P B b :=
|
||||
have Haux1 : ∀ H : A = A, P A (cast H a), from
|
||||
assume H : A = A, (cast_eq H a)⁻¹ ▸ H2,
|
||||
obtain (Heq : A = B) (Hw : cast Heq a = b), from H1,
|
||||
have Haux2 : P B (cast Heq a), from subst Heq Haux1 Heq,
|
||||
Hw ▸ Haux2
|
||||
|
||||
theorem hsymm {A B : Type} {a : A} {b : B} (H : a == b) : b == a
|
||||
:= hsubst H (hrefl a)
|
||||
theorem hsymm {A B : Type} {a : A} {b : B} (H : a == b) : b == a :=
|
||||
hsubst H (hrefl a)
|
||||
|
||||
theorem htrans {A B C : Type} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
|
||||
:= hsubst H2 H1
|
||||
theorem htrans {A B C : Type} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c :=
|
||||
hsubst H2 H1
|
||||
|
||||
theorem htrans_left {A B : Type} {a : A} {b c : B} (H1 : a == b) (H2 : b = c) : a == c
|
||||
:= htrans H1 (eq_to_heq H2)
|
||||
theorem htrans_left {A B : Type} {a : A} {b c : B} (H1 : a == b) (H2 : b = c) : a == c :=
|
||||
htrans H1 (eq_to_heq H2)
|
||||
|
||||
theorem htrans_right {A C : Type} {a b : A} {c : C} (H1 : a = b) (H2 : b == c) : a == c
|
||||
:= htrans (eq_to_heq H1) H2
|
||||
theorem htrans_right {A C : Type} {a b : A} {c : C} (H1 : a = b) (H2 : b == c) : a == c :=
|
||||
htrans (eq_to_heq H1) H2
|
||||
|
||||
calc_trans htrans
|
||||
calc_trans htrans_left
|
||||
calc_trans htrans_right
|
||||
|
||||
theorem type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
|
||||
:= hsubst H (refl A)
|
||||
theorem type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B :=
|
||||
hsubst H (refl A)
|
||||
|
||||
theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a
|
||||
:= have H1 : ∀ (H : A = A) (a : A), cast H a == a, from
|
||||
λ H a, eq_to_heq (cast_eq H a),
|
||||
subst H H1 H a
|
||||
theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a :=
|
||||
have H1 : ∀ (H : A = A) (a : A), cast H a == a, from
|
||||
assume H a, eq_to_heq (cast_eq H a),
|
||||
subst H H1 H a
|
||||
|
||||
theorem cast_eq_to_heq {A B : Type} {a : A} {b : B} {H : A = B} (H1 : cast H a = b) : a == b
|
||||
:= calc a == cast H a : hsymm (cast_heq H a)
|
||||
... = b : H1
|
||||
theorem cast_eq_to_heq {A B : Type} {a : A} {b : B} {H : A = B} (H1 : cast H a = b) : a == b :=
|
||||
calc a == cast H a : hsymm (cast_heq H a)
|
||||
... = b : H1
|
||||
|
||||
theorem cast_trans {A B C : Type} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a
|
||||
:= heq_to_eq (calc cast Hbc (cast Hab a) == cast Hab a : cast_heq Hbc (cast Hab a)
|
||||
... == a : cast_heq Hab a
|
||||
... == cast (Hab ⬝ Hbc) a : hsymm (cast_heq (Hab ⬝ Hbc) a))
|
||||
theorem cast_trans {A B C : Type} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
|
||||
heq_to_eq (calc cast Hbc (cast Hab a) == cast Hab a : cast_heq Hbc (cast Hab a)
|
||||
... == a : cast_heq Hab a
|
||||
... == cast (Hab ⬝ Hbc) a : hsymm (cast_heq (Hab ⬝ Hbc) a))
|
||||
|
||||
theorem dcongr2 {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b
|
||||
:= have e1 : ∀ (H : B a = B a), cast H (f a) = f a, from
|
||||
assume H, cast_eq H (f a),
|
||||
have e2 : ∀ (H : B a = B b), cast H (f a) = f b, from
|
||||
subst H e1,
|
||||
have e3 : cast (congr2 B H) (f a) = f b, from
|
||||
e2 (congr2 B H),
|
||||
cast_eq_to_heq e3
|
||||
theorem dcongr2 {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b :=
|
||||
have e1 : ∀ (H : B a = B a), cast H (f a) = f a, from
|
||||
assume H, cast_eq H (f a),
|
||||
have e2 : ∀ (H : B a = B b), cast H (f a) = f b, from
|
||||
subst H e1,
|
||||
have e3 : cast (congr2 B H) (f a) = f b, from
|
||||
e2 (congr2 B H),
|
||||
cast_eq_to_heq e3
|
||||
|
||||
theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x)
|
||||
:= subst H (refl (Π x, B x))
|
||||
theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) :=
|
||||
subst H (refl (Π x, B x))
|
||||
|
||||
theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) : cast (pi_eq H) f a == f a
|
||||
:= have H1 : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from
|
||||
assume H, eq_to_heq (congr1 (cast_eq H f) a),
|
||||
have H2 : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from
|
||||
subst H H1,
|
||||
H2 (pi_eq H)
|
||||
theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) : cast (pi_eq H) f a == f a :=
|
||||
have H1 : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from
|
||||
assume H, eq_to_heq (congr1 (cast_eq H f) a),
|
||||
have H2 : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from
|
||||
subst H H1,
|
||||
H2 (pi_eq H)
|
||||
|
||||
theorem cast_pull {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
|
||||
cast (pi_eq H) f a = cast (congr1 H a) (f a)
|
||||
:= heq_to_eq (calc cast (pi_eq H) f a == f a : cast_app' H f a
|
||||
... == cast (congr1 H a) (f a) : hsymm (cast_heq (congr1 H a) (f a)))
|
||||
cast (pi_eq H) f a = cast (congr1 H a) (f a) :=
|
||||
heq_to_eq (calc cast (pi_eq H) f a == f a : cast_app' H f a
|
||||
... == cast (congr1 H a) (f a) : hsymm (cast_heq (congr1 H a) (f a)))
|
||||
|
||||
theorem hcongr1' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H1 : f == f') (H2 : B = B') : f a == f' a
|
||||
:= heq_elim H1 (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'),
|
||||
calc f a == cast (pi_eq H2) f a : hsymm (cast_app' H2 f a)
|
||||
... = cast Ht f a : refl (cast Ht f a)
|
||||
... = f' a : congr1 Hw a)
|
||||
theorem hcongr1' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H1 : f == f') (H2 : B = B')
|
||||
: f a == f' a :=
|
||||
heq_elim H1 (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'),
|
||||
calc f a == cast (pi_eq H2) f a : hsymm (cast_app' H2 f a)
|
||||
... = cast Ht f a : refl (cast Ht f a)
|
||||
... = f' a : congr1 Hw a)
|
||||
|
|
|
@ -6,151 +6,156 @@ using eq_proofs
|
|||
|
||||
axiom prop_complete (a : Prop) : a = true ∨ a = false
|
||||
|
||||
theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a
|
||||
:= or_elim (prop_complete a)
|
||||
(assume Ht : a = true, Ht⁻¹ ▸ H1)
|
||||
(assume Hf : a = false, Hf⁻¹ ▸ H2)
|
||||
theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
|
||||
or_elim (prop_complete a)
|
||||
(assume Ht : a = true, Ht⁻¹ ▸ H1)
|
||||
(assume Hf : a = false, Hf⁻¹ ▸ H2)
|
||||
|
||||
theorem em (a : Prop) : a ∨ ¬a
|
||||
:= or_elim (prop_complete a)
|
||||
(assume Ht : a = true, or_inl (eqt_elim Ht))
|
||||
(assume Hf : a = false, or_inr (eqf_elim Hf))
|
||||
theorem em (a : Prop) : a ∨ ¬a :=
|
||||
or_elim (prop_complete a)
|
||||
(assume Ht : a = true, or_inl (eqt_elim Ht))
|
||||
(assume Hf : a = false, or_inr (eqf_elim Hf))
|
||||
|
||||
theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true
|
||||
:= case (λ x, x = false ∨ x = true)
|
||||
(or_inr (refl true))
|
||||
(or_inl (refl false))
|
||||
a
|
||||
theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true :=
|
||||
case (λ x, x = false ∨ x = true)
|
||||
(or_inr (refl true))
|
||||
(or_inl (refl false))
|
||||
a
|
||||
|
||||
theorem not_true : (¬true) = false
|
||||
:= have aux : (¬true) ≠ true, from
|
||||
assume H : (¬true) = true,
|
||||
absurd_not_true (H⁻¹ ▸ trivial),
|
||||
resolve_right (prop_complete (¬true)) aux
|
||||
theorem not_true : (¬true) = false :=
|
||||
have aux : (¬true) ≠ true, from
|
||||
assume H : (¬true) = true,
|
||||
absurd_not_true (H⁻¹ ▸ trivial),
|
||||
resolve_right (prop_complete (¬true)) aux
|
||||
|
||||
theorem not_false : (¬false) = true
|
||||
:= have aux : (¬false) ≠ false, from
|
||||
assume H : (¬false) = false,
|
||||
H ▸ not_false_trivial,
|
||||
resolve_right (prop_complete_swapped (¬false)) aux
|
||||
theorem not_false : (¬false) = true :=
|
||||
have aux : (¬false) ≠ false, from
|
||||
assume H : (¬false) = false,
|
||||
H ▸ not_false_trivial,
|
||||
resolve_right (prop_complete_swapped (¬false)) aux
|
||||
|
||||
theorem not_not_eq (a : Prop) : (¬¬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_eq (a : Prop) : (¬¬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 : Prop} (H : ¬¬a) : a
|
||||
:= (not_not_eq a) ◂ H
|
||||
theorem not_not_elim {a : Prop} (H : ¬¬a) : a :=
|
||||
(not_not_eq a) ◂ H
|
||||
|
||||
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 (a = b) (Hbf ▸ (Hab (eqt_elim Hat)))))
|
||||
(assume Haf, or_elim (prop_complete b)
|
||||
(assume Hbt, false_elim (a = b) (Haf ▸ (Hba (eqt_elim Hbt))))
|
||||
(assume Hbf, Haf ⬝ Hbf⁻¹))
|
||||
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 (a = b) (Hbf ▸ (Hab (eqt_elim Hat)))))
|
||||
(assume Haf, or_elim (prop_complete b)
|
||||
(assume Hbt, false_elim (a = b) (Haf ▸ (Hba (eqt_elim Hbt))))
|
||||
(assume Hbf, Haf ⬝ Hbf⁻¹))
|
||||
|
||||
theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b
|
||||
:= iff_elim (assume H1 H2, propext H1 H2) H
|
||||
theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b :=
|
||||
iff_elim (assume H1 H2, propext H1 H2) H
|
||||
|
||||
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b)
|
||||
:= propext
|
||||
(assume H, iff_to_eq H)
|
||||
(assume H, eq_to_iff H)
|
||||
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
|
||||
propext
|
||||
(assume H, iff_to_eq H)
|
||||
(assume H, eq_to_iff H)
|
||||
|
||||
theorem eqt_intro {a : Prop} (H : a) : a = true
|
||||
:= propext (assume H1 : a, trivial)
|
||||
(assume H2 : true, H)
|
||||
theorem eqt_intro {a : Prop} (H : a) : a = true :=
|
||||
propext
|
||||
(assume H1 : a, trivial)
|
||||
(assume H2 : true, H)
|
||||
|
||||
theorem eqf_intro {a : Prop} (H : ¬a) : a = false
|
||||
:= propext (assume H1 : a, absurd H1 H)
|
||||
(assume H2 : false, false_elim a H2)
|
||||
theorem eqf_intro {a : Prop} (H : ¬a) : a = false :=
|
||||
propext
|
||||
(assume H1 : a, absurd H1 H)
|
||||
(assume H2 : false, false_elim a H2)
|
||||
|
||||
theorem by_contradiction {a : Prop} (H : ¬a → false) : a
|
||||
:= or_elim (em a) (assume H1 : a, H1) (assume H1 : ¬a, false_elim a (H H1))
|
||||
theorem by_contradiction {a : Prop} (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
|
||||
:= propext (assume H, a_neq_a_elim H)
|
||||
(assume H, false_elim (a ≠ a) H)
|
||||
theorem a_neq_a {A : Type} (a : A) : (a ≠ a) = false :=
|
||||
propext
|
||||
(assume H, a_neq_a_elim H)
|
||||
(assume H, false_elim (a ≠ a) H)
|
||||
|
||||
theorem eq_id {A : Type} (a : A) : (a = a) = true
|
||||
:= eqt_intro (refl a)
|
||||
theorem eq_id {A : Type} (a : A) : (a = a) = true :=
|
||||
eqt_intro (refl a)
|
||||
|
||||
theorem heq_id {A : Type} (a : A) : (a == a) = true
|
||||
:= eqt_intro (hrefl a)
|
||||
theorem heq_id {A : Type} (a : A) : (a == a) = true :=
|
||||
eqt_intro (hrefl a)
|
||||
|
||||
theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b)
|
||||
:= propext
|
||||
(assume H, or_elim (em a)
|
||||
(assume Ha, absurd_elim (¬a ∧ ¬b) (or_inl Ha) H)
|
||||
(assume Hna, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬a ∧ ¬b) (or_inr Hb) H)
|
||||
(assume Hnb, and_intro Hna Hnb)))
|
||||
(assume (H : ¬a ∧ ¬b) (N : a ∨ b),
|
||||
or_elim N
|
||||
(assume Ha, absurd Ha (and_elim_left H))
|
||||
(assume Hb, absurd Hb (and_elim_right H)))
|
||||
theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b) :=
|
||||
propext
|
||||
(assume H, or_elim (em a)
|
||||
(assume Ha, absurd_elim (¬a ∧ ¬b) (or_inl Ha) H)
|
||||
(assume Hna, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬a ∧ ¬b) (or_inr Hb) H)
|
||||
(assume Hnb, and_intro Hna Hnb)))
|
||||
(assume (H : ¬a ∧ ¬b) (N : a ∨ b),
|
||||
or_elim N
|
||||
(assume Ha, absurd Ha (and_elim_left H))
|
||||
(assume Hb, absurd Hb (and_elim_right H)))
|
||||
|
||||
theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b)
|
||||
:= propext
|
||||
(assume H, or_elim (em a)
|
||||
(assume Ha, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬a ∨ ¬b) (and_intro Ha Hb) H)
|
||||
(assume Hnb, or_inr Hnb))
|
||||
(assume Hna, or_inl Hna))
|
||||
(assume (H : ¬a ∨ ¬b) (N : a ∧ b),
|
||||
or_elim H
|
||||
(assume Hna, absurd (and_elim_left N) Hna)
|
||||
(assume Hnb, absurd (and_elim_right N) Hnb))
|
||||
theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b) :=
|
||||
propext
|
||||
(assume H, or_elim (em a)
|
||||
(assume Ha, or_elim (em b)
|
||||
(assume Hb, absurd_elim (¬a ∨ ¬b) (and_intro Ha Hb) H)
|
||||
(assume Hnb, or_inr Hnb))
|
||||
(assume Hna, or_inl Hna))
|
||||
(assume (H : ¬a ∨ ¬b) (N : a ∧ b),
|
||||
or_elim H
|
||||
(assume Hna, absurd (and_elim_left N) Hna)
|
||||
(assume Hnb, absurd (and_elim_right N) Hnb))
|
||||
|
||||
theorem imp_or (a b : Prop) : (a → b) = (¬a ∨ b)
|
||||
:= propext
|
||||
(assume H : a → b, (or_elim (em a)
|
||||
(assume Ha : a, or_inr (H Ha))
|
||||
(assume Hna : ¬a, or_inl Hna)))
|
||||
(assume (H : ¬a ∨ b) (Ha : a),
|
||||
resolve_right H ((not_not_eq a)⁻¹ ◂ Ha))
|
||||
theorem imp_or (a b : Prop) : (a → b) = (¬a ∨ b) :=
|
||||
propext
|
||||
(assume H : a → b, (or_elim (em a)
|
||||
(assume Ha : a, or_inr (H Ha))
|
||||
(assume Hna : ¬a, or_inl Hna)))
|
||||
(assume (H : ¬a ∨ b) (Ha : a),
|
||||
resolve_right H ((not_not_eq a)⁻¹ ◂ Ha))
|
||||
|
||||
theorem not_implies (a b : Prop) : (¬(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 : Prop) : (¬(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 : Prop) : (a = ¬a) = false
|
||||
:= propext
|
||||
(assume H, or_elim (em a)
|
||||
(assume Ha, absurd Ha (H ▸ Ha))
|
||||
(assume Hna, absurd (H⁻¹ ▸ Hna) Hna))
|
||||
(assume H, false_elim (a = ¬a) H)
|
||||
theorem a_eq_not_a (a : Prop) : (a = ¬a) = false :=
|
||||
propext
|
||||
(assume H, or_elim (em a)
|
||||
(assume Ha, absurd Ha (H ▸ Ha))
|
||||
(assume Hna, absurd (H⁻¹ ▸ Hna) Hna))
|
||||
(assume H, false_elim (a = ¬a) H)
|
||||
|
||||
theorem true_eq_false : (true = false) = false
|
||||
:= not_true ▸ (a_eq_not_a true)
|
||||
theorem true_eq_false : (true = false) = false :=
|
||||
not_true ▸ (a_eq_not_a true)
|
||||
|
||||
theorem false_eq_true : (false = true) = false
|
||||
:= not_false ▸ (a_eq_not_a false)
|
||||
theorem false_eq_true : (false = true) = false :=
|
||||
not_false ▸ (a_eq_not_a false)
|
||||
|
||||
theorem a_eq_true (a : Prop) : (a = true) = a
|
||||
:= propext (assume H, eqt_elim H) (assume H, eqt_intro H)
|
||||
theorem a_eq_true (a : Prop) : (a = true) = a :=
|
||||
propext (assume H, eqt_elim H) (assume H, eqt_intro H)
|
||||
|
||||
theorem a_eq_false (a : Prop) : (a = false) = ¬a
|
||||
:= propext (assume H, eqf_elim H) (assume H, eqf_intro H)
|
||||
theorem a_eq_false (a : Prop) : (a = false) = ¬a :=
|
||||
propext (assume H, eqf_elim H) (assume H, eqf_intro H)
|
||||
|
||||
theorem not_exists_forall {A : Type} {P : A → Prop} (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)
|
||||
theorem not_exists_forall {A : Type} {P : A → Prop} (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)
|
||||
|
||||
theorem not_forall_exists {A : Type} {P : A → Prop} (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 not_forall_exists {A : Type} {P : A → Prop} (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 : Prop) : ((a → b) → a) → a
|
||||
:= assume H, by_contradiction (assume Hna : ¬a,
|
||||
have Hnna : ¬¬a, from not_implies_left (mt H Hna),
|
||||
absurd (not_not_elim Hnna) Hna)
|
||||
theorem peirce (a b : Prop) : ((a → b) → a) → a :=
|
||||
assume H, by_contradiction (assume Hna : ¬a,
|
||||
have Hnna : ¬¬a, from not_implies_left (mt H Hna),
|
||||
absurd (not_not_elim Hnna) Hna)
|
||||
|
|
|
@ -8,64 +8,64 @@ inductive decidable (p : Prop) : Type :=
|
|||
| inl : p → decidable p
|
||||
| inr : ¬p → decidable p
|
||||
|
||||
theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
|
||||
:= decidable_rec H1 H2 H
|
||||
theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
|
||||
decidable_rec H1 H2 H
|
||||
|
||||
theorem em (p : Prop) (H : decidable p) : p ∨ ¬p
|
||||
:= induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
|
||||
theorem em (p : Prop) (H : decidable p) : p ∨ ¬p :=
|
||||
induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
|
||||
|
||||
definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
|
||||
:= decidable_rec H1 H2 H
|
||||
definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
|
||||
decidable_rec H1 H2 H
|
||||
|
||||
theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2
|
||||
:= decidable_rec
|
||||
(assume Hp1 : p, decidable_rec
|
||||
(assume Hp2 : p, congr2 inl (refl Hp1)) -- using proof irrelevance for Prop
|
||||
(assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2)
|
||||
d2)
|
||||
(assume Hnp1 : ¬p, decidable_rec
|
||||
(assume Hp2 : p, absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1)
|
||||
(assume Hnp2 : ¬p, congr2 inr (refl Hnp1)) -- using proof irrelevance for Prop
|
||||
d2)
|
||||
d1
|
||||
theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
|
||||
decidable_rec
|
||||
(assume Hp1 : p, decidable_rec
|
||||
(assume Hp2 : p, congr2 inl (refl Hp1)) -- using proof irrelevance for Prop
|
||||
(assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2)
|
||||
d2)
|
||||
(assume Hnp1 : ¬p, decidable_rec
|
||||
(assume Hp2 : p, absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1)
|
||||
(assume Hnp2 : ¬p, congr2 inr (refl Hnp1)) -- using proof irrelevance for Prop
|
||||
d2)
|
||||
d1
|
||||
|
||||
theorem decidable_true [instance] : decidable true
|
||||
:= inl trivial
|
||||
theorem decidable_true [instance] : decidable true :=
|
||||
inl trivial
|
||||
|
||||
theorem decidable_false [instance] : decidable false
|
||||
:= inr not_false_trivial
|
||||
theorem decidable_false [instance] : decidable false :=
|
||||
inr not_false_trivial
|
||||
|
||||
theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b)
|
||||
:= rec_on Ha
|
||||
(assume Ha : a, rec_on Hb
|
||||
(assume Hb : b, inl (and_intro Ha Hb))
|
||||
(assume Hnb : ¬b, inr (and_not_right a Hnb)))
|
||||
(assume Hna : ¬a, inr (and_not_left b Hna))
|
||||
theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b) :=
|
||||
rec_on Ha
|
||||
(assume Ha : a, rec_on Hb
|
||||
(assume Hb : b, inl (and_intro Ha Hb))
|
||||
(assume Hnb : ¬b, inr (and_not_right a Hnb)))
|
||||
(assume Hna : ¬a, inr (and_not_left b Hna))
|
||||
|
||||
theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b)
|
||||
:= rec_on Ha
|
||||
(assume Ha : a, inl (or_inl Ha))
|
||||
(assume Hna : ¬a, rec_on Hb
|
||||
(assume Hb : b, inl (or_inr Hb))
|
||||
(assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
|
||||
theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b) :=
|
||||
rec_on Ha
|
||||
(assume Ha : a, inl (or_inl Ha))
|
||||
(assume Hna : ¬a, rec_on Hb
|
||||
(assume Hb : b, inl (or_inr Hb))
|
||||
(assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
|
||||
|
||||
theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a)
|
||||
:= rec_on Ha
|
||||
(assume Ha, inr (not_not_intro Ha))
|
||||
(assume Hna, inl Hna)
|
||||
theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
|
||||
rec_on Ha
|
||||
(assume Ha, inr (not_not_intro Ha))
|
||||
(assume Hna, inl Hna)
|
||||
|
||||
theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b)
|
||||
:= rec_on Ha
|
||||
(assume Ha, rec_on Hb
|
||||
(assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha)))
|
||||
(assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff_mp_left H Ha) Hnb)))
|
||||
(assume Hna, rec_on Hb
|
||||
(assume Hb : b, inr (assume H : a ↔ b, absurd (iff_mp_right H Hb) Hna))
|
||||
(assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
|
||||
theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b) :=
|
||||
rec_on Ha
|
||||
(assume Ha, rec_on Hb
|
||||
(assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha)))
|
||||
(assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff_mp_left H Ha) Hnb)))
|
||||
(assume Hna, rec_on Hb
|
||||
(assume Hb : b, inr (assume H : a ↔ b, absurd (iff_mp_right H Hb) Hna))
|
||||
(assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
|
||||
|
||||
theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b)
|
||||
:= rec_on Ha
|
||||
(assume Ha : a, rec_on Hb
|
||||
(assume Hb : b, inl (assume H, Hb))
|
||||
(assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
|
||||
(assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna))
|
||||
theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) :=
|
||||
rec_on Ha
|
||||
(assume Ha : a, rec_on Hb
|
||||
(assume Hb : b, inl (assume H, Hb))
|
||||
(assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
|
||||
(assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna))
|
||||
|
|
|
@ -16,37 +16,37 @@ definition u [private] := epsilon (λ x, x = true ∨ p)
|
|||
|
||||
definition v [private] := epsilon (λ x, x = false ∨ p)
|
||||
|
||||
lemma u_def [private] : u = true ∨ p
|
||||
:= epsilon_ax (exists_intro true (or_inl (refl true)))
|
||||
lemma u_def [private] : u = true ∨ p :=
|
||||
epsilon_ax (exists_intro true (or_inl (refl true)))
|
||||
|
||||
lemma v_def [private] : v = false ∨ p
|
||||
:= epsilon_ax (exists_intro false (or_inl (refl false)))
|
||||
lemma v_def [private] : v = false ∨ p :=
|
||||
epsilon_ax (exists_intro false (or_inl (refl false)))
|
||||
|
||||
lemma uv_implies_p [private] : ¬(u = v) ∨ p
|
||||
:= or_elim u_def
|
||||
(assume Hut : u = true, or_elim v_def
|
||||
(assume Hvf : v = false,
|
||||
have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
|
||||
or_inl Hne)
|
||||
(assume Hp : p, or_inr Hp))
|
||||
(assume Hp : p, or_inr Hp)
|
||||
lemma uv_implies_p [private] : ¬(u = v) ∨ p :=
|
||||
or_elim u_def
|
||||
(assume Hut : u = true, or_elim v_def
|
||||
(assume Hvf : v = false,
|
||||
have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
|
||||
or_inl Hne)
|
||||
(assume Hp : p, or_inr Hp))
|
||||
(assume Hp : p, or_inr Hp)
|
||||
|
||||
lemma p_implies_uv [private] : p → u = v
|
||||
:= assume Hp : p,
|
||||
have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from
|
||||
funext (take x : Prop,
|
||||
have Hl : (x = true ∨ p) → (x = false ∨ p), from
|
||||
assume A, or_inr Hp,
|
||||
have Hr : (x = false ∨ p) → (x = true ∨ p), from
|
||||
assume A, or_inr Hp,
|
||||
show (x = true ∨ p) = (x = false ∨ p), from
|
||||
propext Hl Hr),
|
||||
show u = v, from
|
||||
Hpred ▸ (refl (epsilon (λ x, x = true ∨ p)))
|
||||
lemma p_implies_uv [private] : p → u = v :=
|
||||
assume Hp : p,
|
||||
have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from
|
||||
funext (take x : Prop,
|
||||
have Hl : (x = true ∨ p) → (x = false ∨ p), from
|
||||
assume A, or_inr Hp,
|
||||
have Hr : (x = false ∨ p) → (x = true ∨ p), from
|
||||
assume A, or_inr Hp,
|
||||
show (x = true ∨ p) = (x = false ∨ p), from
|
||||
propext Hl Hr),
|
||||
show u = v, from
|
||||
Hpred ▸ (refl (epsilon (λ x, x = true ∨ p)))
|
||||
|
||||
theorem em : p ∨ ¬p
|
||||
:= have H : ¬(u = v) → ¬p, from contrapos p_implies_uv,
|
||||
or_elim uv_implies_p
|
||||
(assume Hne : ¬(u = v), or_inr (H Hne))
|
||||
(assume Hp : p, or_inl Hp)
|
||||
theorem em : p ∨ ¬p :=
|
||||
have H : ¬(u = v) → ¬p, from contrapos p_implies_uv,
|
||||
or_elim uv_implies_p
|
||||
(assume Hne : ¬(u = v), or_inr (H Hne))
|
||||
(assume Hp : p, or_inl Hp)
|
||||
end
|
||||
|
|
|
@ -16,12 +16,12 @@ end
|
|||
inductive equivalence {A : Type} (p : A → A → Prop) : Prop :=
|
||||
| equivalence_intro : reflexive p → symmetric p → transitive p → equivalence p
|
||||
|
||||
theorem equivalence_reflexive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : reflexive p
|
||||
:= equivalence_rec (λ r s t, r) H
|
||||
theorem equivalence_reflexive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : reflexive p :=
|
||||
equivalence_rec (λ r s t, r) H
|
||||
|
||||
theorem equivalence_symmetric [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : symmetric p
|
||||
:= equivalence_rec (λ r s t, s) H
|
||||
theorem equivalence_symmetric [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : symmetric p :=
|
||||
equivalence_rec (λ r s t, s) H
|
||||
|
||||
theorem equivalence_transitive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : transitive p
|
||||
:= equivalence_rec (λ r s t, t) H
|
||||
theorem equivalence_transitive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : transitive p :=
|
||||
equivalence_rec (λ r s t, t) H
|
||||
end
|
|
@ -6,34 +6,34 @@ namespace function
|
|||
section
|
||||
parameters {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
|
||||
|
||||
abbreviation compose (f : B → C) (g : A → B) : A → C
|
||||
:= λx, f (g x)
|
||||
abbreviation compose (f : B → C) (g : A → B) : A → C :=
|
||||
λx, f (g x)
|
||||
|
||||
abbreviation id (a : A) : A
|
||||
:= a
|
||||
abbreviation id (a : A) : A :=
|
||||
a
|
||||
|
||||
abbreviation on_fun (f : B → B → C) (g : A → B) : A → A → C
|
||||
:= λx y, f (g x) (g y)
|
||||
abbreviation on_fun (f : B → B → C) (g : A → B) : A → A → C :=
|
||||
λx y, f (g x) (g y)
|
||||
|
||||
abbreviation combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E
|
||||
:= λx y, op (f x y) (g x y)
|
||||
abbreviation combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
|
||||
λx y, op (f x y) (g x y)
|
||||
end
|
||||
|
||||
abbreviation const {A : Type} (B : Type) (a : A) : B → A
|
||||
:= λx, a
|
||||
abbreviation const {A : Type} (B : Type) (a : A) : B → A :=
|
||||
λx, a
|
||||
|
||||
abbreviation dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x)
|
||||
:= λx, f (g x)
|
||||
abbreviation dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
|
||||
λx, f (g x)
|
||||
|
||||
abbreviation flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y
|
||||
:= λy x, f x y
|
||||
abbreviation flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
|
||||
λy x, f x y
|
||||
|
||||
abbreviation app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x
|
||||
:= f x
|
||||
abbreviation app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x :=
|
||||
f x
|
||||
|
||||
-- Yet another trick to anotate an expression with a type
|
||||
abbreviation is_typeof (A : Type) (a : A) : A
|
||||
:= a
|
||||
abbreviation is_typeof (A : Type) (a : A) : A :=
|
||||
a
|
||||
|
||||
precedence `∘`:60
|
||||
precedence `∘'`:60
|
||||
|
|
|
@ -10,15 +10,15 @@ axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x
|
|||
namespace function
|
||||
section
|
||||
parameters {A : Type} {B : Type} {C : Type} {D : Type}
|
||||
theorem compose_assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h)
|
||||
:= funext (take x, refl _)
|
||||
theorem compose_assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
|
||||
funext (take x, refl _)
|
||||
|
||||
theorem compose_id_left (f : A → B) : id ∘ f = f
|
||||
:= funext (take x, refl _)
|
||||
theorem compose_id_left (f : A → B) : id ∘ f = f :=
|
||||
funext (take x, refl _)
|
||||
|
||||
theorem compose_id_right (f : A → B) : f ∘ id = f
|
||||
:= funext (take x, refl _)
|
||||
theorem compose_id_right (f : A → B) : f ∘ id = f :=
|
||||
funext (take x, refl _)
|
||||
|
||||
theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b)
|
||||
:= funext (take x, refl _)
|
||||
theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) :=
|
||||
funext (take x, refl _)
|
||||
end end
|
|
@ -6,17 +6,17 @@ import logic
|
|||
variable epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A
|
||||
axiom epsilon_ax {A : Type} {P : A → Prop} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P)
|
||||
|
||||
theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (inhabited_intro a) (λ x, x = a) = a
|
||||
:= epsilon_ax (exists_intro a (refl a))
|
||||
theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (inhabited_intro a) (λ x, x = a) = a :=
|
||||
epsilon_ax (exists_intro a (refl a))
|
||||
|
||||
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Prop} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
|
||||
:= let f [inline] := λ x, @epsilon _ (inhabited_exists (H x)) (λ y, R x y),
|
||||
H [inline] := take x, epsilon_ax (H x)
|
||||
in exists_intro f H
|
||||
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Prop} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) :=
|
||||
let f [inline] := λ x, @epsilon _ (inhabited_exists (H x)) (λ y, R x y),
|
||||
H [inline] := take x, epsilon_ax (H x)
|
||||
in exists_intro f H
|
||||
|
||||
theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x))
|
||||
:= iff_intro
|
||||
(assume H : (∀ x, ∃ y, P x y), axiom_of_choice H)
|
||||
(assume H : (∃ f, (∀ x, P x (f x))),
|
||||
take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H,
|
||||
exists_intro (fw x) (Hw x))
|
||||
theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) :=
|
||||
iff_intro
|
||||
(assume H : (∀ x, ∃ y, P x y), axiom_of_choice H)
|
||||
(assume H : (∃ f, (∀ x, P x (f x))),
|
||||
take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H,
|
||||
exists_intro (fw x) (Hw x))
|
||||
|
|
|
@ -4,31 +4,31 @@
|
|||
import decidable tactic
|
||||
using decidable tactic
|
||||
|
||||
definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A
|
||||
:= rec_on H (assume Hc, t) (assume Hnc, e)
|
||||
definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
|
||||
rec_on H (assume Hc, t) (assume Hnc, e)
|
||||
|
||||
notation `if` c `then` t `else` e:45 := ite c t e
|
||||
|
||||
theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t
|
||||
:= decidable_rec
|
||||
(assume Hc : c, refl (@ite c (inl Hc) A t e))
|
||||
(assume Hnc : ¬c, absurd_elim (@ite c (inr Hnc) A t e = t) Hc Hnc)
|
||||
H
|
||||
theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t :=
|
||||
decidable_rec
|
||||
(assume Hc : c, refl (@ite c (inl Hc) A t e))
|
||||
(assume Hnc : ¬c, absurd_elim (@ite c (inr Hnc) A t e = t) Hc Hnc)
|
||||
H
|
||||
|
||||
theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e
|
||||
:= decidable_rec
|
||||
(assume Hc : c, absurd_elim (@ite c (inl Hc) A t e = e) Hc Hnc)
|
||||
(assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e))
|
||||
H
|
||||
theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e :=
|
||||
decidable_rec
|
||||
(assume Hc : c, absurd_elim (@ite c (inl Hc) A t e = e) Hc Hnc)
|
||||
(assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e))
|
||||
H
|
||||
|
||||
theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t
|
||||
:= decidable_rec
|
||||
(assume Hc : c, refl (@ite c (inl Hc) A t t))
|
||||
(assume Hnc : ¬c, refl (@ite c (inr Hnc) A t t))
|
||||
H
|
||||
theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t :=
|
||||
decidable_rec
|
||||
(assume Hc : c, refl (@ite c (inl Hc) A t t))
|
||||
(assume Hnc : ¬c, refl (@ite c (inr Hnc) A t t))
|
||||
H
|
||||
|
||||
theorem if_true {A : Type} (t e : A) : (if true then t else e) = t
|
||||
:= if_pos trivial t e
|
||||
theorem if_true {A : Type} (t e : A) : (if true then t else e) = t :=
|
||||
if_pos trivial t e
|
||||
|
||||
theorem if_false {A : Type} (t e : A) : (if false then t else e) = e
|
||||
:= if_neg not_false_trivial t e
|
||||
theorem if_false {A : Type} (t e : A) : (if false then t else e) = e :=
|
||||
if_neg not_false_trivial t e
|
||||
|
|
|
@ -5,8 +5,8 @@ definition Prop [inline] := Type.{0}
|
|||
|
||||
inductive false : Prop
|
||||
|
||||
theorem false_elim (c : Prop) (H : false) : c
|
||||
:= false_rec c H
|
||||
theorem false_elim (c : Prop) (H : false) : c :=
|
||||
false_rec c H
|
||||
|
||||
inductive true : Prop :=
|
||||
| trivial : true
|
||||
|
@ -17,38 +17,35 @@ prefix `¬`:40 := not
|
|||
notation `assume` binders `,` r:(scoped f, f) := r
|
||||
notation `take` binders `,` r:(scoped f, f) := r
|
||||
|
||||
theorem not_intro {a : Prop} (H : a → false) : ¬a
|
||||
:= H
|
||||
theorem not_intro {a : Prop} (H : a → false) : ¬a := H
|
||||
|
||||
theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false
|
||||
:= H1 H2
|
||||
theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
|
||||
|
||||
theorem absurd {a : Prop} (H1 : a) (H2 : ¬a) : false
|
||||
:= H2 H1
|
||||
theorem absurd {a : Prop} (H1 : a) (H2 : ¬a) : false := H2 H1
|
||||
|
||||
theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a
|
||||
:= assume Hna : ¬a, absurd Ha Hna
|
||||
theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
|
||||
assume Hna : ¬a, absurd Ha Hna
|
||||
|
||||
theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a
|
||||
:= assume Ha : a, absurd (H1 Ha) H2
|
||||
theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
|
||||
assume Ha : a, absurd (H1 Ha) H2
|
||||
|
||||
theorem contrapos {a b : Prop} (H : a → b) : ¬b → ¬a
|
||||
:= assume Hnb : ¬b, mt H Hnb
|
||||
theorem contrapos {a b : Prop} (H : a → b) : ¬b → ¬a :=
|
||||
assume Hnb : ¬b, mt H Hnb
|
||||
|
||||
theorem absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬a) : b
|
||||
:= false_elim b (absurd H1 H2)
|
||||
theorem absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬a) : b :=
|
||||
false_elim b (absurd H1 H2)
|
||||
|
||||
theorem absurd_not_true (H : ¬true) : false
|
||||
:= absurd trivial H
|
||||
theorem absurd_not_true (H : ¬true) : false :=
|
||||
absurd trivial H
|
||||
|
||||
theorem not_false_trivial : ¬false
|
||||
:= assume H : false, H
|
||||
theorem not_false_trivial : ¬false :=
|
||||
assume H : false, H
|
||||
|
||||
theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a
|
||||
:= assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H
|
||||
theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
|
||||
assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H
|
||||
|
||||
theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b
|
||||
:= assume Hb : b, absurd (assume Ha : a, Hb) H
|
||||
theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
|
||||
assume Hb : b, absurd (assume Ha : a, Hb) H
|
||||
|
||||
inductive and (a b : Prop) : Prop :=
|
||||
| and_intro : a → b → and a b
|
||||
|
@ -56,23 +53,23 @@ inductive and (a b : Prop) : Prop :=
|
|||
infixr `/\`:35 := and
|
||||
infixr `∧`:35 := and
|
||||
|
||||
theorem and_elim {a b c : Prop} (H1 : a → b → c) (H2 : a ∧ b) : c
|
||||
:= and_rec H1 H2
|
||||
theorem and_elim {a b c : Prop} (H1 : a → b → c) (H2 : a ∧ b) : c :=
|
||||
and_rec H1 H2
|
||||
|
||||
theorem and_elim_left {a b : Prop} (H : a ∧ b) : a
|
||||
:= and_rec (λa b, a) H
|
||||
theorem and_elim_left {a b : Prop} (H : a ∧ b) : a :=
|
||||
and_rec (λa b, a) H
|
||||
|
||||
theorem and_elim_right {a b : Prop} (H : a ∧ b) : b
|
||||
:= and_rec (λa b, b) H
|
||||
theorem and_elim_right {a b : Prop} (H : a ∧ b) : b :=
|
||||
and_rec (λa b, b) H
|
||||
|
||||
theorem and_swap {a b : Prop} (H : a ∧ b) : b ∧ a
|
||||
:= and_intro (and_elim_right H) (and_elim_left H)
|
||||
theorem and_swap {a b : Prop} (H : a ∧ b) : b ∧ a :=
|
||||
and_intro (and_elim_right H) (and_elim_left H)
|
||||
|
||||
theorem and_not_left {a : Prop} (b : Prop) (Hna : ¬a) : ¬(a ∧ b)
|
||||
:= assume H : a ∧ b, absurd (and_elim_left H) Hna
|
||||
theorem and_not_left {a : Prop} (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (and_elim_left H) Hna
|
||||
|
||||
theorem and_not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b)
|
||||
:= assume H : a ∧ b, absurd (and_elim_right H) Hnb
|
||||
theorem and_not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (and_elim_right H) Hnb
|
||||
|
||||
inductive or (a b : Prop) : Prop :=
|
||||
| or_intro_left : a → or a b
|
||||
|
@ -84,59 +81,59 @@ infixr `∨`:30 := or
|
|||
theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha
|
||||
theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb
|
||||
|
||||
theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
|
||||
:= or_rec H2 H3 H1
|
||||
theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c :=
|
||||
or_rec H2 H3 H1
|
||||
|
||||
theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b
|
||||
:= or_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb)
|
||||
theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b :=
|
||||
or_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb)
|
||||
|
||||
theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a
|
||||
:= or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
|
||||
theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a :=
|
||||
or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
|
||||
|
||||
theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a
|
||||
:= or_elim H (assume Ha, or_inr Ha) (assume Hb, or_inl Hb)
|
||||
theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a :=
|
||||
or_elim H (assume Ha, or_inr Ha) (assume Hb, or_inl Hb)
|
||||
|
||||
theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b)
|
||||
:= assume H : a ∨ b, or_elim H
|
||||
(assume Ha, absurd_elim _ Ha Hna)
|
||||
(assume Hb, absurd_elim _ Hb Hnb)
|
||||
theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
|
||||
assume H : a ∨ b, or_elim H
|
||||
(assume Ha, absurd_elim _ Ha Hna)
|
||||
(assume Hb, absurd_elim _ Hb Hnb)
|
||||
|
||||
theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d
|
||||
:= or_elim H1
|
||||
(assume Ha : a, or_inl (H2 Ha))
|
||||
(assume Hb : b, or_inr (H3 Hb))
|
||||
theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d :=
|
||||
or_elim H1
|
||||
(assume Ha : a, or_inl (H2 Ha))
|
||||
(assume Hb : b, or_inr (H3 Hb))
|
||||
|
||||
theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c
|
||||
:= or_elim H1
|
||||
(assume H2 : a, or_inl (H H2))
|
||||
(assume H2 : c, or_inr H2)
|
||||
theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c :=
|
||||
or_elim H1
|
||||
(assume H2 : a, or_inl (H H2))
|
||||
(assume H2 : c, or_inr H2)
|
||||
|
||||
theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b
|
||||
:= or_elim H1
|
||||
(assume H2 : c, or_inl H2)
|
||||
(assume H2 : a, or_inr (H H2))
|
||||
theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b :=
|
||||
or_elim H1
|
||||
(assume H2 : c, or_inl H2)
|
||||
(assume H2 : a, or_inr (H H2))
|
||||
|
||||
inductive eq {A : Type} (a : A) : A → Prop :=
|
||||
| refl : eq a a
|
||||
|
||||
infix `=`:50 := eq
|
||||
|
||||
theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b
|
||||
:= eq_rec H2 H1
|
||||
theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
|
||||
eq_rec H2 H1
|
||||
|
||||
theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
|
||||
:= subst H2 H1
|
||||
theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
|
||||
subst H2 H1
|
||||
|
||||
calc_subst subst
|
||||
calc_refl refl
|
||||
calc_trans trans
|
||||
|
||||
theorem true_ne_false : ¬true = false
|
||||
:= assume H : true = false,
|
||||
subst H trivial
|
||||
theorem true_ne_false : ¬true = false :=
|
||||
assume H : true = false,
|
||||
subst H trivial
|
||||
|
||||
theorem symm {A : Type} {a b : A} (H : a = b) : b = a
|
||||
:= subst H (refl a)
|
||||
theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
|
||||
subst H (refl a)
|
||||
|
||||
namespace eq_proofs
|
||||
postfix `⁻¹`:100 := symm
|
||||
|
@ -145,68 +142,62 @@ namespace eq_proofs
|
|||
end
|
||||
using eq_proofs
|
||||
|
||||
theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
|
||||
:= H ▸ (refl (f a))
|
||||
theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
|
||||
H ▸ refl (f a)
|
||||
|
||||
theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b
|
||||
:= H ▸ (refl (f a))
|
||||
theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
|
||||
H ▸ refl (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
|
||||
:= H1 ▸ H2 ▸ (refl (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 :=
|
||||
H1 ▸ 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
|
||||
:= take x, congr1 H 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 : Prop} (H : a = b) : (¬a) = (¬b)
|
||||
:= congr2 not H
|
||||
theorem not_congr {a b : Prop} (H : a = b) : (¬a) = (¬b) :=
|
||||
congr2 not H
|
||||
|
||||
theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b
|
||||
:= H1 ▸ H2
|
||||
theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
|
||||
H1 ▸ H2
|
||||
|
||||
infixl `<|`:100 := eqmp
|
||||
infixl `◂`:100 := eqmp
|
||||
|
||||
theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a
|
||||
:= H1⁻¹ ◂ H2
|
||||
theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
|
||||
H1⁻¹ ◂ H2
|
||||
|
||||
theorem eqt_elim {a : Prop} (H : a = true) : a
|
||||
:= H⁻¹ ◂ trivial
|
||||
theorem eqt_elim {a : Prop} (H : a = true) : a :=
|
||||
H⁻¹ ◂ trivial
|
||||
|
||||
theorem eqf_elim {a : Prop} (H : a = false) : ¬a
|
||||
:= assume Ha : a, H ◂ Ha
|
||||
theorem eqf_elim {a : Prop} (H : a = false) : ¬a :=
|
||||
assume Ha : a, H ◂ Ha
|
||||
|
||||
theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c
|
||||
:= assume Ha, H2 (H1 Ha)
|
||||
theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 Ha)
|
||||
|
||||
theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c
|
||||
:= assume Ha, H2 ◂ (H1 Ha)
|
||||
theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c :=
|
||||
assume Ha, H2 ◂ (H1 Ha)
|
||||
|
||||
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c
|
||||
:= assume Ha, H2 (H1 ◂ Ha)
|
||||
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 ◂ Ha)
|
||||
|
||||
definition ne [inline] {A : Type} (a b : A) := ¬(a = b)
|
||||
infix `≠`:50 := ne
|
||||
|
||||
theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b
|
||||
:= H
|
||||
theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := H
|
||||
|
||||
theorem ne_elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false
|
||||
:= H1 H2
|
||||
theorem ne_elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false := H1 H2
|
||||
|
||||
theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false
|
||||
:= H (refl a)
|
||||
theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := H (refl a)
|
||||
|
||||
theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false
|
||||
:= H (refl a)
|
||||
theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H (refl a)
|
||||
|
||||
theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a
|
||||
:= assume H1 : b = a, H (H1⁻¹)
|
||||
theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
|
||||
assume H1 : b = a, H (H1⁻¹)
|
||||
|
||||
theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c
|
||||
:= H1⁻¹ ▸ H2
|
||||
theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := H1⁻¹ ▸ H2
|
||||
|
||||
theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
|
||||
:= H2 ▸ H1
|
||||
theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := H2 ▸ H1
|
||||
|
||||
calc_trans eq_ne_trans
|
||||
calc_trans ne_eq_trans
|
||||
|
@ -215,74 +206,72 @@ definition iff (a b : Prop) := (a → b) ∧ (b → a)
|
|||
infix `<->`:25 := iff
|
||||
infix `↔`:25 := iff
|
||||
|
||||
theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b
|
||||
:= and_intro H1 H2
|
||||
theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2
|
||||
|
||||
theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c
|
||||
:= and_rec H1 H2
|
||||
theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and_rec H1 H2
|
||||
|
||||
theorem iff_elim_left {a b : Prop} (H : a ↔ b) : a → b
|
||||
:= iff_elim (assume H1 H2, H1) H
|
||||
theorem iff_elim_left {a b : Prop} (H : a ↔ b) : a → b :=
|
||||
iff_elim (assume H1 H2, H1) H
|
||||
|
||||
theorem iff_elim_right {a b : Prop} (H : a ↔ b) : b → a
|
||||
:= iff_elim (assume H1 H2, H2) H
|
||||
theorem iff_elim_right {a b : Prop} (H : a ↔ b) : b → a :=
|
||||
iff_elim (assume H1 H2, H2) H
|
||||
|
||||
theorem iff_mp_left {a b : Prop} (H1 : a ↔ b) (H2 : a) : b
|
||||
:= (iff_elim_left H1) H2
|
||||
theorem iff_mp_left {a b : Prop} (H1 : a ↔ b) (H2 : a) : b :=
|
||||
(iff_elim_left H1) H2
|
||||
|
||||
theorem iff_mp_right {a b : Prop} (H1 : a ↔ b) (H2 : b) : a
|
||||
:= (iff_elim_right H1) H2
|
||||
theorem iff_mp_right {a b : Prop} (H1 : a ↔ b) (H2 : b) : a :=
|
||||
(iff_elim_right H1) H2
|
||||
|
||||
theorem iff_flip_sign {a b : Prop} (H1 : a ↔ b) : ¬a ↔ ¬b
|
||||
:= iff_intro
|
||||
(assume Hna, mt (iff_elim_right H1) Hna)
|
||||
(assume Hnb, mt (iff_elim_left H1) Hnb)
|
||||
theorem iff_flip_sign {a b : Prop} (H1 : a ↔ b) : ¬a ↔ ¬b :=
|
||||
iff_intro
|
||||
(assume Hna, mt (iff_elim_right H1) Hna)
|
||||
(assume Hnb, mt (iff_elim_left H1) Hnb)
|
||||
|
||||
theorem iff_refl (a : Prop) : a ↔ a
|
||||
:= iff_intro (assume H, H) (assume H, H)
|
||||
theorem iff_refl (a : Prop) : a ↔ a :=
|
||||
iff_intro (assume H, H) (assume H, H)
|
||||
|
||||
theorem iff_trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c
|
||||
:= iff_intro
|
||||
(assume Ha, iff_mp_left H2 (iff_mp_left H1 Ha))
|
||||
(assume Hc, iff_mp_right H1 (iff_mp_right H2 Hc))
|
||||
theorem iff_trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c :=
|
||||
iff_intro
|
||||
(assume Ha, iff_mp_left H2 (iff_mp_left H1 Ha))
|
||||
(assume Hc, iff_mp_right H1 (iff_mp_right H2 Hc))
|
||||
|
||||
theorem iff_symm {a b : Prop} (H : a ↔ b) : b ↔ a
|
||||
:= iff_intro
|
||||
(assume Hb, iff_mp_right H Hb)
|
||||
(assume Ha, iff_mp_left H Ha)
|
||||
theorem iff_symm {a b : Prop} (H : a ↔ b) : b ↔ a :=
|
||||
iff_intro
|
||||
(assume Hb, iff_mp_right H Hb)
|
||||
(assume Ha, iff_mp_left H Ha)
|
||||
|
||||
calc_trans iff_trans
|
||||
|
||||
theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b
|
||||
:= iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
||||
theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
||||
|
||||
theorem and_comm (a b : Prop) : a ∧ b ↔ b ∧ a
|
||||
:= iff_intro (λH, and_swap H) (λH, and_swap H)
|
||||
theorem and_comm (a b : Prop) : a ∧ b ↔ b ∧ a :=
|
||||
iff_intro (λH, and_swap H) (λH, and_swap H)
|
||||
|
||||
theorem and_assoc (a b c : Prop) : (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 and_assoc (a b c : Prop) : (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 : Prop) : a ∨ b ↔ b ∨ a
|
||||
:= iff_intro (λH, or_swap H) (λH, or_swap H)
|
||||
theorem or_comm (a b : Prop) : a ∨ b ↔ b ∨ a :=
|
||||
iff_intro (λH, or_swap H) (λH, or_swap H)
|
||||
|
||||
theorem or_assoc (a b c : Prop) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c)
|
||||
:= iff_intro
|
||||
(assume H, or_elim H
|
||||
(assume H1, or_elim H1
|
||||
(assume Ha, or_inl Ha)
|
||||
(assume Hb, or_inr (or_inl Hb)))
|
||||
(assume Hc, or_inr (or_inr Hc)))
|
||||
(assume H, or_elim H
|
||||
(assume Ha, (or_inl (or_inl Ha)))
|
||||
(assume H1, or_elim H1
|
||||
(assume Hb, or_inl (or_inr Hb))
|
||||
(assume Hc, or_inr Hc)))
|
||||
theorem or_assoc (a b c : Prop) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
|
||||
iff_intro
|
||||
(assume H, or_elim H
|
||||
(assume H1, or_elim H1
|
||||
(assume Ha, or_inl Ha)
|
||||
(assume Hb, or_inr (or_inl Hb)))
|
||||
(assume Hc, or_inr (or_inr Hc)))
|
||||
(assume H, or_elim H
|
||||
(assume Ha, (or_inl (or_inl Ha)))
|
||||
(assume H1, or_elim H1
|
||||
(assume Hb, or_inl (or_inr Hb))
|
||||
(assume Hc, or_inr Hc)))
|
||||
|
||||
inductive Exists {A : Type} (P : A → Prop) : Prop :=
|
||||
| exists_intro : ∀ (a : A), P a → Exists P
|
||||
|
@ -290,41 +279,43 @@ inductive Exists {A : Type} (P : A → Prop) : Prop :=
|
|||
notation `exists` binders `,` r:(scoped P, Exists P) := r
|
||||
notation `∃` binders `,` r:(scoped P, Exists P) := r
|
||||
|
||||
theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B
|
||||
:= Exists_rec H2 H1
|
||||
theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
|
||||
Exists_rec H2 H1
|
||||
|
||||
theorem exists_not_forall {A : Type} {p : A → Prop} (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 exists_not_forall {A : Type} {p : A → Prop} (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 → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x
|
||||
:= assume H1 : ∃x, ¬p x,
|
||||
obtain (w : A) (Hw : ¬p w), from H1,
|
||||
absurd (H2 w) Hw
|
||||
theorem forall_not_exists {A : Type} {p : A → Prop} (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 → Prop) := ∃x, p x ∧ ∀y, y ≠ x → ¬p y
|
||||
definition exists_unique {A : Type} (p : A → Prop) :=
|
||||
∃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 → Prop} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬p y) : ∃!x, p x
|
||||
:= exists_intro w (and_intro H1 H2)
|
||||
theorem exists_unique_intro {A : Type} {p : A → Prop} (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 → Prop} {b : Prop} (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)
|
||||
theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
|
||||
(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)
|
||||
|
||||
inductive inhabited (A : Type) : Prop :=
|
||||
| inhabited_intro : A → inhabited A
|
||||
|
||||
theorem inhabited_elim {A : Type} {B : Prop} (H1 : inhabited A) (H2 : A → B) : B
|
||||
:= inhabited_rec H2 H1
|
||||
theorem inhabited_elim {A : Type} {B : Prop} (H1 : inhabited A) (H2 : A → B) : B :=
|
||||
inhabited_rec H2 H1
|
||||
|
||||
theorem inhabited_Prop [instance] : inhabited Prop
|
||||
:= inhabited_intro true
|
||||
theorem inhabited_Prop [instance] : inhabited Prop :=
|
||||
inhabited_intro true
|
||||
|
||||
theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
|
||||
:= inhabited_elim H (take b, inhabited_intro (λa, b))
|
||||
theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
|
||||
inhabited_elim H (take b, inhabited_intro (λa, b))
|
||||
|
||||
theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A
|
||||
:= obtain w Hw, from H, inhabited_intro w
|
||||
theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A :=
|
||||
obtain w Hw, from H, inhabited_intro w
|
||||
|
|
|
@ -15,9 +15,9 @@ inductive num : Type :=
|
|||
| zero : num
|
||||
| pos : pos_num → num
|
||||
|
||||
theorem inhabited_pos_num [instance] : inhabited pos_num
|
||||
:= inhabited_intro one
|
||||
theorem inhabited_pos_num [instance] : inhabited pos_num :=
|
||||
inhabited_intro one
|
||||
|
||||
theorem inhabited_num [instance] : inhabited num
|
||||
:= inhabited_intro zero
|
||||
theorem inhabited_num [instance] : inhabited num :=
|
||||
inhabited_intro zero
|
||||
end
|
|
@ -7,5 +7,5 @@ inductive option (A : Type) : Type :=
|
|||
| none {} : option A
|
||||
| some : A → option A
|
||||
|
||||
theorem inhabited_option [instance] (A : Type) : inhabited (option A)
|
||||
:= inhabited_intro none
|
||||
theorem inhabited_option [instance] (A : Type) : inhabited (option A) :=
|
||||
inhabited_intro none
|
||||
|
|
|
@ -14,23 +14,23 @@ section
|
|||
definition fst [inline] (p : pair A B) := pair_rec (λ x y, x) p
|
||||
definition snd [inline] (p : pair A B) := pair_rec (λ x y, y) p
|
||||
|
||||
theorem pair_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (pair A B)
|
||||
:= inhabited_elim H1 (λ a, inhabited_elim H2 (λ b, inhabited_intro (mk_pair a b)))
|
||||
theorem pair_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (pair A B) :=
|
||||
inhabited_elim H1 (λ a, inhabited_elim H2 (λ b, inhabited_intro (mk_pair a b)))
|
||||
|
||||
theorem fst_mk_pair (a : A) (b : B) : fst (mk_pair a b) = a
|
||||
:= refl a
|
||||
theorem fst_mk_pair (a : A) (b : B) : fst (mk_pair a b) = a :=
|
||||
refl a
|
||||
|
||||
theorem snd_mk_pair (a : A) (b : B) : snd (mk_pair a b) = b
|
||||
:= refl b
|
||||
theorem snd_mk_pair (a : A) (b : B) : snd (mk_pair a b) = b :=
|
||||
refl b
|
||||
|
||||
theorem pair_ext (p : pair A B) : mk_pair (fst p) (snd p) = p
|
||||
:= pair_rec (λ x y, refl (mk_pair x y)) p
|
||||
theorem pair_ext (p : pair A B) : mk_pair (fst p) (snd p) = p :=
|
||||
pair_rec (λ x y, refl (mk_pair x y)) p
|
||||
|
||||
theorem pair_ext_eq {p1 p2 : pair A B} (H1 : fst p1 = fst p2) (H2 : snd p1 = snd p2) : p1 = p2
|
||||
:= calc p1 = mk_pair (fst p1) (snd p1) : symm (pair_ext p1)
|
||||
... = mk_pair (fst p2) (snd p1) : {H1}
|
||||
... = mk_pair (fst p2) (snd p2) : {H2}
|
||||
... = p2 : pair_ext p2
|
||||
theorem pair_ext_eq {p1 p2 : pair A B} (H1 : fst p1 = fst p2) (H2 : snd p1 = snd p2) : p1 = p2 :=
|
||||
calc p1 = mk_pair (fst p1) (snd p1) : symm (pair_ext p1)
|
||||
... = mk_pair (fst p2) (snd p1) : {H1}
|
||||
... = mk_pair (fst p2) (snd p2) : {H2}
|
||||
... = p2 : pair_ext p2
|
||||
end
|
||||
|
||||
instance pair_inhabited
|
||||
|
|
|
@ -6,20 +6,20 @@ import logic cast
|
|||
-- Pi extensionality
|
||||
axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} : (Π x, B x) = (Π x, B' x) → B = B'
|
||||
|
||||
theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) (a : A) : cast H f a == f a
|
||||
:= have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
|
||||
have Hb : B = B', from piext H,
|
||||
cast_app' Hb f a
|
||||
theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) (a : A) : cast H f a == f a :=
|
||||
have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
|
||||
have Hb : B = B', from piext H,
|
||||
cast_app' Hb f a
|
||||
|
||||
theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H : f == f') : f a == f' a
|
||||
:= have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
|
||||
have Hb : B = B', from piext (type_eq H),
|
||||
hcongr1' a H Hb
|
||||
theorem hcongr1 {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H : f == f') : f a == f' a :=
|
||||
have Hi [fact] : inhabited (Π x, B x), from inhabited_intro f,
|
||||
have Hb : B = B', from piext (type_eq H),
|
||||
hcongr1' a H Hb
|
||||
|
||||
theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type} {f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
|
||||
(Hff' : f == f') (Haa' : a == a') : f a == f' a'
|
||||
:= have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
|
||||
take B B' f f' e, hcongr1 a e,
|
||||
have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a', from
|
||||
hsubst Haa' H1,
|
||||
H2 B B' f f' Hff'
|
||||
(Hff' : f == f') (Haa' : a == a') : f a == f' a' :=
|
||||
have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
|
||||
take B B' f f' e, hcongr1 a e,
|
||||
have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a', from
|
||||
hsubst Haa' H1,
|
||||
H2 B B' f f' Hff'
|
||||
|
|
|
@ -7,12 +7,12 @@ using decidable
|
|||
-- Excluded middle + Hilbert implies every proposition is decidable
|
||||
|
||||
-- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle
|
||||
theorem inhabited_decidable [instance] (a : Prop) : inhabited (decidable a)
|
||||
:= or_elim (em a)
|
||||
(assume Ha, inhabited_intro (inl Ha))
|
||||
(assume Hna, inhabited_intro (inr Hna))
|
||||
theorem inhabited_decidable [instance] (a : Prop) : inhabited (decidable a) :=
|
||||
or_elim (em a)
|
||||
(assume Ha, inhabited_intro (inl Ha))
|
||||
(assume Hna, inhabited_intro (inr Hna))
|
||||
|
||||
-- Note that inhabited_decidable is marked as an instance, and it is silently used
|
||||
-- for synthesizing the implicit argument in the following 'epsilon'
|
||||
theorem prop_decidable [instance] (a : Prop) : decidable a
|
||||
:= epsilon (λ d, true)
|
||||
theorem prop_decidable [instance] (a : Prop) : decidable a :=
|
||||
epsilon (λ d, true)
|
||||
|
|
|
@ -6,57 +6,56 @@ using eq_proofs bool
|
|||
|
||||
namespace set
|
||||
definition set (T : Type) := T → bool
|
||||
definition mem {T : Type} (x : T) (s : set T) := (s x) = '1
|
||||
definition mem {T : Type} (x : T) (s : set T) := (s x) = tt
|
||||
infix `∈`:50 := mem
|
||||
|
||||
section
|
||||
parameter {T : Type}
|
||||
|
||||
definition empty : set T := λx, '0
|
||||
definition empty : set T := λx, ff
|
||||
notation `∅`:max := empty
|
||||
|
||||
theorem mem_empty (x : T) : ¬ (x ∈ ∅)
|
||||
:= assume H : x ∈ ∅, absurd H b0_ne_b1
|
||||
theorem mem_empty (x : T) : ¬ (x ∈ ∅) :=
|
||||
assume H : x ∈ ∅, absurd H ff_ne_tt
|
||||
|
||||
definition univ : set T := λx, '1
|
||||
definition univ : set T := λx, tt
|
||||
|
||||
theorem mem_univ (x : T) : x ∈ univ
|
||||
:= refl _
|
||||
theorem mem_univ (x : T) : x ∈ univ := refl _
|
||||
|
||||
definition inter (A B : set T) : set T := λx, A x && B x
|
||||
infixl `∩`:70 := inter
|
||||
|
||||
theorem mem_inter (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B)
|
||||
:= iff_intro
|
||||
(assume H, and_intro (band_eq_b1_elim_left H) (band_eq_b1_elim_right H))
|
||||
(assume H,
|
||||
have e1 : A x = '1, from and_elim_left H,
|
||||
have e2 : B x = '1, from and_elim_right H,
|
||||
show A x && B x = '1, from e1⁻¹ ▸ e2⁻¹ ▸ band_b1_left '1)
|
||||
theorem mem_inter (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) :=
|
||||
iff_intro
|
||||
(assume H, and_intro (band_eq_tt_elim_left H) (band_eq_tt_elim_right H))
|
||||
(assume H,
|
||||
have e1 : A x = tt, from and_elim_left H,
|
||||
have e2 : B x = tt, from and_elim_right H,
|
||||
show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ band_tt_left tt)
|
||||
|
||||
theorem inter_comm (A B : set T) : A ∩ B = B ∩ A
|
||||
:= funext (λx, band_comm (A x) (B x))
|
||||
theorem inter_comm (A B : set T) : A ∩ B = B ∩ A :=
|
||||
funext (λx, band_comm (A x) (B x))
|
||||
|
||||
theorem inter_assoc (A B C : set T) : (A ∩ B) ∩ C = A ∩ (B ∩ C)
|
||||
:= funext (λx, band_assoc (A x) (B x) (C x))
|
||||
theorem inter_assoc (A B C : set T) : (A ∩ B) ∩ C = A ∩ (B ∩ C) :=
|
||||
funext (λx, band_assoc (A x) (B x) (C x))
|
||||
|
||||
definition union (A B : set T) : set T := λx, A x || B x
|
||||
infixl `∪`:65 := union
|
||||
|
||||
theorem mem_union (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B)
|
||||
:= iff_intro
|
||||
(assume H, bor_to_or H)
|
||||
(assume H, or_elim H
|
||||
(assume Ha : A x = '1,
|
||||
show A x || B x = '1, from Ha⁻¹ ▸ bor_b1_left (B x))
|
||||
(assume Hb : B x = '1,
|
||||
show A x || B x = '1, from Hb⁻¹ ▸ bor_b1_right (A x)))
|
||||
theorem mem_union (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) :=
|
||||
iff_intro
|
||||
(assume H, bor_to_or H)
|
||||
(assume H, or_elim H
|
||||
(assume Ha : A x = tt,
|
||||
show A x || B x = tt, from Ha⁻¹ ▸ bor_tt_left (B x))
|
||||
(assume Hb : B x = tt,
|
||||
show A x || B x = tt, from Hb⁻¹ ▸ bor_tt_right (A x)))
|
||||
|
||||
theorem union_comm (A B : set T) : A ∪ B = B ∪ A
|
||||
:= funext (λx, bor_comm (A x) (B x))
|
||||
theorem union_comm (A B : set T) : A ∪ B = B ∪ A :=
|
||||
funext (λx, bor_comm (A x) (B x))
|
||||
|
||||
theorem union_assoc (A B C : set T) : (A ∪ B) ∪ C = A ∪ (B ∪ C)
|
||||
:= funext (λx, bor_assoc (A x) (B x) (C x))
|
||||
theorem union_assoc (A B C : set T) : (A ∪ B) ∪ C = A ∪ (B ∪ C) :=
|
||||
funext (λx, bor_assoc (A x) (B x) (C x))
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
@ -12,9 +12,9 @@ inductive string : Type :=
|
|||
| empty : string
|
||||
| str : char → string → string
|
||||
|
||||
theorem inhabited_char [instance] : inhabited char
|
||||
:= inhabited_intro (ascii b0 b0 b0 b0 b0 b0 b0 b0)
|
||||
theorem inhabited_char [instance] : inhabited char :=
|
||||
inhabited_intro (ascii ff ff ff ff ff ff ff ff)
|
||||
|
||||
theorem inhabited_string [instance] : inhabited string
|
||||
:= inhabited_intro empty
|
||||
theorem inhabited_string [instance] : inhabited string :=
|
||||
inhabited_intro empty
|
||||
end
|
||||
|
|
|
@ -10,6 +10,6 @@ inductive sum (A : Type) (B : Type) : Type :=
|
|||
|
||||
infixr `+`:25 := sum
|
||||
|
||||
theorem induction_on {A : Type} {B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C
|
||||
:= sum_rec H1 H2 s
|
||||
theorem induction_on {A : Type} {B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
|
||||
sum_rec H1 H2 s
|
||||
end
|
|
@ -10,13 +10,12 @@ inductive unit : Type :=
|
|||
|
||||
notation `⋆`:max := star
|
||||
|
||||
theorem unit_eq (a b : unit) : a = b
|
||||
:= unit_rec (unit_rec (refl ⋆) b) a
|
||||
theorem unit_eq (a b : unit) : a = b :=
|
||||
unit_rec (unit_rec (refl ⋆) b) a
|
||||
|
||||
theorem inhabited_unit [instance] : inhabited unit
|
||||
:= inhabited_intro ⋆
|
||||
theorem inhabited_unit [instance] : inhabited unit :=
|
||||
inhabited_intro ⋆
|
||||
|
||||
using decidable
|
||||
theorem decidable_eq [instance] (a b : unit) : decidable (a = b)
|
||||
:= inl (unit_eq a b)
|
||||
theorem decidable_eq [instance] (a b : unit) : decidable (a = b) :=
|
||||
inl (unit_eq a b)
|
||||
end
|
|
@ -6,25 +6,26 @@ import logic classical
|
|||
-- Well-founded relation definition
|
||||
-- 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 → Prop) : Prop
|
||||
:= ∀P, (∃w, P w) → ∃min, P min ∧ ∀b, R b min → ¬P b
|
||||
definition wf {A : Type} (R : A → A → Prop) : Prop :=
|
||||
∀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 → Prop} {P : A → Prop} (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,
|
||||
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
|
||||
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,
|
||||
absurd s2 s3)
|
||||
: ∀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,
|
||||
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
|
||||
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,
|
||||
absurd s2 s3)
|
||||
|
||||
|
|
|
@ -15,8 +15,8 @@ static name g_string_macro("string_macro");
|
|||
static std::string g_string_opcode("Str");
|
||||
|
||||
static expr g_bool(Const(name("bool", "bool")));
|
||||
static expr g_b0(Const(name("bool", "b0")));
|
||||
static expr g_b1(Const(name("bool", "b1")));
|
||||
static expr g_ff(Const(name("bool", "ff")));
|
||||
static expr g_tt(Const(name("bool", "tt")));
|
||||
static expr g_char(Const(name("string", "char")));
|
||||
static expr g_ascii(Const(name("string", "ascii")));
|
||||
static expr g_string(Const(name("string", "string")));
|
||||
|
@ -101,8 +101,8 @@ bool has_string_decls(environment const & env) {
|
|||
try {
|
||||
type_checker tc(env);
|
||||
return
|
||||
tc.infer(g_b0) == g_bool &&
|
||||
tc.infer(g_b1) == g_bool &&
|
||||
tc.infer(g_ff) == g_bool &&
|
||||
tc.infer(g_tt) == g_bool &&
|
||||
tc.infer(g_ascii) == g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> (g_bool >> g_char))))))) &&
|
||||
tc.infer(g_empty) == g_string &&
|
||||
tc.infer(g_str) == g_char >> (g_string >> g_string);
|
||||
|
@ -115,13 +115,13 @@ expr from_char(unsigned char c) {
|
|||
buffer<expr> bits;
|
||||
while (c != 0) {
|
||||
if (c % 2 == 1)
|
||||
bits.push_back(g_b1);
|
||||
bits.push_back(g_tt);
|
||||
else
|
||||
bits.push_back(g_b0);
|
||||
bits.push_back(g_ff);
|
||||
c /= 2;
|
||||
}
|
||||
while (bits.size() < 8)
|
||||
bits.push_back(g_b0);
|
||||
bits.push_back(g_ff);
|
||||
return mk_rev_app(g_ascii, bits.size(), bits.data());
|
||||
}
|
||||
|
||||
|
@ -142,9 +142,9 @@ bool to_char_core(expr const & e, buffer<char> & tmp) {
|
|||
unsigned v = 0;
|
||||
for (unsigned i = 0; i < args.size(); i++) {
|
||||
v *= 2;
|
||||
if (args[i] == g_b1)
|
||||
if (args[i] == g_tt)
|
||||
v++;
|
||||
else if (args[i] != g_b0)
|
||||
else if (args[i] != g_ff)
|
||||
return false;
|
||||
}
|
||||
tmp.push_back(v);
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
import standard
|
||||
using bool
|
||||
|
||||
check '0
|
||||
check ff
|
|
@ -4,4 +4,4 @@ using bool unit decidable
|
|||
variables a b c : bool
|
||||
variables u v : unit
|
||||
set_option pp.implicit true
|
||||
check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = '1 ↔ true) then a else b
|
||||
check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = tt ↔ true) then a else b
|
||||
|
|
|
@ -13,11 +13,11 @@ check num → num ⟨is_typeof⟩ id
|
|||
variable h : num → bool → num
|
||||
|
||||
check flip h
|
||||
check flip h '0 zero
|
||||
check flip h ff zero
|
||||
|
||||
check typeof flip h '0 zero : num
|
||||
check typeof flip h ff zero : num
|
||||
|
||||
variable f1 : num → num → bool
|
||||
variable f2 : bool → num
|
||||
|
||||
check (f1 on f2) '0 '1
|
||||
check (f1 on f2) ff tt
|
||||
|
|
|
@ -2,6 +2,6 @@ import standard bool
|
|||
using bool
|
||||
|
||||
definition set {{T : Type}} := T → bool
|
||||
infix `∈`:50 := λx A, A x = '1
|
||||
infix `∈`:50 := λx A, A x = tt
|
||||
|
||||
check 1 ∈ (λ x, '1)
|
||||
check 1 ∈ (λ x, tt)
|
|
@ -4,15 +4,15 @@ using bool
|
|||
namespace set
|
||||
|
||||
definition set (T : Type) := T → bool
|
||||
definition mem {T : Type} (a : T) (s : set T) := s a = '1
|
||||
definition mem {T : Type} (a : T) (s : set T) := s a = tt
|
||||
infix `∈`:50 := mem
|
||||
|
||||
section
|
||||
parameter {T : Type}
|
||||
|
||||
definition empty : set T := λx, '0
|
||||
definition empty : set T := λx, ff
|
||||
notation `∅` := empty
|
||||
|
||||
theorem mem_empty (x : T) : ¬ (x ∈ ∅)
|
||||
:= not_intro (λH : x ∈ ∅, absurd H b0_ne_b1)
|
||||
:= not_intro (λH : x ∈ ∅, absurd H ff_ne_tt)
|
||||
end
|
Loading…
Reference in a new issue