From 1da429479367b123b003f9fb89d3cdf89ac3e331 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Jan 2014 09:00:01 -0800 Subject: [PATCH] refactor(builtin): more theorems, fix iff notation Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 2 +- src/builtin/cast.lean | 13 +++- src/builtin/kernel.lean | 136 +++++++++++++++++++---------------- src/builtin/obj/cast.olean | Bin 2666 -> 3585 bytes src/builtin/obj/kernel.olean | Bin 25543 -> 26378 bytes src/kernel/kernel_decls.cpp | 3 + src/kernel/kernel_decls.h | 9 +++ 7 files changed, 98 insertions(+), 65 deletions(-) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index e2408ba85..f1c042d0c 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -36,7 +36,7 @@ axiom add_zeror (a : Nat) : a + 0 = a axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1 axiom mul_zeror (a : Nat) : a * 0 = 0 axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a -axiom le_def (a b : Nat) : a ≤ b ⟷ ∃ c, a + c = b +axiom le_def (a b : Nat) : a ≤ b ↔ ∃ c, a + c = b axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index f89d052a0..e95a68624 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -45,7 +45,7 @@ theorem hcongr L3 : b == b' := cast_eq L2 b, L4 : a == b' := htrans H2 L3, L5 : f a == f b' := congr2 f L4, - S1 : (∀ x, B' x) == (∀ x, B x) := symm (type_eq H1), + S1 : (∀ x, B' x) == (∀ x, B x) := symm (type_eq H1), g' : (∀ x, B x) := cast S1 g, L6 : g == g' := cast_eq S1 g, L7 : f == g' := htrans H1 L6, @@ -54,6 +54,17 @@ theorem hcongr L10 : g' b' == g b := cast_app S1 L2 g b in htrans L9 L10 +theorem hfunext + {A : TypeM} {B B' : A → TypeM} {f : ∀ x : A, B x} {g : ∀ x : A, B' x} (H : ∀ x : A, f x == g x) : f == g +:= let L1 : (∀ x : A, B x = B' x) := λ x : A, type_eq (H x), + L2 : (∀ x : A, B x) = (∀ x : A, B' x) := allext L1, + g' : (∀ x : A, B x) := cast (symm L2) g, + Hgg : g == g' := cast_eq (symm L2) g, + Hggx : (∀ x : A, g x == g' x) := λ x : A, hcongr Hgg (refl x) , + L3 : (∀ x : A, f x == g' x) := λ x : A, htrans (H x) (Hggx x), + Hfg : f == g' := funext L3 + in htrans Hfg (hsymm Hgg) + exit -- Stop here, the following axiom is not sound -- The following axiom is unsound when we treat Pi and diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 8fb67f3c1..a524307ce 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -30,7 +30,7 @@ definition implies (a b : Bool) := a → b definition iff (a b : Bool) := a == b infixr 25 <-> : iff -infixr 25 ⟷ : iff +infixr 25 ↔ : iff -- The Lean parser has special treatment for the constant exists. -- It allows us to write @@ -103,8 +103,8 @@ theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c := assume Ha, H2 (H1 ◂ Ha) -theorem not_not_eq (a : Bool) : ¬ ¬ a ⟷ a -:= case (λ x, ¬ ¬ x ⟷ x) trivial trivial a +theorem not_not_eq (a : Bool) : ¬ ¬ a ↔ a +:= case (λ x, ¬ ¬ x ↔ x) trivial trivial a theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a := (not_not_eq a) ◂ H @@ -174,6 +174,16 @@ theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := subst H1 H2 +theorem heq_congr {A : TypeU} {a b c d : A} (H1 : a == c) (H2 : b == d) : (a == b) = (c == d) +:= calc (a == b) = (c == b) : { H1 } + ... = (c == d) : { H2 } + +theorem heq_congrl {A : TypeU} {a : A} (b : A) {c : A} (H : a == c) : (a == b) = (c == b) +:= heq_congr H (refl b) + +theorem heq_congrr {A : TypeU} (a : A) {b d : A} (H : b == d) : (a == b) = (a == d) +:= heq_congr (refl a) H + theorem eqt_elim {a : Bool} (H : a = true) : a := (symm H) ◂ trivial @@ -228,14 +238,14 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false := boolext (assume H1 : a, absurd H1 H) (assume H2 : false, false_elim a H2) -theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ⟷ false +theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false := eqf_intro H -theorem or_comm (a b : Bool) : a ∨ b ⟷ b ∨ a +theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a)) (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b)) -theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ⟷ a ∨ (b ∨ c) +theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := boolext (assume H : (a ∨ b) ∨ c, or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c)) (λ Hb : b, or_intror a (or_introl Hb c))) @@ -245,118 +255,118 @@ theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ⟷ a ∨ (b ∨ c) (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c) (λ Hc : c, or_intror (a ∨ b) Hc))) -theorem or_id (a : Bool) : a ∨ a ⟷ a +theorem or_id (a : Bool) : a ∨ a ↔ a := boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2)) (assume H, or_introl H a) -theorem or_falsel (a : Bool) : a ∨ false ⟷ a +theorem or_falsel (a : Bool) : a ∨ false ↔ a := boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2)) (assume H, or_introl H false) -theorem or_falser (a : Bool) : false ∨ a ⟷ a +theorem or_falser (a : Bool) : false ∨ a ↔ a := (or_comm false a) ⋈ (or_falsel a) -theorem or_truel (a : Bool) : true ∨ a ⟷ true +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 +theorem or_truer (a : Bool) : a ∨ true ↔ true := (or_comm a true) ⋈ (or_truel a) -theorem or_tauto (a : Bool) : a ∨ ¬ a ⟷ true +theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true := eqt_intro (em a) -theorem and_comm (a b : Bool) : a ∧ b ⟷ b ∧ a +theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a := boolext (assume H, and_intro (and_elimr H) (and_eliml H)) (assume H, and_intro (and_elimr H) (and_eliml H)) -theorem and_id (a : Bool) : a ∧ a ⟷ a +theorem and_id (a : Bool) : a ∧ a ↔ a := boolext (assume H, and_eliml H) (assume H, and_intro H H) -theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ⟷ a ∧ (b ∧ c) +theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := boolext (assume H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H))) (assume H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H))) -theorem and_truer (a : Bool) : a ∧ true ⟷ a +theorem and_truer (a : Bool) : a ∧ true ↔ a := boolext (assume H : a ∧ true, and_eliml H) (assume H : a, and_intro H trivial) -theorem and_truel (a : Bool) : true ∧ a ⟷ a +theorem and_truel (a : Bool) : true ∧ a ↔ a := trans (and_comm true a) (and_truer a) -theorem and_falsel (a : Bool) : a ∧ false ⟷ false +theorem and_falsel (a : Bool) : a ∧ false ↔ false := boolext (assume H, and_elimr H) (assume H, false_elim (a ∧ false) H) -theorem and_falser (a : Bool) : false ∧ a ⟷ false +theorem and_falser (a : Bool) : false ∧ a ↔ false := (and_comm false a) ⋈ (and_falsel a) -theorem and_absurd (a : Bool) : a ∧ ¬ a ⟷ false +theorem and_absurd (a : Bool) : a ∧ ¬ a ↔ false := boolext (assume H, absurd (and_eliml H) (and_elimr H)) (assume H, false_elim (a ∧ ¬ a) H) -theorem imp_truer (a : Bool) : (a → true) ⟷ true -:= case (λ x, (x → true) ⟷ true) trivial trivial a +theorem imp_truer (a : Bool) : (a → true) ↔ true +:= case (λ x, (x → true) ↔ true) trivial trivial a -theorem imp_truel (a : Bool) : (true → a) ⟷ a -:= case (λ x, (true → x) ⟷ x) trivial trivial a +theorem imp_truel (a : Bool) : (true → a) ↔ a +:= case (λ x, (true → x) ↔ x) trivial trivial a -theorem imp_falser (a : Bool) : (a → false) ⟷ ¬ a +theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a := refl _ -theorem imp_falsel (a : Bool) : (false → a) ⟷ true -:= case (λ x, (false → x) ⟷ true) trivial trivial a +theorem imp_falsel (a : Bool) : (false → a) ↔ true +:= case (λ x, (false → x) ↔ true) trivial trivial a -theorem not_and (a b : Bool) : ¬ (a ∧ b) ⟷ ¬ a ∨ ¬ b -:= case (λ x, ¬ (x ∧ b) ⟷ ¬ x ∨ ¬ b) - (case (λ y, ¬ (true ∧ y) ⟷ ¬ true ∨ ¬ y) trivial trivial b) - (case (λ y, ¬ (false ∧ y) ⟷ ¬ false ∨ ¬ y) trivial trivial b) +theorem not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b +:= case (λ x, ¬ (x ∧ b) ↔ ¬ x ∨ ¬ b) + (case (λ y, ¬ (true ∧ y) ↔ ¬ true ∨ ¬ y) trivial trivial b) + (case (λ y, ¬ (false ∧ y) ↔ ¬ false ∨ ¬ y) trivial trivial b) a theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b := (not_and a b) ◂ H -theorem not_or (a b : Bool) : ¬ (a ∨ b) ⟷ ¬ a ∧ ¬ b -:= case (λ x, ¬ (x ∨ b) ⟷ ¬ x ∧ ¬ b) - (case (λ y, ¬ (true ∨ y) ⟷ ¬ true ∧ ¬ y) trivial trivial b) - (case (λ y, ¬ (false ∨ y) ⟷ ¬ false ∧ ¬ y) trivial trivial b) +theorem not_or (a b : Bool) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b +:= case (λ x, ¬ (x ∨ b) ↔ ¬ x ∧ ¬ b) + (case (λ y, ¬ (true ∨ y) ↔ ¬ true ∧ ¬ y) trivial trivial b) + (case (λ y, ¬ (false ∨ y) ↔ ¬ false ∧ ¬ y) trivial trivial b) a theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b := (not_or a b) ◂ H -theorem not_iff (a b : Bool) : ¬ (a ⟷ b) ⟷ (¬ a ⟷ b) -:= case (λ x, ¬ (x ⟷ b) ⟷ ((¬ x) ⟷ b)) - (case (λ y, ¬ (true ⟷ y) ⟷ ((¬ true) ⟷ y)) trivial trivial b) - (case (λ y, ¬ (false ⟷ y) ⟷ ((¬ false) ⟷ y)) trivial trivial b) +theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b) +:= case (λ x, ¬ (x ↔ b) ↔ ((¬ x) ↔ b)) + (case (λ y, ¬ (true ↔ y) ↔ ((¬ true) ↔ y)) trivial trivial b) + (case (λ y, ¬ (false ↔ y) ↔ ((¬ false) ↔ y)) trivial trivial b) a -theorem not_iff_elim {a b : Bool} (H : ¬ (a ⟷ b)) : (¬ a) ⟷ b +theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b := (not_iff a b) ◂ H -theorem not_implies (a b : Bool) : ¬ (a → b) ⟷ a ∧ ¬ b -:= case (λ x, ¬ (x → b) ⟷ x ∧ ¬ b) - (case (λ y, ¬ (true → y) ⟷ true ∧ ¬ y) trivial trivial b) - (case (λ y, ¬ (false → y) ⟷ false ∧ ¬ y) trivial trivial b) +theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b +:= case (λ x, ¬ (x → b) ↔ x ∧ ¬ b) + (case (λ y, ¬ (true → y) ↔ true ∧ ¬ y) trivial trivial b) + (case (λ y, ¬ (false → y) ↔ false ∧ ¬ y) trivial trivial b) a theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b := (not_implies a b) ◂ H -theorem not_congr {a b : Bool} (H : a ⟷ b) : ¬ a ⟷ ¬ b +theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b := congr2 not H -theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ⟷ Q x) : (∃ x : A, P x) ⟷ (∃ x : A, Q x) +theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ↔ Q x) : (∃ x : A, P x) ↔ (∃ x : A, Q x) := congr2 (Exists A) (funext H) -theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ⟷ (∃ x : A, ¬ P x) +theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ (∃ x : A, ¬ P x) := calc (¬ ∀ x : A, P x) = ¬ ∀ x : A, ¬ ¬ P x : not_congr (allext (λ x : A, symm (not_not_eq (P x)))) ... = ∃ x : A, ¬ P x : refl (∃ x : A, ¬ P x) theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x := (not_forall A P) ◂ H -theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ⟷ (∀ x : A, ¬ P x) +theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ↔ (∀ x : A, ¬ P x) := calc (¬ ∃ x : A, P x) = ¬ ¬ ∀ x : A, ¬ P x : refl (¬ ∃ x : A, P x) ... = ∀ x : A, ¬ P x : not_not_eq (∀ x : A, ¬ P x) @@ -378,7 +388,7 @@ theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x (λ (w : A) (Hw : w ≠ a ∧ P w), exists_intro w (and_elimr Hw))) -theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ⟷ (P a ∨ (∃ x : A, x ≠ a ∧ P x)) +theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ↔ (P a ∨ (∃ x : A, x ≠ a ∧ P x)) := boolext (assume H : (∃ x : A, P x), exists_unfold1 a H) (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H) @@ -390,10 +400,10 @@ theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) ... = R (R y x) z : { comm x y } ... = R y (R x z) : assoc y x z -theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ⟷ b ∧ (a ∧ c) +theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := left_comm and_comm and_assoc a b c -theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ⟷ b ∨ (a ∨ c) +theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) := left_comm or_comm or_assoc a b c -- Congruence theorems for contextual simplification @@ -463,24 +473,24 @@ theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) := imp_congrr (λ H, H_ac) H_bd -- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b -theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ⟷ c ∨ d +theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d := imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd -theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : a ∨ b ⟷ c ∨ d +theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : a ∨ b ↔ c ∨ d := imp_congrl (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) H_bd -- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true -theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ⟷ c ∨ d +theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ↔ c ∨ d := or_congrr (λ H, H_ac) H_bd -- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b) -theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ⟷ c ∧ d +theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d := congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c))) -theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : a ∧ b ⟷ c ∧ d +theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : a ∧ b ↔ c ∧ d := congr2 not (imp_congrl (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)) (λ H_a : a, congr2 not (H_bd H_a))) -- (Common case) simplify a to c, and then b to d using the fact that c is true -theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ⟷ c ∧ d +theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d := and_congrr (λ H, H_ac) H_bd -theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ⟷ p ∨ ∀ x, φ x +theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ↔ p ∨ ∀ x, φ x := boolext (assume H : (∀ x, p ∨ φ x), or_elim (em p) @@ -493,19 +503,19 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, (λ H1 : p, or_introl H1 (φ x)) (λ H2 : (∀ x, φ x), or_intror p (H2 x))) -theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ⟷ (∀ x, φ x) ∨ p +theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ↔ (∀ x, φ x) ∨ p := calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x) : allext (λ x, or_comm (φ x) p) ... = (p ∨ ∀ x, φ x) : forall_or_distributer p φ ... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x) -theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ⟷ (∀ x, φ x) ∧ (∀ x, ψ x) +theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x) := boolext (assume H : (∀ x, φ x ∧ ψ x), and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x))) (assume H : (∀ x, φ x) ∧ (∀ x, ψ x), take x, and_intro (and_eliml H x) (and_elimr H x)) -theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ⟷ p ∧ ∃ x, φ x +theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ↔ p ∧ ∃ x, φ x := boolext (assume H : (∃ x, p ∧ φ x), obtain (w : A) (Hw : p ∧ φ w), from H, @@ -514,12 +524,12 @@ theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x obtain (w : A) (Hw : φ w), from (and_elimr H), exists_intro w (and_intro (and_eliml H) Hw)) -theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ⟷ (∃ x, φ x) ∧ p +theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p := calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p) ... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ ... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x) -theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ⟷ (∃ x, φ x) ∨ (∃ x, ψ x) +theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x) := boolext (assume H : (∃ x, φ x ∨ ψ x), obtain (w : A) (Hw : φ w ∨ ψ w), from H, diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index e5d578d430534b9c384583df867269d1e5710373..3712292705c70fdad4189342efa5778892fab4e9 100644 GIT binary patch delta 942 zcmZ8fO-lk%6us|~QMMv{bjb**TwLp4rL~MMzi*zP3d8; zK6_COd&Q*@WR?)mE`h_^-T16McH!cM=$5?$p6ncHG9bh|57?{+RTovpGMATHX3!kW zo&?rlei&)L#&JB#0HYYzoJ6Ax_L2St$2wqb&KNhfrc3}npk%kJMVI3}Tu*iOcSk@V z!+7Q)CmBNL%wYn}uq!XzgfL?0h&~HuJNgum%qDbRgc+=(9&6HNc9>%!Cv-B*y?T5? RqTJbE!r)!BtC!7|FaH=_P}~3j delta 16 XcmZpac_p$TiHpNEFU2i0CzSyJF-Qeh diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index a9ec67ca9a94c4a2fe6081ebc62e7fd97a11ccf5..b8ea3249b6aea200f2b36c4de9c3aa63bcfa5efc 100644 GIT binary patch literal 26378 zcmcIt36xz`m3{C1|9%yQ3W#VDpdlJ6Buy(xP=akR1rD7AL5U>xfX1q%Dk-T{g{n#j zlLH_GkY-d+5J8d1YNIx&XwxkrDkwrbBHid}LKMf~)Hag>efHjW`mcUfl3uH`7B}bJ zd+xbsy62ud{4g}o+dbIVKhT@GKl%E>{tdmuBfVL%EX#ANwW8=58qGFz4`;=3Lqh{u z8>+3LXMO*`X#ZeV8y#NXn}x5w?g8t*s<$sIPCjE@?=r)8bl9y8WsS{)Mz&FOXNBmp zxh(OQ3bb*oq7c#S#G%pd(f*-9;N-=&Pvh@wR)MmvA%})Z5;Y{!U^$83WzmDbvl4`7 z0GdS30ChBzKKtyfX0->C^b0EEo^pg5(Qm)zemgdODruvX-Gi%unC)HKsQ6O`KEwmK z!JiHklbh+yoJn#s$j1vSd>nC#8qse`bH5#%HYaW5qkrwXf&ShRAh+VBiHi>P=<6E~ zyB!T=xUG5M1uuUs2cAZb52|py+-Z!{NFNx7csbh|&Krm)w>yj&q&^E^8^PHCiFM%Owd?Sa z&9wjWyjk*N=&SQ6#7sHkVDD)}KfE;Q@aGWk18v?19LJq#Jp$gy{^H$_cDPknN854H zjmdb2XQOMfqIYf3TX`r5?uVjHIw44T<^nV)Tr?=Zo6n~1jajj>+h#7*k3Wq@v1qQQ zNn25Hj$7NJd8#6Z?OvJX46t59w>A(O?(G|Bp>jzHED1<_FXgN4E6>q;WPQ&FB7@VJ zA0%2V^^iFrVlz7MitjmOG%B@@%7tv9HrQ#QA9;Z_)N}iT!TZ(^_HJw%{WxPqnxZ$F z2lZKvb2!kP(I{4D4M2-g%!xx7%Zmc;LQa}xK$$_1Ty%IYUT^h*i|&DeFYWiB{hdaTj)l6nM4i&x*^s}WCxN7M$>Ak~hBvkKcx6uhcbR2M@KgG0@qc1M^JW_i!o+f?|dMMbeWM_`gXnyixoTspv z8JzWRCy0V3-T=s^xhyf~P~yYKUHc5rF)JH6R}ig1&x6Mc?A z!7*gbFgjHzeXJ!8k+@!qks;K6fVFhEIkQlKp+!%Vl;tCWZ2&e;8``4~p zF*@8mi1pNolUR>V?97NRmj<&LBy=}v(RwBd4SiMw&yFB{^HQ?;Zq#0C!N5_WchNOM zyg9=#{6q(vy{GLlrxo?n*Eq;6Wa8Y&+IbN?KZ5TED26Wpcza}+YP|-P(g2`l{@-Uc zo`2(g&oq5I=xrvK7Xg%7FOJ|P5&Qr^u%`JuMyruk&TsNdRfHJ0$q0B>5mWJ>Wg_0j z^6-OcBPPa50Lb0tx@Jt`wc0WOr4pD>H8ps&0vyF#NXb6LE(B?3v2!hZvG&6NCkK~U*vWaz$fVSP zVLb$(4;r=$+bf4`(du3|q}=+ye2y3Md?O0t*;E4tdk9WetN<0CnE;~C1w&qEHEs+= z{xJbV#FYN9KNS!aOUF<=z6tG;`r{G&1ba~dHv`&ZszVrtCmsV z2%OXA2*~>s1)A(L*xlo{T%a};h1j|UpxD|R!A}8vO1!}MhP_v@rh7y0ir$UuhO<0M zxDz_nfIG#msX*W4S=Rq2kXR_4-v~IF=UP}$*DT*Bt;T6T6)@RgCb3lpehO5SrfdNy zxjqxY&jNhPSeD^BqJp2Z%7ksQ5}fVR*2}Rn+&eNfu%UNuYc0lyHefbsR60cF0xKj{NX0j4al+M(}O}^O*_-@CWll z6pUA4ntsJ|{yRIErz+*un&F52mNkZ9t7%mjeI-b^3@A<%3edsG>0=kA!!Ghj z_IM7ZBFT3FilOgC@cR+`fr0sA>hwW?O9(y$gy*77ZDS-2B(A+=FCg8Tqg=uW*OAop zD|+3=9aaN4T>lq3ln@c~r8Lsd3?W|%v?V^W=(7uTjCs|<>+(B>;PVID$*)hdV;IgW zX+9{mqmVcM2%uE+V}tTl+7p7Dp`eh>w9ZrO*3;Wl6Eb{GrmlXEUc?MB>0zsprAN+K zi|qMW;Iul}@lH0k69`P^6R)LN9%Wa8I{?b-e*#c4{S@HbSt!?_kYfN+J2xo{;{Z&@ zsMv)RfJt)f6k^79qu_PyGxiAtk>kQ4=Vo!RNLSt)TVhtIC5FP&U(`a0;UaE-`*VO2 z{uclx+%ExYO8&~A{2X@sHNbaAmBGzyd*b~Ry6XKH z{M{%%R$7_;359gPRa8277PZm=gSvF^yjA9(L$@65yXoCg2jhA7Ge#_kyT*jIt-@-o zhr1)}DzK6*Rnlrm(yObVLDO+Bk7xj?W08$Tm9U%3PQ(MAqpmrhk z0JG*>34&t2br#CYtl&XSes>%PE}3sbJ7Z)r;Ylik+vH0t+&U~$p$qlLc*#-k2EC37 z)g*egq^h~tPpZUit58Lrkog&!!`dZIet8TU4AkoE+UGE){}_z5`f=*FCGr{7d>eUS z^pS2~fRSZ~NdRSsy#dM&2`<*jeEV#ejy$H@6^{apG*oO3hT6w^ z)lC)((|ekoXIPRS5|NNjUJL5d=1TxF8OfRNUyIK_w$K}I@M?Uq zwfSND#u?Tf9RPD0Xld930Df3|*mnRn&io#aql+8bGdfEUd8&2LzziDL@P(*x9LdGQ zY+OL#&vKudA!@ip!5{xCqoi&rq5Mb&=9^71 z2e_QzO968F=Pxs;=uj@W+@#ourmUaTW8joKl*Jk}76)|VuOlLkE>*}PIa(atrNCq< z;2?2cA7mdP?oxg8TB@%by%17+2$SYA7(u!9VZfC>W&xBw;O5Q; z{}P~Z4+q#y)%=w~T44&<*roA+=J+GGeho`WDf2RkOAc58brobFI1C)RS?HEBOTv>| zxs0^1ge#5=fKlkjGLN;mTm;LGLbx164AY!s?I4N@EToU-3=hz66kEztd>ri_s z!Pf(n&%FVleC~|~6@x@r1km}Mff}shZAofFPbwB0X68H&>XGZn8^<^pnolAQ29*24 zALW#ky@jWNOyX&JMB!H_ij58NTR<_J-Y8@R9TRIodMTUazMR!w7p#4c4q zF64E`qiH&8-vm(W9l74b+7qp^xL6}S3=D)e9!6w4JMsC5A5O~v5~5-nyArD(u`K%; zYXRX11AiCO7zfD}V=^Z#p*emMLi=IY#m6P#+;Xg9x{G%>8gn%Mb0ZzfUjD)D?K;|Tx5-Y5-*n-fSuO_z)+>uQ6=96Ny1AUtgb4Cod zA(7vV0xE77F@h*Q5A2xu6<;*eo)q;mv~xuIJmVH!u9~Q^lFfFzzNm+BrT9Gk;`bHa zHG9BGa>LC2@Kpr3z-v`K%78pZJ7W8?8eKKKi8NBCX!0=;=J`Nl6 zE55-2czK@>V?eP%Kc0{1ld#bq*&vZefX~nwEGM?wgAcf7&*5p-K^)qXurXm;lQ^8u zV~39s^2NaR^>^7SEztEkwjQ zl_{xvWMpV%h_`7-UJ10!sViv8jUB!@qFu8YYW{w9Ab3FpFC-Y0Sew*91%=sZfZZra zpS4L6HIgQ`l&B;2!Kz!6&AgUti6t0F77CqFkSo=aNK^=50UDBrE`j$;Lkwx~hT4m* zSuVo`i2AKDnD$3>Qls<0Vp3T&hxi0et*~bMJFD#-4GQ`4#T8!FN1hNE6bCRNIjC_n zZkdO?EMMGA)6z){e)w!05rO4NHM0?wM@1B}d;Mtg+)@?? z0{562=i~UM(rZXlv!f9(@-+a-xjk^-^&+C{>?!PoLQB=n0JVsGlHg1$x$^Rsytdl; zM?O>cEl9dtP;^ViHr6Qm0c_Js@|9|}_sZ26p>`^o)d>^1h73ZnRuP4jOiAdls)RQ} z)^Vn8l#S}v6uA|IlPSVw8W9!swKFQ?Xm*4-5m{wJm^)GJd$KG|p>fG&qORu3d}e8U zk*1o|1WYt+}a1Ut()*wL#fbGdc&SE@odUJDZ}6y!(P7)<>9 z8^Ed>pqrXF!(g?|KvGXB;Y+AU=3wPbHaXO49+fa3T{P%j023wfJ1F5UC_zu|m>|hX zDeGjk$a7=7Ql$?Wt(7DkD5;I;F<-@)WH!6LX-T^u4V5L#Qy=4qo;ux- zvd9hZ9gq6=#-ZNYz(C#$#e7aR?jn>VoP%0aX7j!Ht$h|KH=)py_W;0FV*dyY6|wO+ z5I^$rQpVkZTmj2vhWy&S>0(w+n~2}4YqWQOh>;gKVu;YEuKHNbC7)yU67+4}F@lmwf^-cku#8waE zTddI)syXDX*u~%Ah$BlBUYW5$4;zvF_*~J!JwvK62DzIw3hs* zXcwE05%eDJ5_5HuCq)7bfO@>j0cZf-)>;5;F~ee4EwbTT1|+@RGhpcHR-5o$qb;kH zAXBg=ey!~KORG-p>VAMa zUYrD#r#KGh3r(vC`5QEe$=?#3z?7ak)y0$6jO6&etLgXMI6SSnXVWjcDR$p=c(m0L zzsKE$*;0*A^9qsw6E*Tg1fK->RBARc`lD4Rw(|FQ;{@*dq0t|b z$nZ3X%TCWk@J|NT51nOY@upDAi!LqAT%Utiaixr*`zdtuhr9OpA3qijC(Xx#Tvksm zy13KMW@CNvH!<=7PG;`AdB>A6L31}fKCwaSpLId9Rt?KIGjO<+)d@Zaa5}-~0nP?k z0IIK-v<-YvQzT8zQ1JSD&;tBAPGjpE5r*8LhZ&fig@PB8Qk42zox?|SSl<3@AO1iW z>s#N@u>F426j0TVj20Hp?Bpn`Jxx(uJt?rZ~ zUtW7#y!A1G>mMTvFN)mkPi|QIVjyful@;aT>^~a_cSvvhpkFJ!A?@|?K*3=BVBgTd zs;1{rZ(;B0ekt%5D)l?5O_JC*4sJ)%a(%tnp3;flN1<4PLJJ9?F3K?#An#v_X#nL4 zI+-BCfmT_+lRpsFH2@DHG;!}m58Kn8j=y7*Q3Aa=pahVmmBlRDncu+Tzh$DK2 zQD*`^2M$#`m5KueNi2r#lP`lDlkPIEKswOMg_@p-wQ`}LeT5vw>liaCvL?4k)DIS) z`suV4H7yrnC%F)1U{ow1RQ(U~32?hFzV9IcE8sx7(kS*N=5|y@`_OL{vZx54&jU*R zp2JYy57?em$m@0K6MaUmN4sLxDJFqM$qFB;Gsy@pjF%a7=K7xkE3`rVAw#yGE?H3< zsF;WP(0jyaaKD@tFS9PK>=PEW^ks_@l$fyB@3h|aKTyrDFwo6Z&MB#xDq%*?gJ$1B zJJR}{bTj&h?g2S(-9E!)1A8R+dB^(W+7g-n8_CXSf5i(e-N z$k`i2cOxtFSn$%WLqEo(APQ6x1by@dShmKu_3L^Z~|RsSoFwpwuXs=QIMdv^6*{ZCyK$)uY$)jF%kXwsGLpV znXe`2pd15giAYtx67nzsYI;Ei_M|t(vV@eH&`V*Ll3*22#-AR?PsH<1d88q`xrM8Y z)HCIS@$kyObJs~4^5@$59B_((>F+xelf4m5OmmCBi6AFU$=B=!7;q@c{mPgX=WMb< zmp_}4OXr_PWts^fKe3~WJ!E}vvW}&nb2&en&U8G!#c$l2Xpt&sqlx>8$f4mzqp`0Q zeD6>@p4^^~$||?E)6)+>lFPkt?iAGAC|0pEPG44ZOPdiI)$l}(e95p<(Y#67rykG(GfD&JjXV*@m2u-!Zb0n5pt*M%U1CMYMF@85Ta@O5%|k1f z;;l^aJCNXVhkVRUZ6|FquMDXiK{3vBKoh*TgyN)$D2SYv8-lSefKF%lsR8a~5HQc5 zPn1_qWCh?uyAvsYBFnk?R7C+F*&)c+Rd1(FwMojH;KVoKN-n-G42|;Q?bSh7g8yVqU*b2?WqwQ z0P0=rHVAMll||o(&!p)>3t8+8wkHl*>t&1CIIU5DNaNlMe?Y}1qw8Q9%up)b(S&1$8;aiVZ zxXjS$--kZuS4Kkc;Be(dXuh~IjoF(4<~y7t(&58ZsnK{+HX5*hvB?Uj2ZSOA zUL3(oBKQHcYr(kGz{XUWn=zsRA7V&rOa>(J=@z{IYwUyCAm4@dF-E>UabxRWK50dR zPdf^PFUR|p5xgpbS4R+OMVY#7pX7kfommsN1v0N*0`G{Ifp@(|v|ripvAeEL+;z3w zmF1KsE^-}1AhmGveK>+2i6CNyL%1H$YFd|3iF>Kk`+QP{457T&f5CNSJ3jd?pS5o~ zxn`_hZ`1QRdGUm3#h~pNvEI{#Yx@(_!ONe0Z=N2yeHOETl#_tOdBa-|{|~Pe*I46N zHSf_JfQIFQ;Jftc6X2~@G>)Q@K4G9!-OUmFWCU-C;AR6GC$ihE1}bMtCGy&YZaF9N zL(rQlZ4m5_(SmNqXhHe$Z;P2q#j(!E6J-*GxjYwWnx^r3A3{HFgN)VI|7k|?61?~f z*jB9kYy>|SL9DzE;Wj|&jB*PBOgMH%xrIRKR`Wuz#n6Kkx>vO4Gb>ivHSBPIkNwL) zm}SS3s-0=BBVcRZw=W>11Gj_yNuhMdGZ>Ddi#vYXi6s|0twX#DEWQXDI_bLupk)6N zz}Yjc;PGu^nAT&kW1Q=8(lmy#J|w?8*%=Xc`q60bF3b|;(g>0gqSdcK8fRMbpxSvP z!yh{|xE6;?q$OZ2KgkN|vkMT{68!ofAC1v)WEok6Gd0ePEFyK+kJ`~~F8b*getNu5 z#xaMAeXMyNS{r9};`0c#q7O#21*cfsL!4b{AgRo7A#&7Igc}K2!!HLPAKGZ;POpDj`eb(rndFWcV zS=YN0W}xxbcXHO?0t>A|we!Twp`(2RE$|>fS>T5N<+Tq1Of0a~J{#Nobl!THed|+AQ*qy)?<+AwhmYL`X3Ju}AaW{t7HS7+6@`j%PlsEhoU^Rw4 zW_68iD1KInVQksTW?f-36Qe&iK&o+96H~R#R;L_JKXECbfwA$5XpC2P`#JQep*5+h zX{Fwsa0M;2oI;51E)Gyr_~y-N<8GL|_yyXfsb2!rRqL++CiCWL`)oYp{qO0-|GWw` zZ#Y^PI&0o=G)$0j=gsp}`f5XQ{~V0CjPf*3p=pLFXG8vWI+xdCGMusCFa4+kZV2lS zg^A_94N1YI<%0*1mJ#tQuV$&|c)M#7i3E*RvJ()JQSW5>_BlJS8t6?htni49UbH=OtSpIcR)zj>Yg ke`MS%Dt*`suuPD>_ZDDlii7&yTh#mwgR9<%|NqVZ0*Mv#qyPW_ literal 25543 zcmb_l33#1Vng0L(-v1_ut=Q2iE>o%{g;Jd^C@s)70Tt6Sbt!E{A2gG+H*FwI+B7X7 zo62I5MNpB=K@i+VM;&oMK~X?)9ClDdWKlo`DWlG!2#WK)?|Zg;bCb3{)92yz`_K8# zx1aB2d(?sdVf}|Jbq(+mEk)&?AC^|!sa0(TPu3ALUh?&miS8r z+Q_RYL^ONL@M!Po!0-@o^5Uj1;_qzV0%cV!het>fH6&7FxjVnhq7Q#(B?!*|v^ymO zG^vsFi6>?itDQ#DFKFU>)EqUU-;~CFk8b;1(nc+Nht>iydtqr@@uv)ONCrrQKa)^Q zZlpJJCdtj994~H?W6n`(M8Bzx{T|)+*`$qf3~bmqI8fgVq`pIk6itf|Mq<-AM=F!dOv_mp>sTlaS;6p}>qJibB(Qz+= zG~RS?!sF18P0}YzNhcngNFNw`c|F@|E*glZu-k_iq`oh}HiEMN66+O9H*Ca5Hq-vg z^G3}VGgjwQiJ1zD!FV;B4lZM31Er zG8aT_L%J(q$;qgGMb$rf6JojN_|Mb=Qw?GKpuZyBl|*TDTy6GfI{G+G4pTa61i z(40{#)@3z7OHs^?EKKC?fZNGIvkE9P2vUkkUWzwbeUPGeaBz$i=y*h}cta3}Ml^9E z3sQWCxkb`ZM}TZ<^Yq?h zHBzcR+G}(|3>^ww*iSiaWsJquUPfAv&eOo}Lk}gJHSA3O%;qci;W&lQ%;BtmH$fD1 z@m4@K%;kx>dlMfq?%HQ~i4j_bL>?U(*gDWVNTfx31 zXmZ44^k`=n+FX`88nx2u7=V+dCcqGY>+QptZjwu75 zhN2C;xuEH(4-OfT`22wj_p6nAS&PO4FfF^w+LU)4}t?xx4)+a>p#0WAr&!LznqxKw22964&i=h$n&GCle2Rg*8 zZ`x%^o6OHxBa_cihz~^3PL1Gc5j-8B1U>`c)lp!Y^+Ht20)QIjf4|ju`Azm+v-H)V z_gPALCP10>LlHbHf@cGSXd2IBtQtk-_@=xxMaY5MjDQyvITioeO2qqE5k8GR;=))9 z07`cr;4zycF@ong#DE=rw>HIN(w@HU60h87wt#UsMjHX%QBUYo- zv_V@2pfn{WRP7leS_zKobyBmBvkO7`S>jy8UaY+s;N%bzogEyv%uHH3Fs+9Kbb(>J zw7q87CavC$!&+NE?ALg4oo_@zJloTNp+16>l`BBSuS@_j=7J+HwHn7mnSV^e5HT%( z*q;W7hGk$VA76oXY5l1PUddiGz*PXZYog-pmCfxy)gvgFmm8(K+^Xdi1Omsj1p?N6 z$^s4k8S3qGTP{%B6NSY33_ywX*$93P;4_j1&NuAciuJu)>pk`3HjZR@)Nng&Du&x7 zu9-mJlv&>Y0!Vbq=9dFb#+Ku?z_nS>lUdqeQFycSs)4RWxE0C^Et|8%y5&EngM06uX2Y~ z0}ki^PKOdQV!nb-`lTV{D}c7lXBK^Sp^iDPx$w5U%Mkqf!FKXn($z5>=Z&-gl-f}! zntuvVrg_kye699`AZI8jE&_617MVr5ir&}~SB08ls669EEz}qx;`X<{0x0F504U|2 z1gIhTYlHHW*zGBRCr6Vg3?nK{G7w}@)Dekxk)M66{lfb3)Z;A;N4t-nwJq7o{es6^ zL-n4W@i-YDKygrrU94=5fd2%NHu=8+C?ot9pp1YJ%+K?2nQzp<)L{G>(6p3bkdk=t z@zd7keQa9>lYbXIZT<6;%;)pvb1K#BSyncC_J1Ijl=@$QQtI~rrPLn)%ClIrIM4nO z;AO2mt0b0q7Hs8N1-pG_ZAd)%#{ouxWN+{8|F$-|8@p9ANU{sumFTC^&Cw6$C!_de zX=U~t3fX|OsBG|O)XD}->axLKtTO)!y5(r!$>@$Y7%#e?HDW>C`X<|k+1e!J&oB#K z1f~=!F90%!<`sY!F_~Woa1n}0(ZrFlHly%CpI7ZejBQ)AZUpPp;MqfgnViAl+!TLS`x&JZDZ2wz zbNs2LCPGF%H6&k`)HoE`q+@i&8f%3{kM0I~421jz0FPiTw}vYTz7Vym3DTUM1Tk0T zcWDY+ZCV@$tZabPqrVk|Ww9QO`9mG}Yfi+`S#TV)OT(m)VeAR3g$;;&KZmO4wrm90WXR#?_JIpz<6i{y(b z6!W0cmI6cq2UYS%sOl@wRTg?BKw0ST04idp0aV271yB()9UwDh{wjm=zmV9g4JJF#!e!$R5QWV5sm#JSr%uJ0rL;(qrX+pxdvKT?3C9gL*XAV?%p^&&V1(yo4>jE@QXYE3On(q!Ys5qRp z2LW6zPS|E38jBSKws+vKM?5=C1DHed2ibKAngPs;p8fHSzV_0wA?9nZP3 zOB%Bxx}QS(lb5{92)L66T&C#CQo=Qy{@LLl{@{4F54Unoe$*vuF>(2_>liEc&(t}45GM*$UEMUo(jW7#Fxw|K9i z_NAyFMmO?h)C_{ct24Vm44Z`NIAb2yx&{QbA5zS@*F85g1p+MsCh>(D9B2B+K~mc7)Y9E?Ah4bMM^N=+U4kDy=z4W5%&?I8wSvzHJn4oPV5S;i!54drmSh^!0_`FSLVg;IVJDkSY1fXYd0 z0dh@~*8ytniJ-N<1^xnK*E<9U5{XZfcED)Yw+;I#D8ruRpH z#dVPhBL|%Fr9h5M=)B?vR8kP;ugHQoHN}l+Rtpia$u=YPZr(h+CS=_-G1DEHGgq*b z;~l=q(e4P0X1)o8Wx0_EGJ{4V7I)UrMrF1eV8@}dXK|-gjif29OdI=P?k(;EiC}=@ zzGx&Sl1`yB3v#|%7KsYM_g922L-fl+bUC7-_=(A-kl{2$`xZYzN1k5^ozxgS@R&>% z-61)FQ{3XUyerBI{qm(vvZ@cYhJq4M62OI&pm@k2tUnZG`O-$3_QVP8?)jKO5<7%N zs@09rGE`lrU@TF$U=PlLQcwX!9MCM_M!j6Xv3~Ldg|w$d4m6Ys2Fxkwn1sf&B;+mi zY}AU;5(|*Xk7nVJGbUsCgm~n_cMm2LA5OOlR|0%h>&fW1OqPsYr zg-{wzRp*g3gZzAgGp*#z%PYQ$z547%eLho%#n<9PNzqLiH?c<94`7>S5{|k!-!KWH zxiT9ZDsup<6LMN5_9w(qQsK@{sPbm}uHYdf>ML)K z(jwbc4vV@mqcR)Pruoa!LE6Mlk|}yaoj_@Ms7!l$zTJU@YYpFSA<-yDh4 zC{0XO3d<|exjA*Lx4MetQW|6O)R}pkk_U5E48I8`jA(>*@Y2%t(*P4Aa3zG*HR>yy zf}a%}?C4FDxwUnSSDHdN-U<^;6qHBUU?zD!53tz`*w|Gh8JJa$0g`&k2v?yZ8lm|? zDJ9fw9*wX7UBvVY023o{77a!?6-LkwgA1f23*j`~MQ(^k_l&})jMhd{M;K{9)W-y(r_M0cz%Q+Pel>`+qW*C-w4mPF!9d;( z#R5{j7N8d7+%};yTj14i9kW2W0)^E62EbN=aTqrVhL=tFg^JfQ?hX_Rm@YG{uib-` zDfp&OB=0xzt!(=(g2-Trxtpj|X0w7+7*>-#{_*JNw<3XSWxeo2g+?^HCYtPk$O+9v zI3k*ffInB0&L)1VtL1q#jN9Q>u8OK~b{a%2gEe!k`N?b>*AN zSJwkMo%H?on>zxx|2Ai(KXCFFKyCvU2)kYHR8UNObql^F+V=^1v$@qC^@;C7i|bfH zDzw#(eD%_RU-=T~HyhZq8^_fzjNQN1sypg}e{7B0e3z;%kNK$^n3eAba#`Y@+t4N( z+#bO@*rCZi+y+-3l6$@fA<5OB8Dws41DmZ@Nlz++Apwn0FKO zwrk<4NPr1YFYm~J4$z&gCBPPDk6ks%hHp8L^mcBTg`RG<3Evg^vY8Te3ckcC-wvGl zWS}Q!Y6Z?C0$J(Dv=YbK{RUQ^Or04!hql=ksQBwH2f}z?CDKrGpkN~%-_c-1~`~kp_Mm185d~ozQ-?YI?>z(&000AqP3p{PL<%V0qRERDS)$B3v*Nt zl(scg(^4c&%TV#^8_)v$>Om+LVcu~}_c1WTBGkQ>d^bT92|hlLSB z?8k3rfM)y1XL?)wgmh zoCFN<*Z@;Q5cZt4A6|<)gyvL2xz^DB3oQLWHZPc8OAv@EcL2y#ZoWY z!4I%zW4KAKx;z@ejtXT2y*Xhd%I$vuBbnkEfO7jEQMtT%ysbuUUE}SyKu&@?`0V#q zos75SC%otoLppU?6ch%l9tq42dg@OACElL_HhXGQ^f{&NAlYa#wbPm%-g>QWmZMzW zdYioWk({b)D9v9W0;MSc$ymIouWm|>74>0eI}yE3klmhRM^-a9g593C2A>a<47LpQ z4-c+wcqH{U_O^7O^yM#9s;5wGteo?EBXc{Fme=*%bZQ5BAAo{KyP8Pw*#+&2DnQ=9 z6!>=9)c`W23v{TS!e2M$uSYcxA~ev?!l&(NkHz0SE1pNFi$iN2SF@*6xgTY+=b`XU= zs9p*@oni3ok3&lCp*{2}F*@82@d9i3R{jYSn!PD%b`NcjIlg)difd?Qo-@kKudrHY z=2rsbik=6}zJsDcbgWP_%jRN7^m{(8*edCH^KseMgYIxq&OD zgN@wxDub#I)2TqMK1Pti{FIMlOXE(C(#ydCg!PId@@cV&%xFAu1l8Z{2tP3l@c)R2 z=fXtvpF`!-9ad`WC+MIY6KeHY`>H+zCAi>ect-~DWH${K3_`bpP!qm6Jhe^5ES~Ux zJn~P}^Fg_nA-l1K`-3zx6@%#+%^Gm>=Sc=tx@o$ps1AIah z<;x%NvlD~dOv*n@@d zh|HlX{sRbcUs5hiQFz)}azmD)SZB2yL^;LE>OyBNRcNwBK#4ENG%R^g?1CaOxunev z9|kHH@tf+AR2;GyY+EiwSn^s`RP_Vy{7Y7A%7y$Q8lL2LS6DQChyK*_2-_kUU*_#RGV;m#0;RCH~h+rOPSc38(3MiX#%O7Js zF$iLY0iEAVZgg&W7P&DR66XRH|Gvrpw_7nB<<=;oyx9(xQUm5?UQ-JeR^=8H-6*iR z?{WWfUrSS+i|(y*ITKBJZVU4!S^m@DaTIW(giO&Cri9VTzD7SL3S8OPQ7scB&htR7 z2gOIN$hv$|!C~asq!RXaEtb>G>%0!oi)%ajmX>@iGXX5Wb=_@*;a9O) zi35cOxdV@@|xzj_v^@^%)kt|10lBZP0JCeT>m>SHjr(m)E1Xm1<~7MDS#* zb!wav!S_Y*{b*0ac0cI>n>)8AVGHD&&=6!l(LRFg*w+4a;W|4BSG}=FUhy!vAVvOi zDs>tp(5O2-f@ehVgAv>Y)Yfq&1zBf+~-9C$}fK-xz#Bsw55dW`66sKC_STpa^7=VQp zf{?rP%O}7vX!$ISq|F#Xq+Ms`^CS3?2!7PS8sF6y7XX!Orc@(uP1+V?BHs(WWzxq0 z4#aH1Fk`l${`iNH%%qa|&&|dp3fJ=+(ZBujvY~MBG7WHaU!_b(1RAbSG4CdJ!|b6c4VN>{#g?oX&geTcBY9G zZH#Nhog4_+tiAC)&7Tx15T~GyTyzu5Z#(5gGV={o_*3}S`QMcQrTbL?XU(*N$G5cu z=sirBdZ*Lpw5c6{L6iLMWP3#1?zz$5U2v?%gAX@%*)QLJEF8%Ru0N|sx(Bo)NynxH^$rIU2(my)tW|E7<{~<@Pe&Nlcte|fzuudd@unB>5|kIx1uWqL zjbXz#&_cs^ZGku0SM007WSCoG=%9_{jpa+wwwl^8S@Z18KPIgm4Wm`Kw(JF>jSU4Ue<-7;rCn%{OpUFu zZPtatw<>y%322eJ(D;p5%BPAlc}i%7(G@ zRK}s1sZL^co_INQ>zHk2&f$QU2e`&i)ZPq)!~>_oKM@wK6R-UvVglvMn9$x z{gOTiQeBLehI`;+QBylB+LRYE6418z(g%}Reh0?6oQENnRjHQGOC zU^M3gFTaO0Z!oZS8;Tz^QmfqxEK&1jxgn^+%l_)(z($LN@1hIDrqtDgqZKivs@F$! zp33V-jq#VAdKb{;h%oE$A6X!j-;u}%$8uVAr`+@cR-rk}r{u!bNR|1q4J~(@T-3a} zIFZYH7XorhsbP5&^Iv#GkaZ>e4WpKDf)VLl$IeGR_OW^X){XW*!Empr^kFZ+GC}s< XTY$|e4jOQ8QS&zqtvw9?^N#-mxh|Eo diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 74ed6351a..046b726ff 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -53,6 +53,9 @@ MK_CONSTANT(trans_fn, name("trans")); MK_CONSTANT(ne_symm_fn, name("ne_symm")); MK_CONSTANT(eq_ne_trans_fn, name("eq_ne_trans")); MK_CONSTANT(ne_eq_trans_fn, name("ne_eq_trans")); +MK_CONSTANT(heq_congr_fn, name("heq_congr")); +MK_CONSTANT(heq_congrl_fn, name("heq_congrl")); +MK_CONSTANT(heq_congrr_fn, name("heq_congrr")); MK_CONSTANT(eqt_elim_fn, name("eqt_elim")); MK_CONSTANT(eqf_elim_fn, name("eqf_elim")); MK_CONSTANT(congr1_fn, name("congr1")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index b77bf028c..3190b0c7a 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -151,6 +151,15 @@ inline expr mk_eq_ne_trans_th(expr const & e1, expr const & e2, expr const & e3, expr mk_ne_eq_trans_fn(); bool is_ne_eq_trans_fn(expr const & e); inline expr mk_ne_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_ne_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_heq_congr_fn(); +bool is_heq_congr_fn(expr const & e); +inline expr mk_heq_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_heq_congr_fn(), e1, e2, e3, e4, e5, e6, e7}); } +expr mk_heq_congrl_fn(); +bool is_heq_congrl_fn(expr const & e); +inline expr mk_heq_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrl_fn(), e1, e2, e3, e4, e5}); } +expr mk_heq_congrr_fn(); +bool is_heq_congrr_fn(expr const & e); +inline expr mk_heq_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrr_fn(), e1, e2, e3, e4, e5}); } expr mk_eqt_elim_fn(); bool is_eqt_elim_fn(expr const & e); inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_elim_fn(), e1, e2}); }