chore(builtin/kernel): remove \bowtie as notation for transitivity
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
2753a0ffc0
commit
7a3aab60c6
8 changed files with 17 additions and 19 deletions
|
@ -19,8 +19,8 @@ axiom H2 : b = e
|
|||
-- Proof that (h a b) = (h c e)
|
||||
theorem T1 : (h a b) = (h c e) :=
|
||||
or_elim H1
|
||||
(λ C1, congrh ((and_eliml C1) ⋈ (and_elimr C1)) H2)
|
||||
(λ C2, congrh ((and_elimr C2) ⋈ (and_eliml C2)) H2)
|
||||
(λ C1, congrh (trans (and_eliml C1) (and_elimr C1)) H2)
|
||||
(λ C2, congrh (trans (and_elimr C2) (and_eliml C2)) H2)
|
||||
|
||||
-- We can use theorem T1 to prove other theorems
|
||||
theorem T2 : (h a (h a b)) = (h a (h c e)) :=
|
||||
|
|
|
@ -156,9 +156,6 @@ theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
|
|||
theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
|
||||
:= subst H1 H2
|
||||
|
||||
infixl 100 >< : trans
|
||||
infixl 100 ⋈ : trans
|
||||
|
||||
theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
|
||||
:= assume H1 : b = a, H (symm H1)
|
||||
|
||||
|
@ -239,13 +236,13 @@ theorem or_falsel (a : Bool) : a ∨ false ↔ a
|
|||
(assume H, or_introl H false)
|
||||
|
||||
theorem or_falser (a : Bool) : false ∨ a ↔ a
|
||||
:= (or_comm false a) ⋈ (or_falsel a)
|
||||
:= trans (or_comm false a) (or_falsel a)
|
||||
|
||||
theorem or_truel (a : Bool) : true ∨ a ↔ true
|
||||
:= eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a)
|
||||
|
||||
theorem or_truer (a : Bool) : a ∨ true ↔ true
|
||||
:= (or_comm a true) ⋈ (or_truel a)
|
||||
:= trans (or_comm a true) (or_truel a)
|
||||
|
||||
theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true
|
||||
:= eqt_intro (em a)
|
||||
|
@ -274,7 +271,7 @@ theorem and_falsel (a : Bool) : a ∧ false ↔ false
|
|||
(assume H, false_elim (a ∧ false) H)
|
||||
|
||||
theorem and_falser (a : Bool) : false ∧ a ↔ false
|
||||
:= (and_comm false a) ⋈ (and_falsel a)
|
||||
:= trans (and_comm false a) (and_falsel a)
|
||||
|
||||
theorem and_absurd (a : Bool) : a ∧ ¬ a ↔ false
|
||||
:= boolext (assume H, absurd (and_eliml H) (and_elimr H))
|
||||
|
|
Binary file not shown.
|
@ -9,7 +9,8 @@
|
|||
Assumed: H
|
||||
Assumed: a
|
||||
eta (F2 a) : (λ x : B, F2 a x) = F2 a
|
||||
funext (λ a : A, symm (eta (F1 a)) ⋈ (funext (λ b : B, H a b) ⋈ eta (F2 a))) : (λ x : A, F1 x) = (λ x : A, F2 x)
|
||||
funext (λ a : A, trans (symm (eta (F1 a))) (trans (funext (λ b : B, H a b)) (eta (F2 a)))) :
|
||||
(λ x : A, F1 x) = (λ x : A, F2 x)
|
||||
funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) = (λ (x : A) (x::1 : B), F2 x x::1)
|
||||
Proved: T1
|
||||
Proved: T2
|
||||
|
|
|
@ -9,6 +9,6 @@ theorem Comm2 : ∀ n m : ℕ, n + m = m + n :=
|
|||
λ n : ℕ,
|
||||
Induction
|
||||
(λ x : ℕ, n + x = x + n)
|
||||
(Nat::add_zeror n ⋈ symm (Nat::add_zerol n))
|
||||
(trans (Nat::add_zeror n) (symm (Nat::add_zerol n)))
|
||||
(λ (m : ℕ) (iH : n + m = m + n),
|
||||
Nat::add_succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add_succl m n))
|
||||
trans (trans (Nat::add_succr n m) (subst (refl (n + m + 1)) iH)) (symm (Nat::add_succl m n)))
|
||||
|
|
|
@ -9,7 +9,7 @@ Failed to solve
|
|||
Induction
|
||||
with arguments:
|
||||
?M::3
|
||||
λ m : ℕ, Nat::add_zerol m ⋈ symm (Nat::add_zeror m)
|
||||
λ m : ℕ, trans (Nat::add_zerol m) (symm (Nat::add_zeror m))
|
||||
λ (n : ℕ) (iH : (?M::3[lift:0:1]) n) (m : ℕ),
|
||||
@trans ℕ
|
||||
(n + 1 + m)
|
||||
|
|
|
@ -15,7 +15,7 @@ definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x
|
|||
theorem f_eq_g (A : Type) (f : A → A → A) (H1 : ∀ x y : A, f x y = f y x) : f = g A f :=
|
||||
funext (λ x : A,
|
||||
funext (λ y : A,
|
||||
let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := refl (g A f x y) in L1 ⋈ L2))
|
||||
let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := refl (g A f x y) in trans L1 L2))
|
||||
theorem Inj (A B : Type)
|
||||
(h : A → B)
|
||||
(hinv : B → A)
|
||||
|
@ -26,6 +26,6 @@ theorem Inj (A B : Type)
|
|||
L2 : hinv (h x) = x := Inv x,
|
||||
L3 : hinv (h y) = y := Inv y,
|
||||
L4 : x = hinv (h x) := symm L2,
|
||||
L5 : x = hinv (h y) := L4 ⋈ L1
|
||||
in L5 ⋈ L3
|
||||
L5 : x = hinv (h y) := trans L4 L1
|
||||
in trans L5 L3
|
||||
10
|
||||
|
|
|
@ -56,12 +56,12 @@ theorem Example2 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @e
|
|||
Set: lean::pp::implicit
|
||||
theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a b = h c b :=
|
||||
or_elim H
|
||||
(λ H1 : a = b ∧ b = e ∧ b = c, congrH (and_eliml H1 ⋈ and_elimr (and_elimr H1)) (refl b))
|
||||
(λ H1 : a = d ∧ d = c, congrH (and_eliml H1 ⋈ and_elimr H1) (refl b))
|
||||
(λ H1 : a = b ∧ b = e ∧ b = c, congrH (trans (and_eliml H1) (and_elimr (and_elimr H1))) (refl b))
|
||||
(λ H1 : a = d ∧ d = c, congrH (trans (and_eliml H1) (and_elimr H1)) (refl b))
|
||||
Proved: Example4
|
||||
Set: lean::pp::implicit
|
||||
theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a c = h c a :=
|
||||
or_elim H
|
||||
(λ H1 : a = b ∧ b = e ∧ b = c,
|
||||
let AeqC := and_eliml H1 ⋈ and_elimr (and_elimr H1) in congrH AeqC (symm AeqC))
|
||||
(λ H1 : a = d ∧ d = c, let AeqC := and_eliml H1 ⋈ and_elimr H1 in congrH AeqC (symm AeqC))
|
||||
let AeqC := trans (and_eliml H1) (and_elimr (and_elimr H1)) in congrH AeqC (symm AeqC))
|
||||
(λ H1 : a = d ∧ d = c, let AeqC := trans (and_eliml H1) (and_elimr H1) in congrH AeqC (symm AeqC))
|
||||
|
|
Loading…
Reference in a new issue