From c56df132b849ba4217ada1ecfd60b76d8fcc91e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Feb 2014 18:27:14 -0800 Subject: [PATCH] refactor(kernel): remove semantic attachments from the kernel Signed-off-by: Leonardo de Moura --- examples/lean/dep_if.lean | 24 +- examples/lean/ex4.lean | 7 +- src/builtin/Nat.lean | 24 +- src/builtin/cast.lean | 28 - src/builtin/heq.lean | 83 +-- src/builtin/kernel.lean | 717 +++++++++++++++---------- src/builtin/obj/Int.olean | Bin 1478 -> 1480 bytes src/builtin/obj/Nat.olean | Bin 22872 -> 22865 bytes src/builtin/obj/cast.olean | Bin 2804 -> 62 bytes src/builtin/obj/heq.olean | Bin 2543 -> 4669 bytes src/builtin/obj/kernel.olean | Bin 38400 -> 44201 bytes src/frontends/lean/parser_cmds.cpp | 2 +- src/frontends/lean/pp.cpp | 7 +- src/kernel/kernel.cpp | 85 +-- src/kernel/kernel.h | 9 - src/kernel/kernel_decls.cpp | 162 +++--- src/kernel/kernel_decls.h | 486 ++++++++++------- src/kernel/normalizer.cpp | 14 +- src/library/cast_decls.cpp | 6 - src/library/cast_decls.h | 19 - src/library/heq_decls.cpp | 14 +- src/library/heq_decls.h | 42 +- src/library/simplifier/simplifier.cpp | 4 +- src/tests/library/arith.cpp | 27 - tests/lean/add_assoc.lean.expected.out | 2 +- tests/lean/arith1.lean.expected.out | 4 +- tests/lean/arith3.lean.expected.out | 8 +- tests/lean/arith6.lean.expected.out | 14 +- tests/lean/arith7.lean | 8 +- tests/lean/arith7.lean.expected.out | 11 +- tests/lean/cond_tac.lean | 6 - tests/lean/cond_tac.lean.expected.out | 2 - tests/lean/eq4.lean.expected.out | 4 +- tests/lean/find.lean.expected.out | 6 +- tests/lean/lua11.lean | 2 +- tests/lean/map.lean.expected.out | 2 + tests/lean/norm_tac.lean | 4 +- tests/lean/norm_tac.lean.expected.out | 3 +- tests/lean/revapp.lean | 18 +- tests/lean/revapp.lean.expected.out | 7 +- tests/lean/rs.lean.expected.out | 12 +- tests/lean/scope.lean.expected.out | 2 +- tests/lean/scope_bug1.lean | 4 +- tests/lean/simp10.lean | 5 + tests/lean/simp10.lean.expected.out | 5 +- tests/lean/simp17.lean | 2 +- tests/lean/simp17.lean.expected.out | 5 +- tests/lean/simp3.lean.expected.out | 8 +- tests/lean/simp33.lean | 2 +- tests/lean/simp33.lean.expected.out | 3 +- tests/lean/tst1.lean.expected.out | 5 +- tests/lean/tst11.lean | 7 +- tests/lean/tst11.lean.expected.out | 6 +- tests/lean/tst12.lean.expected.out | 2 +- tests/lean/tst17.lean.expected.out | 2 +- tests/lean/tst4.lean.expected.out | 2 +- tests/lean/using_bug1.lean | 4 +- tests/lua/env4.lua | 2 +- 58 files changed, 1029 insertions(+), 910 deletions(-) diff --git a/examples/lean/dep_if.lean b/examples/lean/dep_if.lean index 71f0c9975..e89113c32 100644 --- a/examples/lean/dep_if.lean +++ b/examples/lean/dep_if.lean @@ -10,14 +10,14 @@ import tactic -- We define the "dependent" if-then-else using Hilbert's choice operator ε. -- Note that ε is only applicable to non-empty types. Thus, we first -- prove the following auxiliary theorem. -theorem nonempty_resolve {A : TypeU} {c : Bool} (t : c → A) (e : ¬ c → A) : nonempty A +theorem inhabited_resolve {A : TypeU} {c : Bool} (t : c → A) (e : ¬ c → A) : inhabited A := or_elim (em c) - (λ Hc, nonempty_range (nonempty_intro t) Hc) - (λ Hnc, nonempty_range (nonempty_intro e) Hnc) + (λ Hc, inhabited_range (inhabited_intro t) Hc) + (λ Hnc, inhabited_range (inhabited_intro e) Hnc) -- The actual definition definition dep_if {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) : A -:= ε (nonempty_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) +:= ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : c) : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = t H @@ -35,9 +35,9 @@ theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) theorem dep_if_elim_then {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : c) : dep_if c t e = t H := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = t H) := funext (λ r, then_simp A c r t e H) - in calc dep_if c t e = ε (nonempty_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) - ... = ε (nonempty_resolve t e) (λ r, r = t H) : { s1 } - ... = t H : eps_singleton (nonempty_resolve t e) (t H) + in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) + ... = ε (inhabited_resolve t e) (λ r, r = t H) : { s1 } + ... = t H : eps_singleton (inhabited_resolve t e) (t H) theorem dep_if_true {A : TypeU} (t : true → A) (e : ¬ true → A) : dep_if true t e = t trivial := dep_if_elim_then true t e trivial @@ -58,12 +58,12 @@ theorem else_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) theorem dep_if_elim_else {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : ¬ c) : dep_if c t e = e H := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = e H) := funext (λ r, else_simp A c r t e H) - in calc dep_if c t e = ε (nonempty_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) - ... = ε (nonempty_resolve t e) (λ r, r = e H) : { s1 } - ... = e H : eps_singleton (nonempty_resolve t e) (e H) + in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) + ... = ε (inhabited_resolve t e) (λ r, r = e H) : { s1 } + ... = e H : eps_singleton (inhabited_resolve t e) (e H) -theorem dep_if_false {A : TypeU} (t : false → A) (e : ¬ false → A) : dep_if false t e = e trivial -:= dep_if_elim_else false t e trivial +theorem dep_if_false {A : TypeU} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial +:= dep_if_elim_else false t e not_false_trivial import cast diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean index e470b12d3..adc9f50e3 100644 --- a/examples/lean/ex4.lean +++ b/examples/lean/ex4.lean @@ -1,8 +1,5 @@ import Int import tactic +set_option simplifier::unfold true -- allow the simplifier to unfold definitions definition a : Nat := 10 --- Trivial indicates a "proof by evaluation" -theorem T1 : a > 0 := trivial -theorem T2 : a - 5 > 3 := trivial --- The next one is commented because it fails --- theorem T3 : a > 11 := trivial +theorem T1 : a > 0 := (by simp) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 92c94d039..11beb542d 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -44,7 +44,7 @@ theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a := induction_on a - (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) H) + (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) (a_neq_a_elim H)) (λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0), or_elim (em (n = 0)) (λ Heq0 : n = 0, exists_intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 })) @@ -60,7 +60,7 @@ theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n + theorem add_zerol (a : Nat) : 0 + a = a := induction_on a - (have 0 + 0 = 0 : trivial) + (have 0 + 0 = 0 : add_zeror 0) (λ (n : Nat) (iH : 0 + n = n), calc 0 + (n + 1) = (0 + n) + 1 : add_succr 0 n ... = n + 1 : { iH }) @@ -95,11 +95,11 @@ theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) theorem mul_zerol (a : Nat) : 0 * a = 0 := induction_on a - (have 0 * 0 = 0 : trivial) + (have 0 * 0 = 0 : mul_zeror 0) (λ (n : Nat) (iH : 0 * n = 0), calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n ... = 0 + 0 : { iH } - ... = 0 : trivial) + ... = 0 : add_zerol 0) theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b := induction_on b @@ -118,14 +118,14 @@ theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b theorem mul_onel (a : Nat) : 1 * a = a := induction_on a - (have 1 * 0 = 0 : trivial) + (have 1 * 0 = 0 : mul_zeror 1) (λ (n : Nat) (iH : 1 * n = n), calc 1 * (n + 1) = 1 * n + 1 : mul_succr 1 n ... = n + 1 : { iH }) theorem mul_oner (a : Nat) : a * 1 = a := induction_on a - (have 0 * 1 = 0 : trivial) + (have 0 * 1 = 0 : mul_zeror 1) (λ (n : Nat) (iH : n * 1 = n), calc (n + 1) * 1 = n * 1 + 1 : mul_succl n 1 ... = n + 1 : { iH }) @@ -142,7 +142,7 @@ theorem mul_comm (a b : Nat) : a * b = b * a theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c := induction_on a (calc 0 * (b + c) = 0 : mul_zerol (b + c) - ... = 0 + 0 : trivial + ... = 0 + 0 : add_zeror 0 ... = 0 * b + 0 : { symm (mul_zerol b) } ... = 0 * b + 0 * c : { symm (mul_zerol c) }) (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), @@ -223,7 +223,6 @@ theorem le_refl (a : Nat) : a ≤ a := le_intro (add_zeror a) theorem le_zero (a : Nat) : 0 ≤ a := le_intro (add_zerol a) - theorem le_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1), obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2), @@ -353,8 +352,9 @@ set_opaque add true set_opaque mul true set_opaque le true set_opaque id true -set_opaque ge true -set_opaque lt true -set_opaque gt true -set_opaque id true +-- We should only mark constants as opaque after we proved the theorems/properties we need. +-- set_opaque ge true +-- set_opaque lt true +-- set_opaque gt true +-- set_opaque id true end \ No newline at end of file diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index d09e26189..2fc7ea68e 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -1,29 +1 @@ import heq - -variable cast {A B : TypeM} : A = B → A → B - -axiom cast_heq {A B : TypeM} (H : A = B) (a : A) : cast H a == a - -theorem cast_app {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : - cast Hb f (cast Ha a) == f a -:= let s1 : cast Hb f == f := cast_heq Hb f, - s2 : cast Ha a == a := cast_heq Ha a - in hcongr s1 s2 - --- The following theorems can be used as rewriting rules - -theorem cast_eq {A : TypeM} (H : A = A) (a : A) : cast H a = a -:= to_eq (cast_heq H a) - -theorem cast_trans {A B C : TypeM} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a -:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a), - s2 : cast Hab a == a := cast_heq Hab a, - s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a, - s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3) - in to_eq s4 - -theorem cast_pull {A : TypeM} {B B' : A → TypeM} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) : - cast Hb f a = cast Hba (f a) -:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a), - s2 : cast Hba (f a) == f a := cast_heq Hba (f a) - in to_eq (htrans s1 (hsymm s2)) diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 8bc994b37..6321f7e77 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -1,40 +1,28 @@ --- Heterogenous equality -variable heq {A B : TypeU} : A → B → Bool -infixl 50 == : heq - -axiom heq_eq {A : TypeU} (a b : A) : a == b ↔ a = b - -theorem to_eq {A : TypeU} {a b : A} (H : a == b) : a = b -:= (heq_eq a b) ◂ H - -theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b -:= (symm (heq_eq a b)) ◂ H - -theorem hrefl {A : TypeU} (a : A) : a == a -:= to_heq (refl a) - -theorem heqt_elim {a : Bool} (H : a == true) : a -:= eqt_elim (to_eq H) - -axiom hsymm {A B : TypeU} {a : A} {b : B} : a == b → b == a - -axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} : a == b → b == c → a == c - -axiom hcongr {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : - f == f' → a == a' → f a == f' a' +-- Axioms and theorems for casting and heterogenous equality +import macros +-- In the following definitions the type of A and B cannot be (Type U) +-- because A = B would be @eq (Type U+1) A B, and +-- the type of eq is (∀T : (Type U), T → T → bool). +-- So, we define M a universe smaller than U. universe M ≥ 1 definition TypeM := (Type M) --- In the following definitions the type of A and A' cannot be TypeU --- because A = A' would be @eq (Type U+1) A A', and --- the type of eq is (∀T : (Type U), T → T → bool). --- So, we define M a universe smaller than U. +variable cast {A B : (Type M)} : A = B → A → B -axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : +axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a + +axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a + +axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c + +axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : + f == f' → a == a' → f a == f' a' + +axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : A = A' → (∀ x x', x == x' → f x == f' x') → f == f' -theorem hsfunext {A : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : +theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : (∀ x, f x == f' x) → f == f' := λ Hb, hfunext (refl A) (λ (x x' : A) (Hx : x == x'), @@ -42,8 +30,39 @@ theorem hsfunext {A : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, s2 : f' x == f' x' := hcongr (hrefl f') Hx in htrans s1 s2) -axiom hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : - A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) +theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool} + (Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x) +:= boolext + (assume (H : ∀ x : A, B x), + take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x'))) + (assume (H : ∀ x' : A', B' x'), + take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x))) + +theorem cast_app {A A' : (Type M)} {B : A → (Type M)} {B' : A' → (Type M)} + (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) : + cast Hb f (cast Ha a) == f a +:= let s1 : cast Hb f == f := cast_heq Hb f, + s2 : cast Ha a == a := cast_heq Ha a + in hcongr s1 s2 + +-- The following theorems can be used as rewriting rules + +theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a +:= to_eq (cast_heq H a) + +theorem cast_trans {A B C : (Type M)} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a +:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a), + s2 : cast Hab a == a := cast_heq Hab a, + s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a, + s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3) + in to_eq s4 + +theorem cast_pull {A : (Type M)} {B B' : A → (Type M)} + (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) : + cast Hb f a = cast Hba (f a) +:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a), + s2 : cast Hba (f a) == f a := cast_heq Hba (f a) + in to_eq (htrans s1 (hsymm s2)) -- The following axiom is not very useful, since the resultant -- equality is actually (@eq TypeM (∀ x, B x) (∀ x, B' x)). diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 080da2172..45aa54ac3 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -2,12 +2,43 @@ import macros import tactic universe U ≥ 1 -definition TypeU := (Type U) +definition TypeU := (Type U) + +-- create default rewrite rule set +(* mk_rewrite_rule_set() *) variable Bool : Type --- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions -builtin true : Bool -builtin false : Bool +-- Heterogeneous equality +variable heq {A B : (Type U)} (a : A) (b : B) : Bool +infixl 50 == : heq + +-- Reflexivity for heterogeneous equality +axiom hrefl {A : (Type U)} (a : A) : a == a + +-- Homogeneous equality +definition eq {A : (Type U)} (a b : A) := a == b +infix 50 = : eq + +theorem refl {A : (Type U)} (a : A) : a = a +:= hrefl a + +theorem heq_eq {A : (Type U)} (a b : A) : (a == b) = (a = b) +:= refl (a == b) + +definition true : Bool +:= (λ x : Bool, x) = (λ x : Bool, x) + +theorem trivial : true +:= refl (λ x : Bool, x) + +set_opaque true true + +definition false : Bool +:= ∀ x : Bool, x + +set_opaque false true +alias ⊤ : true +alias ⊥ : false definition not (a : Bool) := a → false notation 40 ¬ _ : not @@ -24,16 +55,25 @@ infixr 35 ∧ : and definition implies (a b : Bool) := a → b -builtin eq {A : (Type U)} (a b : A) : Bool -infix 50 = : eq - -definition neq {A : TypeU} (a b : A) := ¬ (a = b) +definition neq {A : (Type U)} (a b : A) := ¬ (a = b) infix 50 ≠ : neq +theorem a_neq_a_elim {A : (Type U)} {a : A} (H : a ≠ a) : false +:= H (refl a) + definition iff (a b : Bool) := a = b infixr 25 <-> : iff infixr 25 ↔ : iff +theorem em (a : Bool) : a ∨ ¬ a +:= assume Hna : ¬ a, Hna + +theorem not_intro {a : Bool} (H : a → false) : ¬ a +:= H + +theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false +:= H2 H1 + -- The Lean parser has special treatment for the constant exists. -- It allows us to write -- exists x y : A, P x y and ∃ x y : A, P x y @@ -42,103 +82,14 @@ infixr 25 ↔ : iff -- That is, it treats the exists as an extra binder such as fun and forall. -- It also provides an alias (Exists) that should be used when we -- want to treat exists as a constant. -definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x, ¬ (P x)) - -definition nonempty (A : TypeU) := ∃ x : A, true - --- If we have an element of type A, then A is nonempty -theorem nonempty_intro {A : TypeU} (a : A) : nonempty A -:= assume H : (∀ x, ¬ true), (H a) - -theorem em (a : Bool) : a ∨ ¬ a -:= assume Hna : ¬ a, Hna +definition Exists (A : (Type U)) (P : A → Bool) +:= ¬ (∀ x, ¬ (P x)) axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a -axiom refl {A : TypeU} (a : A) : a = a - -axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b - --- Function extensionality -axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g - --- Forall extensionality -axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x) - --- Epsilon (Hilbert's operator) -variable eps {A : TypeU} (H : nonempty A) (P : A → Bool) : A -alias ε : eps -axiom eps_ax {A : TypeU} (H : nonempty A) {P : A → Bool} (a : A) : P a → P (ε H P) - --- Proof irrelevance -axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 - --- Alias for subst where we can provide P explicitly, but keep A,a,b implicit -theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b -:= subst H1 H2 - -theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (nonempty_intro a) P) -:= assume H : P a, @eps_ax A (nonempty_intro a) P a H - -theorem eps_singleton {A : TypeU} (H : nonempty A) (a : A) : ε H (λ x, x = a) = a -:= let P := λ x, x = a, - Ha : P a := refl a - in eps_ax H a Ha - --- A function space (∀ x : A, B x) is nonempty if forall a : A, we have nonempty (B a) -theorem nonempty_fun {A : TypeU} {B : A → TypeU} (Hn : ∀ a, nonempty (B a)) : nonempty (∀ x, B x) -:= nonempty_intro (λ x, ε (Hn x) (λ y, true)) - --- if-then-else expression -definition ite {A : TypeU} (c : Bool) (a b : A) : A -:= ε (nonempty_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b)) -notation 45 if _ then _ else _ : ite - --- We will mark 'not' as opaque later -theorem not_intro {a : Bool} (H : a → false) : ¬ a -:= H - -theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f -:= funext (λ x : A, refl (f x)) - --- create default rewrite rule set -(* mk_rewrite_rule_set() *) - -theorem trivial : true -:= refl true - -theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false -:= H2 H1 - -theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b -:= subst H2 H1 - -infixl 100 <| : eqmp -infixl 100 ◂ : eqmp - -theorem boolcomplete (a : Bool) : a = true ∨ a = false -:= case (λ x, x = true ∨ x = false) trivial trivial a - theorem false_elim (a : Bool) (H : false) : a := case (λ x, x) trivial H a -theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c -:= assume Ha, H2 (H1 Ha) - -theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c -:= assume Ha, H2 ◂ (H1 Ha) - -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 - -add_rewrite not_not_eq - -theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a -:= (not_not_eq a) ◂ H - theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a := assume Ha : a, absurd (H1 Ha) H2 @@ -148,29 +99,6 @@ theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b := false_elim b (absurd H1 H2) -theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a -:= not_not_elim - (have ¬ ¬ a : - assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna) - Hnab) - -theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b -:= assume Hb : b, absurd (assume Ha : a, Hb) - H - -theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b -:= H1 H2 - --- Recall that and is defined as ¬ (a → ¬ b) -theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b -:= assume H : a → ¬ b, absurd H2 (H H1) - -theorem and_eliml {a b : Bool} (H : a ∧ b) : a -:= not_imp_eliml H - -theorem and_elimr {a b : Bool} (H : a ∧ b) : b -:= not_not_elim (not_imp_elimr H) - -- Recall that or is defined as ¬ a → b theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b := assume H1 : ¬ a, absurd_elim b H H1 @@ -178,23 +106,82 @@ theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b := assume H1 : ¬ a, H -theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c -:= not_not_elim - (assume H : ¬ c, - absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H)))) - H) +theorem boolcomplete (a : Bool) : a = true ∨ a = false +:= case (λ x, x = true ∨ x = false) + (or_introl (refl true) (true = false)) + (or_intror (false = true) (refl false)) + a -theorem refute {a : Bool} (H : ¬ a → false) : a -:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1)) +theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true +:= case (λ x, x = false ∨ x = true) + (or_intror (true = false) (refl true)) + (or_introl (refl false) (false = true)) + a -theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a +theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b +:= H1 H2 + +axiom subst {A : (Type U)} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b + +-- Alias for subst where we provide P explicitly, but keep A,a,b implicit +theorem substp {A : (Type U)} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b +:= subst H1 H2 + +theorem symm {A : (Type U)} {a b : A} (H : a = b) : b = a := subst (refl a) H +theorem trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c +:= subst H1 H2 + +theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a +:= substp (fun h : A → B, f a = h a) (refl (f a)) H + +theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b +:= substp (fun x : A, f a = f x) (refl (f a)) H + +theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b +:= subst (congr2 f H2) (congr1 b H1) + +theorem true_ne_false : ¬ true = false +:= assume H : true = false, + subst trivial H + +theorem absurd_not_true (H : ¬ true) : false +:= absurd trivial H + +theorem not_false_trivial : ¬ false +:= assume H : false, H + +-- "equality modus pones" +theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b +:= subst H2 H1 + +infixl 100 <| : eqmp +infixl 100 ◂ : eqmp + theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a := (symm H1) ◂ H2 -theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c -:= subst H1 H2 +theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c +:= assume Ha, H2 (H1 Ha) + +theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c +:= assume Ha, H2 ◂ (H1 Ha) + +theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c +:= assume Ha, H2 (H1 ◂ Ha) + +theorem to_eq {A : TypeU} {a b : A} (H : a == b) : a = b +:= (heq_eq a b) ◂ H + +theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b +:= (symm (heq_eq a b)) ◂ H + +theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b +:= (λ Ha : a, eqmp H Ha) + +theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a +:= (λ Hb : b, eqmpr H Hb) theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a := assume H1 : b = a, H (symm H1) @@ -211,41 +198,72 @@ theorem eqt_elim {a : Bool} (H : a = true) : a theorem eqf_elim {a : Bool} (H : a = false) : ¬ a := not_intro (λ Ha : a, H ◂ Ha) -theorem congr1 {A B : TypeU} {f g : A → B} (a : A) (H : f = g) : f a = g a -:= substp (fun h : A → B, f a = h a) (refl (f a)) H +theorem heqt_elim {a : Bool} (H : a == true) : a +:= eqt_elim (to_eq H) -theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b -:= substp (fun x : A, f a = f x) (refl (f a)) H +theorem not_true : (¬ true) = false +:= let aux : ¬ (¬ true) = true + := assume H : (¬ true) = true, + absurd_not_true (subst trivial (symm H)) + in resolve1 (boolcomplete (¬ true)) aux -theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b -:= subst (congr2 f H2) (congr1 b H1) +theorem not_false : (¬ false) = true +:= let aux : ¬ (¬ false) = false + := assume H : (¬ false) = false, + subst not_false_trivial H + in resolve1 (boolcomplete_swapped (¬ false)) aux --- Recall that exists is defined as ¬ ∀ x : A, ¬ P x -theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B -:= refute (λ R : ¬ B, - absurd (take a : A, mt (assume H : P a, H2 a H) R) - H1) +add_rewrite not_true not_false -theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P -:= assume H1 : (∀ x : A, ¬ P x), - absurd H (H1 a) +theorem not_not_eq (a : Bool) : (¬ ¬ a) = a +:= case (λ x, (¬ ¬ x) = x) + (calc (¬ ¬ true) = (¬ false) : { not_true } + ... = true : not_false) + (calc (¬ ¬ false) = (¬ true) : { not_false } + ... = false : not_true) + a -theorem nonempty_elim {A : TypeU} (H1 : nonempty A) {B : Bool} (H2 : A → B) : B -:= obtain (w : A) (Hw : true), from H1, - H2 w +add_rewrite not_not_eq -theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A -:= obtain (w : A) (Hw : P w), from H, - exists_intro w trivial +theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b +:= not_not_eq (a = b) -theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P) -:= obtain (w : A) (Hw : P w), from H, - eps_ax (nonempty_ex_intro H) w Hw +add_rewrite not_neq -theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) -:= exists_intro - (λ x, ε (nonempty_ex_intro (H x)) (λ y, R x y)) -- witness for f - (λ x, exists_to_eps (H x)) -- proof that witness satisfies ∀ x, R x (f x) +theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b +:= (not_neq a b) ◂ H + +theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a +:= (not_not_eq a) ◂ H + +theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a +:= not_not_elim + (have ¬ ¬ a : + assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna) + Hnab) + +theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b +:= assume Hb : b, absurd (assume Ha : a, Hb) + H + +-- Recall that and is defined as ¬ (a → ¬ b) +theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b +:= assume H : a → ¬ b, absurd H2 (H H1) + +theorem and_eliml {a b : Bool} (H : a ∧ b) : a +:= not_imp_eliml H + +theorem and_elimr {a b : Bool} (H : a ∧ b) : b +:= not_not_elim (not_imp_elimr H) + +theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c +:= not_not_elim + (assume H : ¬ c, + absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H)))) + H) + +theorem refute {a : Bool} (H : ¬ a → false) : a +:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1)) theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b := or_elim (boolcomplete a) @@ -256,23 +274,10 @@ theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b (λ Hbt : b = true, false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf)) (λ Hbf : b = false, trans Haf (symm Hbf))) +-- Another name for boolext theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b := boolext Hab Hba -theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b -:= (λ Ha : a, eqmp H Ha) - -theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a -:= (λ Hb : b, eqmpr H Hb) - -theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} : - (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) -:= iff_intro - (λ H : (∀ x, ∃ y, P x y), axiom_of_choice H) - (λ 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 eqt_intro {a : Bool} (H : a) : a = true := boolext (assume H1 : a, trivial) (assume H2 : true, H) @@ -281,19 +286,26 @@ 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 -:= eqf_intro H +theorem a_neq_a {A : (Type U)} (a : A) : (a ≠ a) ↔ false +:= boolext (assume H, a_neq_a_elim H) + (assume H, false_elim (a ≠ a) H) -theorem eq_id {A : TypeU} (a : A) : (a = a) ↔ true +theorem eq_id {A : (Type U)} (a : A) : (a = a) ↔ true := eqt_intro (refl a) theorem iff_id (a : Bool) : (a ↔ a) ↔ true := eqt_intro (refl a) -add_rewrite eq_id iff_id +theorem neq_elim {A : (Type U)} {a b : A} (H : a ≠ b) : a = b ↔ false +:= eqf_intro H + +theorem neq_to_not_eq {A : (Type U)} {a b : A} : a ≠ b ↔ ¬ a = b +:= refl (a ≠ b) + +add_rewrite eq_id iff_id neq_to_not_eq -- Remark: ordered rewriting + assoc + comm + left_comm sorts a term lexicographically -theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) (assoc : ∀ x y z, R (R x y) z = R x (R y z)) : +theorem left_comm {A : (Type U)} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) (assoc : ∀ x y z, R (R x y) z = R x (R y z)) : ∀ x y z, R x (R y z) = R y (R x z) := take x y z, calc R x (R y z) = R (R x y) z : symm (assoc x y z) ... = R (R y x) z : { comm x y } @@ -325,7 +337,8 @@ theorem or_falser (a : Bool) : false ∨ a ↔ 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) +:= boolext (assume H : true ∨ a, trivial) + (assume H : true, or_introl trivial a) theorem or_truer (a : Bool) : a ∨ true ↔ true := trans (or_comm a true) (or_truel a) @@ -338,6 +351,9 @@ theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) add_rewrite or_comm or_assoc or_id or_falsel or_falser or_truel or_truer or_tauto or_left_comm +theorem resolve2 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a +:= resolve1 ((or_comm a b) ◂ H1) H2 + 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)) @@ -374,16 +390,19 @@ theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) add_rewrite and_comm and_assoc and_id and_falsel and_falser and_truel and_truer and_absurd and_left_comm theorem imp_truer (a : Bool) : (a → true) ↔ true -:= case (λ x, (x → true) ↔ true) trivial trivial a +:= boolext (assume H, trivial) + (assume H Ha, trivial) theorem imp_truel (a : Bool) : (true → a) ↔ a -:= case (λ x, (true → x) ↔ x) trivial trivial a +:= boolext (assume H : true → a, H trivial) + (assume Ha H, Ha) 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 +:= boolext (assume H, trivial) + (assume H Hf, false_elim a Hf) theorem imp_id (a : Bool) : (a → a) ↔ true := eqt_intro (λ H : a, H) @@ -391,7 +410,7 @@ theorem imp_id (a : Bool) : (a → a) ↔ true add_rewrite imp_truer imp_truel imp_falser imp_falsel imp_id theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b -:= iff_intro +:= boolext (assume H : a → b, (or_elim (em a) (λ Ha : a, or_intror (¬ a) (H Ha)) @@ -400,83 +419,18 @@ theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b assume Ha : a, resolve1 H ((symm (not_not_eq a)) ◂ Ha)) -theorem not_true : ¬ true ↔ false -:= trivial - -theorem not_false : ¬ false ↔ true -:= trivial - -theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b -:= not_not_eq (a = b) - -add_rewrite not_true not_false not_neq - -theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b -:= (not_neq a b) ◂ H - -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) - 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) - a - -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) - 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 := congr2 not H -theorem exists_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∃ x : A, p) ↔ p -:= iff_intro - (assume Hl : (∃ x : A, p), - obtain (w : A) (Hw : p), from Hl, - Hw) - (assume Hr : p, - nonempty_elim H (λ w, exists_intro w Hr)) +-- Recall that exists is defined as ¬ ∀ x : A, ¬ P x +theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B +:= refute (λ R : ¬ B, + absurd (take a : A, mt (assume H : P a, H2 a H) R) + H1) -theorem forall_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∀ x : A, p) ↔ p -:= iff_intro - (assume Hl : (∀ x : A, p), - nonempty_elim H (λ w, Hl w)) - (assume Hr : p, - take x, Hr) - -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) -:= 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 exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P +:= assume H1 : (∀ x : A, ¬ P x), + absurd H (H1 a) 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) @@ -504,6 +458,46 @@ theorem exists_unfold {A : TypeU} (P : A → Bool) (a : 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) +definition inhabited (A : (Type U)) +:= ∃ x : A, true + +-- If we have an element of type A, then A is inhabited +theorem inhabited_intro {A : TypeU} (a : A) : inhabited A +:= assume H : (∀ x, ¬ true), absurd_not_true (H a) + +theorem inhabited_elim {A : TypeU} (H1 : inhabited A) {B : Bool} (H2 : A → B) : B +:= obtain (w : A) (Hw : true), from H1, + H2 w + +theorem inhabited_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : inhabited A +:= obtain (w : A) (Hw : P w), from H, + exists_intro w trivial + +-- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty +theorem inhabited_range {A : TypeU} {B : A → TypeU} (H : inhabited (∀ x, B x)) (a : A) : inhabited (B a) +:= refute (λ N : ¬ inhabited (B a), + let s1 : ¬ ∃ x : B a, true := N, + s2 : ∀ x : B a, false := take x : B a, absurd_not_true (not_exists_elim s1 x), + s3 : ∃ y : (∀ x, B x), true := H + in obtain (w : (∀ x, B x)) (Hw : true), from s3, + let s4 : B a := w a + in s2 s4) + +theorem exists_rem {A : TypeU} (H : inhabited A) (p : Bool) : (∃ x : A, p) ↔ p +:= iff_intro + (assume Hl : (∃ x : A, p), + obtain (w : A) (Hw : p), from Hl, + Hw) + (assume Hr : p, + inhabited_elim H (λ w, exists_intro w Hr)) + +theorem forall_rem {A : TypeU} (H : inhabited A) (p : Bool) : (∀ x : A, p) ↔ p +:= iff_intro + (assume Hl : (∀ x : A, p), + inhabited_elim H (λ w, Hl w)) + (assume Hr : p, + take x, Hr) + -- Congruence theorems for contextual simplification -- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then @@ -588,6 +582,87 @@ theorem and_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H 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 not_and (a b : Bool) : ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b +:= boolext (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_intror (¬ a) Hnb)) + (assume Hna, or_introl Hna (¬ b))) + (assume (H : ¬ a ∨ ¬ b) (N : a ∧ b), + or_elim H + (assume Hna, absurd (and_eliml N) Hna) + (assume Hnb, absurd (and_elimr N) Hnb)) + +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 +:= boolext (assume H, or_elim (em a) + (assume Ha, absurd_elim (¬ a ∧ ¬ b) (or_introl Ha b) H) + (assume Hna, or_elim (em b) + (assume Hb, absurd_elim (¬ a ∧ ¬ b) (or_intror a Hb) H) + (assume Hnb, and_intro Hna Hnb))) + (assume (H : ¬ a ∧ ¬ b) (N : a ∨ b), + or_elim N + (assume Ha, absurd Ha (and_eliml H)) + (assume Hb, absurd Hb (and_elimr H))) + +theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b +:= (not_or a b) ◂ H + +theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b +:= calc (¬ (a → b)) = ¬ (¬ a ∨ b) : { imp_or a b } + ... = ¬ ¬ a ∧ ¬ b : not_or (¬ a) b + ... = a ∧ ¬ b : by simp + +theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b +:= (not_implies a b) ◂ H + +theorem a_eq_not_a (a : Bool) : (a = ¬ a) ↔ false +:= boolext (λ H, or_elim (em a) + (λ Ha, absurd Ha (subst Ha H)) + (λ Hna, absurd (subst Hna (symm H)) Hna)) + (λ H, false_elim (a = ¬ a) H) + +theorem a_iff_not_a (a : Bool) : (a ↔ ¬ a) ↔ false +:= a_eq_not_a a + +theorem true_eq_false : (true = false) ↔ false +:= subst (a_eq_not_a true) not_true + +theorem true_iff_false : (true ↔ false) ↔ false +:= true_eq_false + +theorem false_eq_true : (false = true) ↔ false +:= subst (a_eq_not_a false) not_false + +theorem false_iff_true : (false ↔ true) ↔ false +:= false_eq_true + +theorem a_iff_true (a : Bool) : (a ↔ true) ↔ a +:= boolext (λ H, eqt_elim H) + (λ H, eqt_intro H) + +theorem a_iff_false (a : Bool) : (a ↔ false) ↔ ¬ a +:= boolext (λ H, eqf_elim H) + (λ H, eqf_intro H) + +add_rewrite a_eq_not_a a_iff_not_a true_eq_false true_iff_false false_eq_true false_iff_true a_iff_true a_iff_false + +theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b) +:= or_elim (em b) + (λ Hb, calc (¬ (a ↔ b)) = (¬ (a ↔ true)) : { eqt_intro Hb } + ... = ¬ a : { a_iff_true a } + ... = ¬ a ↔ true : { symm (a_iff_true (¬ a)) } + ... = ¬ a ↔ b : { symm (eqt_intro Hb) }) + (λ Hnb, calc (¬ (a ↔ b)) = (¬ (a ↔ false)) : { eqf_intro Hnb } + ... = ¬ ¬ a : { a_iff_false a } + ... = ¬ a ↔ false : { symm (a_iff_false (¬ a)) } + ... = ¬ a ↔ b : { symm (eqf_intro Hnb) }) + +theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b +:= (not_iff a b) ◂ H + theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x) := boolext (assume H : (∀ x, p ∨ φ x), @@ -602,9 +677,16 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, (λ H2 : (∀ x, φ x), or_intror p (H2 x))) theorem forall_or_distributel {A : Type} (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) +:= boolext + (assume H : (∀ x, φ x ∨ p), + or_elim (em p) + (λ Hp : p, or_intror (∀ x, φ x) Hp) + (λ Hnp : ¬ p, or_introl (take x, resolve2 (H x) Hnp) p)) + (assume H : (∀ x, φ x) ∨ p, + take x, + or_elim H + (λ H1 : (∀ x, φ x), or_introl (H1 x) p) + (λ H2 : p, or_intror (φ x) H2)) theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x) := boolext @@ -622,10 +704,6 @@ 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 -:= 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) := boolext @@ -643,6 +721,26 @@ theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ obtain (w : A) (Hw : ψ w), from H2, exists_intro w (or_intror (φ w) Hw))) +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) +:= boolext + (assume Hex, obtain w Pw, from Hex, exists_intro w ((H w) ◂ Pw)) + (assume Hex, obtain w Qw, from Hex, exists_intro w ((symm (H w)) ◂ Qw)) + +theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ (∃ x : A, ¬ P x) +:= boolext + (assume H, refute (λ N : ¬ (∃ x, ¬ P x), + absurd (take x, not_not_elim (not_exists_elim N x)) H)) + (assume (H : ∃ x, ¬ P x) (N : ∀ x, P x), + obtain w Hw, from H, + absurd (N w) Hw) + +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 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_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x)) := calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x) : eq_exists_intro (λ x, imp_or (φ x) (ψ x)) @@ -650,25 +748,73 @@ theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ... = ¬ (∀ x, φ x) ∨ (∃ x, ψ x) : { symm (not_forall A φ) } ... = (∀ x, φ x) → (∃ x, ψ x) : symm (imp_or _ _) --- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty -theorem nonempty_range {A : TypeU} {B : A → TypeU} (H : nonempty (∀ x, B x)) (a : A) : nonempty (B a) -:= refute (λ N : ¬ nonempty (B a), - let s1 : ¬ ∃ x : B a, true := N, - s2 : ∀ x : B a, false := not_exists_elim s1, - s3 : ∃ y : (∀ x, B x), true := H - in obtain (w : (∀ x, B x)) (Hw : true), from s3, - let s4 : B a := w a - in s2 s4) +theorem forall_uninhabited {A : (Type U)} {B : A → Bool} (H : ¬ inhabited A) : ∀ x, B x +:= refute (λ N : ¬ (∀ x, B x), + obtain w Hw, from not_forall_elim N, + absurd (inhabited_intro w) H) + +theorem allext {A : (Type U)} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x) +:= boolext + (assume Hl, take x, (H x) ◂ (Hl x)) + (assume Hr, take x, (symm (H x)) ◂ (Hr x)) + +-- Up to this point, we proved all theorems using just reflexivity, substitution and case (proof by cases) + +-- Function extensionality +axiom funext {A : (Type U)} {B : A → (Type U)} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g + +-- Eta is a consequence of function extensionality +theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f +:= funext (λ x : A, refl (f x)) + +-- Epsilon (Hilbert's operator) +variable eps {A : TypeU} (H : inhabited A) (P : A → Bool) : A +alias ε : eps +axiom eps_ax {A : TypeU} (H : inhabited A) {P : A → Bool} (a : A) : P a → P (ε H P) + +theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (inhabited_intro a) P) +:= assume H : P a, @eps_ax A (inhabited_intro a) P a H + +theorem eps_singleton {A : TypeU} (H : inhabited A) (a : A) : ε H (λ x, x = a) = a +:= let P := λ x, x = a, + Ha : P a := refl a + in eps_ax H a Ha + +-- A function space (∀ x : A, B x) is inhabited if forall a : A, we have inhabited (B a) +theorem inhabited_fun {A : TypeU} {B : A → TypeU} (Hn : ∀ a, inhabited (B a)) : inhabited (∀ x, B x) +:= inhabited_intro (λ x, ε (Hn x) (λ y, true)) + +theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (inhabited_ex_intro H) P) +:= obtain (w : A) (Hw : P w), from H, + eps_ax (inhabited_ex_intro H) w Hw + +theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) +:= exists_intro + (λ x, ε (inhabited_ex_intro (H x)) (λ y, R x y)) -- witness for f + (λ x, exists_to_eps (H x)) -- proof that witness satisfies ∀ x, R x (f x) + +theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} : + (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) +:= iff_intro + (λ H : (∀ x, ∃ y, P x y), axiom_of_choice H) + (λ 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)) + +-- if-then-else expression, we define it using Hilbert's operator +definition ite {A : TypeU} (c : Bool) (a b : A) : A +:= ε (inhabited_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b)) +notation 45 if _ then _ else _ : ite theorem if_true {A : TypeU} (a b : A) : (if true then a else b) = a -:= calc (if true then a else b) = ε (nonempty_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b) - ... = ε (nonempty_intro a) (λ r, r = a) : by simp - ... = a : eps_singleton (nonempty_intro a) a +:= calc (if true then a else b) = ε (inhabited_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b) + ... = ε (inhabited_intro a) (λ r, r = a) : by simp + ... = a : eps_singleton (inhabited_intro a) a theorem if_false {A : TypeU} (a b : A) : (if false then a else b) = b -:= calc (if false then a else b) = ε (nonempty_intro a) (λ r, (false → r = a) ∧ (¬ false → r = b)) : refl (if false then a else b) - ... = ε (nonempty_intro a) (λ r, r = b) : by simp - ... = b : eps_singleton (nonempty_intro a) b +:= calc (if false then a else b) = ε (inhabited_intro a) (λ r, (false → r = a) ∧ (¬ false → r = b)) : refl (if false then a else b) + ... = ε (inhabited_intro a) (λ r, r = b) : by simp + ... = b : eps_singleton (inhabited_intro a) b theorem if_a_a {A : TypeU} (c : Bool) (a: A) : (if c then a else a) = a := or_elim (em c) @@ -732,4 +878,17 @@ set_opaque not true set_opaque or true set_opaque and true set_opaque implies true -set_opaque ite true \ No newline at end of file +set_opaque ite true +set_opaque eq true + +definition injective {A B : (Type U)} (f : A → B) := ∀ x1 x2, f x1 = f x2 → x1 = x2 +definition non_surjective {A B : (Type U)} (f : A → B) := ∃ y, ∀ x, ¬ f x = y + +-- The set of individuals, we need to assert the existence of one infinite set +variable ind : Type +-- ind is infinite, i.e., there is a function f s.t. f is injective, and not surjective +axiom infinity : ∃ f : ind → ind, injective f ∧ non_surjective f + +-- Proof irrelevance, this is true in the set theoretic model we have for Lean +-- It is also useful when we introduce casts +axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean index 7c50c8c1d497be3278ecfdef185e2d43d4096be6..f2f432c9b9dfb733201f7beabee4574e73ec7661 100644 GIT binary patch delta 98 zcmX@ceS&+#QD#L%`!OcreXJB;AOL5E0No4>4K(iE- delta 96 zcmX@XeT;jE%cl_mXw90PXvHWIS=Y6Gr&dTeY;jGnPuVgU^?NqVY0ThHbZ`N@`K zAUFY{W15l=8z>H6fyOOq3!(I!p3|lfXu-B{a8oErlbq578X8D2q4e~RHVG~1{r&E~ znb~=(_k<3N@66n}bLW1|o!Q+tK31zXw$#UJQT`X#w{0Jvn2J7Ln`qR=qHC)Yk=an4 zisr?U*)%>CRmbYp$;iC2dta33kWD-5V^j6UWNj*n8-jUWl((=tQXL(QHjGbIr|RPk z42aD+k&%Djk4jQN-L`WqKs}qNYk`^;P=(H7j<#a_fU$-)L=1lyXU1 zYf+b}Vn7sknN12LX3hBcn9xAA2SrSTc`Cw?4gagn`6dKY^17I^gP zqfTTPtFl={5JiD4V?G(lfAggMH^|w-sCs>r0&m{r&dr-g8aFscA!tFx;2xz zJ~W!**m~m{H`r>g%dCrpk|l(J^HH2Kh;lKC80w=6d)IHYw8XKUL2P#9hT6pV zgqy+}A8RYx%5m)8Bs7Kms*ViYfCc!L>$ZS@iR6hOa3#P0$Mt5#zMCme@ zaqK)%{rS;=#Whl2COk3bz`yJ3v{%UuKs+?c`Ic`Eu8>00Fc41ScGImJ2O&Dl=@tpvh6f)@Z(2U`Vj16x-EykZGiXRwRNu``$cChsc* z(c^vlL~XR-aai{tsGW=g!811;swN-iu=nMUF5Q?w@b_cZ?22MGzF*2c19!m;+{!B?ih|4U)1IJTLyt!r_^*ekoW|MJPuc%0 zP_>8SU4VQGJ#UoDBqY5HxU*Z;f1Jky66F$$7L7v!t^GLYq61Y9HVpqbx4L%b$|(uYKc69XkN@d6srOHCUJi1dUBKU`cccGorXJu$MP=VmCcag)+&l4uoiGm2fC}AmVr-iYUEc)uJAPtaS-=n7XHjQS^VJoI7HqnCDkZF(jX()f7KQ zA+I>ME4QM4OKK^nokkr_ z7GDF%^IT)&8RS3L1dKCr#a`@MPSWJ^W`G*7K25M=Y$8QJ7bD+nR{QGu16TbMCR3cTl?Ghf&ZPoSuRtTlIdlGn*jwD2fkA5rwA=cBvq>%L(#cjg#9kEKkM)1>Pkc z@xHmU5d9paN@a3)ps;-)eODli3WkTl`c7c(?aYKV8(p%~mgnqD&O$kSF<@;kCcG2m z)V7r?$13_&UVVjNKaNLk_N)Q?mc5pu(WuJ>-2$ZYz4nLbYP;8xm;st`(Nt$>4Vgdm ze4CO=F_75)@zu4`FkQcjg7r{AuY*$OI}Asf?n6?+$ss-pQpFTTr0PA4DU~V(N_u)v zbStQoOZ8`*pw&N}NGMPe0~Ei;0j=`AteEh?GqU20$j`b8Gc=29N>0_*2`z}Yu;L&)L^mk3Oj{4NkNA|JEzXwkv+#sF)2;n z*9aKN51$@cw5|m{NSSpWFQ~WR!&5x`OFQA8V5eek?hV~A_n|tfB2z1um$w^gCp0Hm zUfs|SmJbEyl~V9x!fY%@BIQ)D=(R*u{HxI8{5ibCFnlm_Ww|9OyN)!}5U*jOT>>(` z#A{feMjfHU@R?C?hha9N=c+;AJPZ(v$}f7jD4QOe525>aIx^Lg9)rRBX_ZauW| zQEkqfo_cSW-rT6^c|n%W-8kRshk)tllu|WUS`O6&*0SzIz6^EqRSc!)=nmq-1~+<@ zOACEVnrB|4q`BRfYWLw_s$Q!|+^N0mX9Ou2XHKAML|vnkvWs(hu0~uV-^2v;T!ZXm;d7t+o(5{LAq?d2~42JBLje#^kAe} zQ*^{mNe{`JV>q4Fbd1!*ENVIOm?NH1S`H&UJ*F}y-%e~7v*-No9sSI4!{-L(yTo^S zI(KK?&cA~}-}7cgJ;bL-4N+OV2zo9Gm>_#M|BCK^q5lpESnz{@6_0oK+`zn~SQtwc zYu$>^e4jmm;e1aT&5P=(xK)t@1j-7E(33jG^i&3!&tRx`lA%+E+Zm@Fu^7!Wte2Cy#Qkr)NqQFq|RYaxeJ`|mX1^4C$Qbt)8*^gvW^aM75xu^*vFpH>nR_7^W`i5kgq^1@Nb{vzs%qSn($ zx4HEEf+vF52E}r?oTnmPQSbn~iHa^FO$m^kR$OWU$r0tP35X`A&yLS+ibw+;kdRp= zXUvY|&SZM|M*P7x_(G4D9?8-{fjqy#$XpP17go$A8M=m0_`AGYbAEaQ!W}5`8!LcV zWE7-Z3H_gbt8uWeXb=fFYvGTAC6he?=j_o-7t48~dh5tJX2R^rxm?b)fHc=+0CnY2 z=?6TXhC!zXoK!HpPpog*Y?1=P9iHS+AJ#a|XVb~W(vS?HnGtw>^94ejvXVG>>rFyO z+YA)0E`RZI@ag1z)BTL(TSV7y#k=>-$HOK_=yk0+pc580ff)Q{ZZw^6QiZ?6Z7O9nP4QX zn>_Z*i-Ph_bE7umzb=Rw)}X-40WD8U_1w-VNWmd!#S4qV&ky$&iEfgNg-95=NQz_| zd#qQfyUwQoX`|)wfI$F@F(=a?rUj&IblIN&lF@hVzu;^sXzCkMmVAQyv1E18Qz@)u z45HR($2qAac^Mm2kRZuhNliO@Tx$O7rSe6CzLMQ0dB`0tTFv!RKAb^!&O@AltuqdM z#(~^0SK}4%9ry@^L@sdMG`(_B(_|PaFkkW+xArd9QQW3yymLWNUBAB@;8vJxavO)- zfCkq00-}sa*1mOnP?`(wCvxFS-DP4~2O^Qalanu``7OX8dKRPLbmU6KbcBr*6Y~W1 zPM%Iyg309bPP+ZT1((VFXiRuqwTdx?E2Gyo{2-MeD%2^I%L2 zJ{;3`M_raFvcM-o?s1(XYdD-_UjWGDEqMr_b^-F<_$Uxn@3+i)0d6yf;Zqh3Ov!$M zaMq8K{cdhrhYI)GL?;{n>_8lG@+kOSfs*}1K$@TIr-yykA^ao3L6nOLavsWv4o~S| z#^kSbLwgoj?xcgKEZ1oiVIi>s(V>+lelkNJ z+l@Mn9{!#j1kVgfJ~}DefSWu6%tM)!vn61TKdS&Ht#NP;PcW&bv(~4-B`u*(%aO#H zv1f4WFg#jm&vcv@j3snoJ;VI~IO?}AIq+qGE4he&W2>igsV4|I$;%Ljs;~m2eiSen z{Hq!SknB+fT3Kt#N$j5k!Oux7Qt~Rhv~F8~>Q*r~X5efHMR|mWfoi(+B-xoJsuT%LQ!^!{A6VH>fE03~t1WVp{1`Onb|oIs zVK^Vu6kfq6nAC+|TwVm>x7wJh%g03JHm2c0j7(w~S4-(w4JF62{v*txR`#j`UjwLC zhV`UbnUx(YJ;{&C0?{51owKyWI}BxFyk}5Aw}+`2c_D~lSM^>Jg3{iy<7sphG!2a# zk4%z7sB0s&HG{eroos({h>~K+Vx#f!WlZWF$EZArGdWa_6p*T5QsAfWA-)YvX&)L@ z9Ya7WHC_#Dbj#ojmqBaVwBXoNi^2Z~ZpLL?(d=~)3U zXJh0M$IFqTKs1fGqn$uN7Fv|gEK$N#(q91-YUS+W)N0unt*6o9W{&*t(&GEId=)t| zHZ^jd^J=m?!Rd~(;|-a73-wq&GsLL;Yeyoom&ag(TORpKFPV#1MlS-_^dkZXR2N)SGxa(}Cg(wowo zGHmEhQL*U3D~5c=o^GIchJaM+Y-;DYT1vh^aZVEz1wZKU&eVbPaZN3pIPRI9CZ7VO zqxSMw)IFzT5tQKxma6J?cELq!iuymm)UeL?suX1OQ1BPhpN=v_J_KBxaPvF?kWFj; zTPnr0W~$v$#W6!4QJh)PxISUpzcCJ(N&7!BfUvF(i^dKwQy4Iv*^wBa}B}z8*SGQlHMoe{Uk|w z%mb)G=yo8Kl#XKw=~}c7*bAKjPe>pT{SrmFgK?qMcSUg0-_nf$%4?ph0k!6=>0a=g zUW(Fl1r1I?WI$uO0f0_>k&cwi@k4@C*nH?#Jlqz=xkV+rRP(PmF+^t^KNvl^A0~Pi8ev0OH z)X7W*P}wOzeR}TmMSDSo^LeLyHgc~_IUlkqowV$fpFX2^H`oaBb38L&e;ZbJa85z9 z>cfDy!mdMTWf%1soc_~qIwHWNkEYKBo|Pk6)Rb3TkeK2>UyhG{V5Y+;UI_g0E%s0$ zLjsnBEjwRw1PENjf7!cR~7v;eF2T%g2EZfefEn?rT-*2bGfnrLC)_* zF7oGv4#w@^i8xt_`UC!+1G(ode|mf(IrYIjbBz&S!`wh_@8;%~nB%dgFX~qMIHVt+ zBt`COCp(aVPkr%JY0VvwPmcWCHFUxH(t{`tl^jkB{v$}q-vjd-fSxWnVJ5ufN}+K* zfzkL&FS%5YM}avbMHJfh+s;;?SMD0&bykYJCw<$>-q}X@@x>f$1EhX{nGpC|4s6V@ z7!qynaH8N96vLD)pTM}_;bRaKn891pci3%n3z|j-WoDqB@!6PO1&|NA^1FY?>sCWKQmc7< zDR$|O6J#mmG+ABbGcd;x)3^UYF#(4Mmsicu_EC`j3RVTRt)D^d-g%+L8^ zScWFtYBaP;HNA@~p9WQmdJ&+aQvsvkRPrQJoC@Ecx+A`SIh;QQ)!+wuFoCGYUF5lB zh8b=R;)~x0B=xNG9EihtRw2SNfNMJ@4}z64#=%_v70o`=ca(7;V~(r4{l4}{Jn(0iV;y>M zV!A_-_7#nBj#mQ|4&;yom&n-_(x|75Xt#j02ri^$dWt~R3ad?O6an>0^5hXu%5MOj zNDq`(V-4=iqucTxJ2I~qrNPE@0R{%!k@nDl(4FdwF*b(iO&Bd_HqVq%x+NN?K*pCa z3Bn}NEhxC;J2JB!6|q*cj!?3-7@l=0rB5GpLj;`^p)b69&Bg*=xWJQ&LJ5&*N7*)O zBDyNoQPD(*8FhMS&-^fbN!ZIyCp#`aG*H*uqcZyX1xVYc2UzqGDfo7F3;k`yAgF0Q z<IiAT9wK+R{?Z9kAf9|`a3<0e{#;M zqKRH0zikC*CF=YUzW4%xvfJ!$b9Ni$K)#{EZDzGG3RKw?W|?gmo%(tDC`jiv3h8Ed zqP~8Xf%Gi(yl&uaY?fD%0Dd`ZVu%6j&y1!Q(~tG{ z59r67!*HY&@>H5(>puWT^3-Cpyj17prXHlz1EB}6yfpAWBY(e+h+MMilHPb7aCkP3 z*9(+hOaw*_T^jloYI*A~`%+=uz`U%mVp=ShK$AhF%O2^LU;Gn}0q?_2ukeN!7RE4K zn%WV-ssc4&>+hjvhe^Q2PHF-is;3SIPKh3U z_9r{3{N!82nS=da59}47_HzrR&*sSmC!l&fQ&NfT;@XL@3xj$4lRa!Dkep2u`Uv_| z{2vXZwHLVhOe3@=Fq(Z0#pg(6NWh#5IL+`#FS`eg_Dr!tDseo#y&9!xpND7SUR6FD U@T+oF>vh%zwbB?}i=R>cf9ilo4FCWD literal 22872 zcmb7MYmgnqb)N2-k#;wL77#eth%CEWz!5k?MU?~y1tcy=fLU2MWjkfO?Bhzh@@iM? zt^ff}ZWJm;5=0BeV6ako@d(c2M>GSH-Ju`P~q&hIVzBW>gvOiPXyk%^BGWv9Ne6%_e-83*B*=q+T zqq!!sgJYA?z({RiBC<#B_PB zVt}!WA}jx1hDuyO-Mn=qK>c;1UIEmkfGP|Zi7vk+GJ>@PsA;k5$c~4-zTxWnDB+Se zRHHd|00Sa3#||nG+m&NuBSHh!b`*wS2f>9XQ?O6QOmU(W84napTfpFv9gjFJP9PT` zGk0VX|3qzRgO#+wicZFo6gw#1^NHSGoO!vDCfW&+Bfg0$=RvVz%5Y%ytxxwhlct`Z*|mqV>?>C5q(0{t(nZt zL!&K@t&MJSgLCc8v8$tAlhJ`aM4c!W^rGxSVW2!Juw%{UEog}rpv9P+zF2Jkt<~|d zaW{cCKH!a{+6!Z`Hg9asTqzOS)dD5zNV8Sfo|6{un2D_f%i%CJ(Zbl-vPB|IY`Ipo zmz?xSwIBA@>`4n_TU)T?mA^1TO-p?sYN1YuUOS;JUNOx&{Jr?98RR!TT~n z^myMgUL7v@8`j+mYNw;1tEk~nU7S)hGl$wc&hdroY}#+-2 z?UB$UI~)JT{NUi)l!B z^=Nf*s5%wc+4-tecO==;So%D%0{b=;m#6k-{EHB|hp-v-G+ixW$FggeLTw&)q z0B=XZwREC8Z6zTmCoYRrGGT#A9fh|Q(VE!b-f*(t1cnO`!?lT_@!IB^WI;$RR)Rn@ zCyy|UQMuoBq0{p_RJ+5lmHB8FI*Ch8>3@A_Qw#Vwz&Tv%CjhGGejDJ!Z2cs_$0#8B z%^2$3Y^m{^eUn9(XolJc{MoZn-id-7>;%-ekj9Vo3lk{BC7YB<0kgM*dfg60RSuvj z6uB%vCKcI*^Jv@Hg-6`h(u)CIC_J@T)ET4 zE#s}+hIDOgC&z0y)dn)hDG5AJig!+q4~#apGiOz#(5dyHl>wW!)Txr}0c%-a5*YF! z^mKSjX%a&~yc+{ZT=R-L>JNcS?o=`V#GZt z+8x)+Q76OgT>C-PJr#4>a%t*T%ke!l$uj{*VK5-tt7KHo!Q%_~On`Fa)>u3MrwW0On~=(66D#qYeE33Q;+Yv#cMm|5>1FPheN?py#b} znS`Xb0e5=4`XRbicP;?Gg~qpMrtj9;hY@a;QWO3`8<490euoB~EKu0n>~UgnvM&0- z(3tFkUYH)lxI%0|eUW37E}$;Cg{WL518Peb0PgaD4A<-1J&@GY03AZ{day7ycBsJ* z0YTzJm=T%d1ABQ}Cw9}*R49|o>OhF5Rtblq2O>5+G5#{Jq@(CLxm?p2`4beOcTr>Q z#f6zu1kudbkhlq>B4x4=vIZt5#)eAtHD}s`gj+MEO`2Z(VdEn5zZG-p{&|xFxwENe zx3d*UVBPd`0scnQ3xqBdUIc@|n1wkT<~a0|jc!lWdB1K1i-6==-67Q55q}I_V^N?6 z(mOP*8pw`m<0N&E;+B9(%!$p`b6zQ5SrEhM3X1NWWwi{i4pm0}>ZEFxDZU$ZGOlvO0}&Tk7K6+R%omz2&Thu> zV{~N!KX4y&%FO)a0@83ue#lD2^)Lu&y)I;_PIF-!z%V>gIqF=@9bNcqTq<}eKrbkC zp-=-(09q8B(UN;6@XfJKkj$ru+RO(zcf?4M#Q_dzHo;F(cn8rNa>6LJ4?WgH0^+a= zD42|{!O8Y%aN(%Ze9Kfxc19h!m2`6einBRw9Uz>`tOrD?9mpdXBtF}ui*subm;A?~-{(Y_Rl~<7EERH`8y}x`Y&>xV3siS$Y9Ep^< za+i7nG7q80Y-o&+IygR04b2zP{XmNTRVe&yPT6&&UFx|_yD)$js`WbR^tL^K!m#`x zdLQbAaYnpA(PdFV^8&WM0Nl^d$W|P(*azZt9~P`axM9v?9&AHvQ*_pOd!@@fiefjg zoSuTjTJ?T(W;Q|UODL`ez3^ngE)}G9)qzDp-mfuo3=J6{fuueM)O%*nLiA&hDwWB7 z3~K@S`pi-mXT`Xx!z3?qEOX_mfKudJSFe&6dPvCg>zF3y8%5K+QK7 z<~1tyAbLYi{KKjvsY?Ss`&9^>EL6=KK$`i^!jV>eU{r8UFmIx2@k|(9;gnEDjnm3;xmCBQQi|>3~v=b%iX174U1Ip@gVQl&-d$^Vv zL#7iZiH8#X8Auf+I=d6_1q(5f{8PTF;JeVMNyyyX9)%OmPbr0h1d z-RPO0f>M)qq|LmbGozo9>tnr+I)ff4hg+9DRod(+z%)NczjB*L7P)PfyUD?=lfE^F-C`yP2%G3NM&ovEI4Y9xruE3HT>N z#{m=`EyAGnY{a&$25@~*mv%8QaRM;w%X&y?Uyt-#>Jv1h14XT6<~6O>NIuNz*=SEH zqjdeWl*}f#ni@EvTs8+beLZ@toC$xvPAH?IN^$6#*$>qTFPC@|Mb!D|S+t{jP!6Tza_5>@f9Lyz<4@W#S^RJ!fja!XQn9cgIPT*^Yb z1XR;fUDQ!We6ha;C`gU%I`mxED<#uTE{c-Ru5I%0WYb+Wq7G2|(QQg#e|Sg`F?DF(G<2xx=3Z1jFmr`AT-H3(XaOu?0k zCI9AWkfJf`*5G)#8a=Czl^5PIDMO`VxTY8!Rn{5|I>T|rElXWK;A$l>FQ1XC1f;p|sM#>^45888eAz!lU2jC{0BJX? z0)bsF9d;#_;=C>DF4;Z3)O>ckr|xg=M#k_m>;kThXJ*|eajMIv4^zkBm1x?@mc?X4Le&AWP?NoNe_@UIfBxa}L!6 zE@Qn8q7?agsM|+Tr|0Mn;yivsMv5c#$@E9xOWMQVx4;$_ftQNVty zC=&b6Ao88r#U@RlxVC%`v#%(_LPi}$>vh!WDBlGXZol7_Hv6)A>is~_WmW)&o-|`j z2Sau{hI%I%`d_%6aoRI-_rYrxBh~ej{nH!)%gzxpi%~0v!>R!Jat8^@+o;}+L^ET}Z~bUgSPr5+WZ+8xm94*Y;9n7JiZ1e=P}GaA zF7`{oM~bGc*qFH=aJo6k-vs@K(Dg*ooph1x(GBAukYLB!^G!g9icv6PV>d#NKAY?Y z670`(Hbsqip1fWZvd?pF_D&|ocDLDU&MzdIAa>0{^ksP_K+aPEq!%VRuMN~3X<7Ff-d1Nt= z=kZtOiIAfFiUYsuz^@5tmgrl$ zV8ZvCz{lg$oZ|Cq1GBJbjqzz9xKxUGos+TiMWzpG97>}hfxQ?KN}zh9_Z@&2JHr^k ziy_U4#<*gsnB_g@c`4i41!C2UcyCc8tya0(7V%gk?$L^p{ygh&{P zv?1Qeo;)j8|LddxTf~DY8LDU0_t7BgsACh*WqbZhMvvKlg;Gp|(f6V1QYZO%BYKt< zJ(a?WH$c=H?Ko!zW8~Fq`~z2(caR!(_I0WGFO$kg3i<+ei{v45wCED9m-68Zx^sSm z6R`D=0}ng!S%8<|h3^~jT?vU??79~d>_yo{kO<_RCc{X9`Qq(v?Q>X1u}jZ*yv9`5 z?`{K`DpV5h;*eX=!1_)=lo841@7Q8@EV!S@g|BdziDfm2L>KuBX}sR=Edvz!hOmn1 zd5keB$`>5?_W&;flksOsj|fyhxQxGm#+VNh@<#V&@HeG1P$pkx&zW{4b-ASek1|Tq zR7x1@)^tPvmr$cy=U@yup zf}DpkqQg^um@)oq-OwQWY|E|ylJ^X6)+oxC_6f#&k6{`rnbYVNN@m&E2ex8vVB{rR zxV@Pok#);Q0xF%a(~=&B=-a>)haWu$AT_PIHC7crjmD$8O5o2$ot|-*hc9ih9u{0` zsY7+q=s!Ro+m7+{G0YV21J4XeJ~}Dq0XKdInEScVRRWfz6^_4L0nBX8aqOvcloT)jHwIj8SYi!s0+X5!0!RPh>Q3>TRoji zJ>H4pUm*@vVFgI!6efd;Y7juYLlvmYMhg{A>>s1*=Oj5&{O|12dfuu-sZkvtsP#XJ znDIIx62IOWiS`q}fyL-{s zyNMHBZD3_bK(ntECr%P{7|sVZg;($~CUpk(Z&C@u@4)C}O+Fnew=oS5Vq_A_I3;+K}lM6Jk>Y2c&`|LL}myc*c(mcgxH617vw|kgOmj3yXf7Kq&EH$BSN^=6i&u5mT)M0n=_S=lTa(Y#i`Y@ zFF>@f`Xs4lL?QKNESUv?rIU ze-$zhsFeCUWt85Q-sCDUtNTPHM-MMyu#994g)_aY>Cx;SL5=SuJ9W@wc;d$!-ibQ6 zZi%p_CQcmp%uQn+5RT?ozoP6}9g46%Pq0*!#v@t<7p)2E{{mAZ`MVBe?9kSqNNds$ z1J&$#99Z2bDC9h;`5$R1CN-0-4l2$>l??0I;j84#;#AG~nRDp^ehOBU)t@===K?01 zAO_8CprL@__oT&lCXucDL`7NBuRgH}#57a?KTzYG)N}>{PBwX-gZgGE;yr-I3(g=d zQ8MDh%4i9_B>tNdZrSKh*0}mM5TNKP#o&?L3e0U-x>`6Xdv?_bCchMnVEv;l*AJ53 zH{ognDds_u31N-{=L(qcHJaoywD#oJIX#|`IQADD#R<9y1`DOWE7FrxbQ^&38jq>~ zHD|2JPLNBk^oRmcgHsS0)YZ|Apqs3vT96LVy^}S7!tI?3a8JB75Hum>>xjt*6&Adt zl7NzGZ3@usWX|m~)L+YeMn)-l?^>GiTx+U?$U;U9UB9jwv$I%p8&BXbC%dFT1b zS)S*qE5=7P?Z(kQ+3R|!3t=Id z0fL<0i(C}47dl`DN$@XLF?K*mw%+?RM*3$*d91!8KaJPo8r%~)fv0v=@d;vgD?yLwF{6~7?C!|Qe0qCg` z^N)GOl^jMt2)DT6Qav68<^f^`X85kN6<))_0m93y1SwkbZm*PqZG<0P%)&N6>R+Vb zHqdljV=|~4M3y_4UlrVJct5XOb(T3F?j~FwbCNGktruI{wNGfnd)){@+MIu0JPW?p_=e% zI?Qo_pXyu7;8}O@Qha^tO8nr#lX40Lrl(4gyjK!7Qao}>m@xk$Hzze=y7I9<;&rP( zETs9MxACcNu}gQHAWI>q@vSD>*AJLA+bjhL?Kz!ajAALa?DXVd=@rlj zj)b$m7M7v$vm}55u9Mu$mDf>6+L9tU$g-}6Qvt8wRPr2BoC;r_mLE&9XP^jkSuO;q z-Cg6kWQG~;4G^C>4@l}{A9CPt2$)__VAU{nLD7t&lQ#}8p zCA~s!bRq-fs0#&z5g!56r|H99z}iCd^Rs1VJsg4lgh|P^VgyaE&M}$e>TW;P8i_}P z^ct|H2Paa7SA}*!%$ctSnEgNwad3s4epnjylo4$QeF%XIX_}rQAP-E=;~Tgz>Xqcl zBc7Av)F;o$87qeZ@iLXVD<7%bbP&1Nm>drxr9HTrV|Svj#kli{#TflnqiOOX>DPE- zbG2waOoA{;^!q5dgu&mMG>1)T(;FT8n8Hw3(N5;HK70Eu># zZp=-@i;}@p24Y4tJ+fzhn7kr0r>B#hx`4EXw1&Fg9;po!;~`D3^|J#RulXlTu!;W0 zVi44{9x}*caw906D=q%{PCj578{HtcP-Va8Ct+$7B=CTAKq{ME1<)zn>MH>CH+i}V z=2tGL@qKf%3?P41&s-=_x-0*w%{HqX$QM+&%N!UT2C9skX0|?b>aDl`t}mpU?nd95 zX$DTAQ$4Q@V3p_8bT`*P#^vV%iwjIv2wpnXW{2cOB!FK`8yMoD`m3SI3UyJcn|{nW z;6y2>Y}dCV-jN2GUuelIbxv;TK{`DU+VR56DBfn|Z`BczOSW^Q*IWS{L-0z0k`+W? zjvi9!iwDzaAM#m0O@0G^6P%WvDDKk-1G`>cwJ!x7}C^=09KVg z20Zz}ubMoHQpT@Ci-I2wrmSE&Sq$(dlMRXMq&!I#sXK)Uq79wE?gE0_NRT<09H}$y z=DJJw(FsS3;Wdj@oN4|HT?pv!o2CZ?FQz8Ip?Yc`Y{P8{nja8Hc2fCy zw}>+b`@J66=~dm_Le06L;txjEGbNSSHm;r2aRa3v}betBej`fnQVpf2u%4_5c6? diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index 47d0db100ee6ff8bb1fe7091a6e91cedabe2b61b..431b4fac16891182e3728aaeb05c7d944a9d9e51 100644 GIT binary patch delta 14 Vcmew&YB#}*!!<9(Ei)&T0RSe21g!u7 literal 2804 zcmZve$!-%t5Qb+70|*BY+awXo09g>?0D%Yy5)vR#kbnc?z;cL&;IKKiV;ht_0UVH6 z9sxKYmUpE8uRQL~fDfg=tNyO7yQbY~HOuzu%T_ZQ{^FNw-A->1y>9l}%~mvA-75zb ze9>Hw-j=;6StM4S0={uqDQ-8XZ`2ZICXONR;6=q1;)Xh8DSzHN(w> zIAdfEoIsnSot4~W3h=o0shVg?B9#c-WF$LYh*XBrRUOwNcE8bO-8vpi;Z0&EVsve3C^shaN@4Zk2|8|Mg^A2Ei-~u zBGvS)z0)9Q;*yEc+w&(%GOIEcJU&mQ%h^?kh@bfi_tma91}wcjv<~ zV(0L>Yil7fLDEkI=}aNyJ^2*rt=%`GLB!=NZOL4;3t=>T1j)lknfr?Ts9ISy%Tz5n zPp@Zq+Rb=y$e3Y+I?9lqt)CX`OJFI4Ai`;D8C;1u=eEDOwkGv(2V|Zocy``i9^IMvd^87^r@0BWd=w6S)5w_ zR)h?}6xE5-?!xt&t1Z!nz0hQhoerD2|=D1Ic19WGoa6v|Vj2N6CfFe(PMc z%XWyI>;m3w4x(hKIb4gf%J!%WDE3pfn@ zuxN5L(#eag4hkU;z3vdpi^KA~NOVSk7*b)Ca%36d5LxOYGb)j>?L=PgV@^kA;jOK> z9vp6u&X<{VKcURzd3tM;TX^Jg6P*b~Pf7s!Q^Mx!czu8tdP$~?n`o7RR2z=nt3qrq!x*+r$cUdjExRe3D%Yt`Z3)!mZ zs&OaSx}lqqI*ijldnH5|6OPS=#Wto1MS)3DDDEY~q4@VCS+Sc@*Iuqj*!Kc8gH#RcVB$2FV2IhqUiecQbx z&Se7K^W>c1XeQBl?2s~M4*N+2wfb2y*Xa`GlQq|psD@q@`VaveHT0UON1?6=t%0rz zoddlt^r!Lw!uT|uc;9UKr;pbXobTmbbb#*)grwQ;t-HyhGfWo#TJK8nh86oaf#4*R73b~Wbz(v9Z+%P_PZNjCNuhea(OfJ? zW)7>-mymjt2U+t$S_x?wl1XmUNy$T`3UJV7u6s`Ph>MYzE*4@zzXfIHg&3AGCZuI- zT~tGFdi0jiN92(yW$31;wQ|$@R`^r=KX9D>4x)im?r*%b`A0Z)NkOy}XlZ#sU779F zy&T@@>o=^~ZteS9Kre`sp*6e-ocD@@DejLX)`CjI zsh6Dd;yzaMa9TbL1>o3jE&mm$3Op{!;1Ghy{8I>8H!wFJi0CywE@Z69e%Ct4sP}Kj zp@5e4hz>mJ|26sCEy1 zA@m~DFNIb?zj9c-5A=@EZATJ2vKT+-Ky)1k+d{zr#O})&?-#q|e^oT%^ao>`;2{ZV zSeo)}Pwi7;ZB7bu%9$b%?e8fZk)?PFAx>W)LoG$ zfq!eAQ`0j8OhR$Gs=B)RR8>RLjiY|M(~V93*-q~uNi*|3PWy4!CT#qj1y=9@Y%q%lB8?QO7DOQ2xskDl0{i3>0@c#!UA{A2Ur>t zo$!q9{21zdWI1bx3OgORPP=W)43@(<6+fm9VIjhXl?eDMI-f@ea4u?Po+v6>nQ)=uPQp21d7 zavzSC{Y?@vMf}c85HvDDJG5|=${g7*m3F9DkohI#&EogrH&UxfZPB3&r`jg9zC?4f3Y8CQkNTbCI32{stxB(mMTFZ)GE*8h z3j@Nu+>6_WPw}c5)*Vp0VM;bz`=}qEWMnvib`el1Nqp-Gp)FOBTDS>=RW2LQjY9C< zCOb`V;HWcd%~3G_%vRI<{w0PAa6jS zH<+gXq)z4sZs2KbCGt;at5nPy8X2=$`c6l>MV~%D+Waxcv5) QK)Lw-zwYn7!9RKb0f8>SRR910 diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 98684cbb49d824d81a7e7b550b2f0beced71cff3..0b37c6f801b90b01cba5a3649581675470693a3c 100644 GIT binary patch literal 44201 zcmcJ23z%M2dG5ab^UwTv30B0O3R+?yjzmMWAQI#fkbp!IB=nraWirXkkbyrlVKRYG zt*9s90E-BVKXcZW>t&(1jSdB;(P(Y)ntqSLR-*?^io__}DdCojf zR=%~?x4!kQ@3t;`?fp-7M~5fI#=E1L`^&dZj9)N1wPiFb)@FHbrIr-yC#SQK(Xp&J z?V`=2YqPemV52tDV$*p;Q&U^A!qA4dcBiuohNrUP*vZMRVG}K9$;Q$1v%caOmGl+I zdSEy!49xqA^(-k%{8wcsZraRz%hDpxUq3lLJUu=+fwH_f@<=vXM%-35ye%s>PK}Or z(+)&8I}j}fkPw+k2icDAVK2+%IR{y1aTsVBky~IRdp44s-~xc1mSN(V)gxFyPLVL%2GBh%^8t2P`nv#2@q&J#QTyB5^YT2)IGImRZ5>5jR;iP| zVwGVM-lj-&A&QnFVe_(1`b}?Q@&2qkD63bV`EpgF@uBsq-Iw2x)Y0;XCq{sn z9TLVA_z(}CU-q@EPVc}2Np2zQUe@5_bk~;D+zG-uJd~^$td+}1^ zqGXE+vt;}|yXAw6A3}6b4FOpDc?&$;GEINn{mws6Jo0dQD8)5^VRUKQH<3YD7iZnRUNWRbJQSKqSP#Q<%Dq8 z5DNq*CZ~tSC#I(+BOQnee=kF_jG}oRz>46>09h3R^GQ~sfHk~+%hsup8mU8oPx&t+ z#8d)*Jqkqi6oBG&HNa&OIKa|Nd6i{+{NFadWqM1h=GCE7s+9s3=~F>OYJCI1VF|}a zmr_}#CF(nvr8W#(6zVI;OLmY+TFM{k^I@yHM z?V1?R0GusYg!Iiwga;`2z_?{3fXOL26c#xRom&)gJVsxYG|AK?D2l1g0Ob#in($re zcDrPS{!&In#>;BL>gwEJA`9|quvJEGC~}F2bEml3ioOJ10I&?)(3^vYLg(ssy)7#@ zOxheVIt@Q^9jYJ7F@{08RIfrsiHp!<#f95+D_wJZQl>efxE=`(qQM~hI)H7NZ*)MU zC8DsUNrAq(q|t(fO|mTP!0yu#4{f<{c=P7bBoIak-vn-MY$1IUl3pYGEW5rH)qjcP zW+Z>b!cPOd4ar|4*@=YxPmOMw>|QW>NR)P>aI>Arf!qoWuOu561C(~(62Z3uyu%bt z6=&O#9r5-BFEC$3q};M~{T2kHV}O9|fpi^A-JCGSW?HG@6hjGhzkqJa(d|Iax{b=5Xkn^*Z`6&Day(I1cjQMt_CQVzXqV<(0c*yw;1WYND{uhGjt<) zvQD9Pqy5JwAzEE!l>8_xT2Iub(%A~!fSxnx>5#-#B3%XA1{+jc84GuT1{u`Q-;cb8 z{-*#n^gjcrp??6Na6bs}p%&5)A$d3ogk;4E>#s%qE_DlQ>SG=WZ$^lg(V` zOu>JGDIbewuxTynY+5}hxEF_KB9XMZ(6u^chu5Pa2dfbyo5*5jAqvQ~)*liU2k_^p zl3cEf;70&zhW;qP$BFwffSTApZcy%43-1bCQaY)Kij8QJ?cEM^$;1ryX*V2b0W#6bGt$cn^56=|tKP$qCAa3vOoP=TLBsmx^u zK;eGMpnP9S=r2)9bIGaynk=+|b;bfj$%4wDKrU{`LOW+43;x1d)Me3A6p8VmkH-_6 zk#J_}j+O5PGzuvVjVRoMM79#8wucG~1IwSmf!_jD35gSlK+YU8qn$vI8F4C+8QqT3 z8B+L+LHWT1{|4Za=yXY!;Kp@H*V`k;3M+1tG4f1lb`)wMwk*fKPUF!?k>wa177Q)L zVjan7{9Xx|8~ZRHXhy(Mg6#x{bW%VDmV(mF7Vzh5R5APUEcDiYzBox5&f> ziRTmW@JLV1D4Z`?i+mM_&D9~RA{`LWM!+A1L@G->S8*LNdcGZ~c@ycewqFGXrM5c& zYT~{#f?ol+D$H*S8sm-9W(A!hEa1LuO>JIp>`C9mxpAZf;V(D0q}RSpwN{s(fjJoi zNRCZ>1cj%tTmE2JQ5Fa z>+4qMb`Rs5Hk(E@=_yR5V%`8MIDB&JZF5)0ZE#$&BDTLtWHR`z2>x9J{~n;!^$!C5 z&MFCZ7kgv=hN1X*8Eo2##?$4LcDN6^qCDg*mdno}mvke^`5%eI(tnEJKLZrQ|6)*X zYi_p{oQcAh1b|5?2mbFxiStC`{b@-$pGJ2Z$rmz%}864-NIZ7TLf||kOaSV4;5I*!BS#c=lr`NI)(lR8p#6x6QC6OYlHHg z#~(2=Y~1@WbPQVbW`6^!+%5soLyVkpNU<}mggKT&Vvtr69McTRa%rN49=oMxX?7ZT z6iH-=HDPM}tx*k&JrhV0nxCRfq9jOJ8V<9|!$v><3Yg_eO)|*)EbnB%hj>(L-j7nr zV8EdKUN+-!p4!eR%7DXVONcOda}HMz!yP?;de&jvN}y*qA`w&107z%ap9%2B=%jg)kwV2=g+c?I=0Z-Yrq(gVmJrDguHVUlEUu*N9;V;p!^qPM@xDW0fqcS;LH+& zAOCaEjHer6=}F58b9%lC&6o5S!&|py`9frt_QDvn!J{(&tseM%UJtJ5ALJcuix?ee zYjgrstA<1Ch;OcLb2vi&8OI? z$dba-{>b+@$Sa<^xU`3xSZeaG3au$zu{hWmsLNK{xF zl=K0qMqcpY#B51BDF&g&C)vH`4-RN` zZhT0aCw#92*@DvInlA_F zSa}KR#7g4-FJ%LTzBm{fvKDzcl{VKRFUM1HKl27t)FVx2j95RR6Gj>Z9R@Q6otLqy z(SNoKEqKyY^ay+hTV;$mShV9I>KtpgiQ)ChHh4J*YbII>P)r;WLG)Z4uONti47^Fr#v#Ch zrKS3ZGJ5uZ0x;zS_5jaaA_yKAbhLr(r7UWP1UVk*ttN6D-@O7Ya>imF8RRFUKuj{! z3w(VnJ;lJ{jV(*_)d1f_@KogYjRWes**#12I@1rNSLBvv?sy?7*#!sUY^ig%T|nzP zgoVh^h4;|UE=8WJ2+8DZS1RdK~;$8vT)I z(%%B0sz0(qLxv^!p|HP(IM{w}aj-f>vopYktPDpXvo6?#c(SsGopB)W{M5wGL0-37c#rmBumfLS-am+=jR!|WQ2|09Biy<7!)Zkf$8VxqeHPV1#nG+4QwX35=o|N z1%se)v9%P+H6$Cp}SpXvFjLgl|1K;+ByyuV(kLrkjo1JYNK*jA7BpXd4Om$ zVas#B&Hy>5iw}+!E(YYxamnT@P{6oG93gtHw_2T->(DqZAL?xxor(Ix$|3z|VKaz8^w?RPz>qI%0V%K&{~422ksXOANBM7-kLwup=fU!M88AjGx|c<#2j3 z?iZVa_76XF!v;Q`?*y@t~99Jo2Bmt_&kDt0&xFuL8ImQXn8&s8-h0ISX7lS zQa7yc2X#*4#`^5R=N6Vh}ogaF25> zn;%a0Bsbuu6O5`*C^a)r^CeaGzi;e68J;)ncUjxG0C$Ea>$BzddXV-v&j}*AgWVho zP~B4aA3|R9!iNdQdEpMrm&f{udIzO?EpVbhK7wpqN6NNuMPZa2sx@`!B>U5-4%*_H z3?=2Uv4b$;f^jx>APVe&6xd7bK>f1=)vzo0u5DAiD>cPrjtVqI*Gw@OQgVGqsjwVF-XoJ z=?Z-z;H609|J1S&P>A*#w&DdPL~n*AltWf6o9WW(Am0+JaCbF`=%hx&!75rJi|P=c zz$s7mqdYw-v}+Z`8ymc;jVvKBC=SpgIVjoD0;}fYqUu>g04musx zr=z$zbcuqt#IXf=&?Gg$hC!EHI&p5r#ns;PH)T&jDWR3z299{>Dbsih@=y!@FW(YJ zRk9!?AW{4&6Nl{9n$!uA*$eME8&5o%O%9_t=4jLMd@iLle|`o%C49XT`M}pZ8+@^0 z=u~{&H!ojHob!>d@0R$Y<`jpI&$&B1;Y z^uz&#RbB%mwbW3*fC4S_O!3phTc?xP5+q+BoQg!_`zk=Uhy-}*LQ9JG0rV0}*EmlS zD6Lg_I{Tr;(=6V{@q7&wHK%+%g52^{F9BYT`O8p{pmBK(OFxc$GP~4I$!(CF=xQrB zD^y%>mNu7o(Kniy&NQ3FvYlR~Q}xAT5PlOk$`VfCt{g85>%}-x+ZtS3uR9FVRLN9F zVBdjIB+Yvx$Y`a>=pRwK>_AI&UZt54dG2k?GozAJg}m&Efs%z(Us$$(8^qjZ&W>T{ zSYVLuYM}D$FgwD)bZzm^$cyuTAxIu!2gSH0<=31u73128<5<;-ku1;&oYgpPRR+&ikrvC#(=J--JUNxg~d4Cb2qsr_`?X^PcUexL{)je7wiwCU|}=m z?l?BtP{A@5e0p9f={R76i7Y-1MHu$W3e^ZXQPC z#(Yv$R#u8HO`iV*ES)mB$@AY>63lO&wL}yGC+;OJYnlHH&7(I|&qUsz*i_F9dY0E| z#&>%5=QYt@DJbE1Da^BmAV0!ZrU{}7J0~{YJ>0m2gs*!yEZo>w#}Z(W5k<< z+?>pT>a24XZm;Pa_&w%xU)-3`$%xcGi+U6<1U}Bou|3v$UiKY`f$lj75f(^N>)^`C zuP`g-;tCTD{vqvVRtWIjum>6pmB#xWX*WlrTOW?9BNsA@1f6M_2TqG```&uH8d~6R zB3r}3JR2aFlksjvwx&j67RP8Zg+%h$8({PnU*#er5$p1}&y%0M`SQY`%qa}@u@C!z zaTkxFw^O`35wX6;j0&x3-WPZ4D?b$XGPh9P1K;@eLrCA34~I62FJO5&LE3~10~o^o zsN$NcU}#B%x4aK^u!Z7iOZd1C|7Xj&kBUb(+auyhs9yks&^`b=Z5c$e^<_A?2$&;Q zUAuO`4G^m+O*98ywKmehjID(!@if_@P)}a;?#fcMx`?Ig09N?N-8<`b5rc~cPEWY( z!8ee4uckpEzdnj`I|_JPp+FZ-eg{Pm0?MyvN?$?u+MbAAWXYmmAs36R#6K6}`_;9R zcHG%njYiq9|0sxi3{J!3eBr_)m;By#?GTpo%Qm4c$IHtC1+=QGG{s9%HB1jY7@&*+ zQ&_c?rEt;eLQV2(fnj$}ic<+}2iw`3eRq0;XDQdk0`C)@bH zdNbup-Z&U4p3s65^?8$m6NA6mF6sCuR>y!wO*}F;{~#h80r_egXvz5hfUP(@dW6P* z7_j&tqIeZRm?z#z+lGvL0h?;uq;Yegq6!2u?Jso{ue1`UQC`OC@zy*V4a=-ZYH8%v zo`|Yf5*-2N7}@2fhR5FpO=}od=B}F=RDDpC(BK>-W2AoozzY9ZFZ&-uei|t=^18uC}I>=cw>Vl6P zWtqBc9F{yQL4u`$$+?$o>FHH^u2ONW%eN8A zdm@E8mpT1dA;m|N&|!Zv1nQVW(6ma$chosk&Ih{fv=sCn0X@te(Y_JrY3bFY2U@w< zqLySqP+d9GP#{e}bQ3%C8eDBndTDSz1yVa`SnWXaBT64nL!9(^%pmEXZKb*~&%^a< z2ZuU{(oy?Y-EJd7rrIH!gh83XBB7AUd{`d;NJ!{VY^KVU#} zv^R_GPt!7&FgeB|OR`?1Ix1<9OF`d0-0BEMJq$wjff_LAA1+f47?zX67*Q}nAMSyj zuUd%o2~?itnI1tAFUyaIKGXXF2*);mqGgM#W_vh{Nx_(}tx}@UWb)@4hU4Zu16%u( zN6J@HKoo7gFd8rqHuczzSX33*#!4kdSwX1G3qJ-P9Om{q8@69@6x(JCPYSg4mvsMu zI4n(OQ=oe#S>1xJWlPfrRUe3~Vyx9CX;6!p(t}W%ud<}!J6QjU>x&OWL%B5i&;w%n zV;rr2jiWf<5S)X=LD^OKb8s6ln8UG_aVBB-)Rt3Ls`_liV{zV>CN=NF^xTlK7H_?p zqkkhn-is>!*uac|u>#mSvQ@mEU2yf#I55EoP)RD5`je zCHdj(>Tn=vZF{LfEt&=!)Iwitbx@zZeX-@0Hc~|Iezew0+$BLvszWE*}Hj+JF?{tE+4@-uhYw zM(gR%@-kL}2;9QRNjdN~9|R-E=%+OvJhfrz#kGJ0P^?PiYqLm7&JCHHQenE zJtb*bqt**SN0NCjh{$!XMU?{1`+&gxaBCw~$d7lO~$1dzy=#1Te;a_k@6_$^ob zq1W*>mUDsAw*1_9CXe^R-aXtT=qnIvjTs9*L&LbgvvSCNy=nU*R4}?$fG8(ieI8nm z2M;TUs7=mGt#{OM^|IH#@RZ_%Xsh7*p$L9Bf`1;t>kMpN%4Q!0c-dl03kZ(AmzX|V zmoG#iMTiB!5GSsTtH~5K;mAiBE)AGG0Yd)^tu+X>-q%VY2}Uk1EAzvBTdWmSv=^BY zF34P!qR_cpf6_z&VR&)t>Sj&an<7Kw#i5K04?-xjUmWVQ!r}%HK9xy5-@I0kIxB@rF19DqU?af@r(i=p@lYQ8*s4uxpCq}FFC9Mq`In?dr! zb>>?rG`W?Q7W7=%W+FL;a&D;R(C7}3Al4pAj`wfTwTxw+oCE?Vl20M|+(M+cSVEI+-G=NJd@TNe z<-)tR<31cG2hC3sj$N2#G;*8P7>zkG;3z6YZ3XgWi@;691aCL6bswAk4Zwe;ylFe`JPx?%Aq~pApj9!=kfESVez}x;4}_-pZL|K$A@SX9 z>Jn5Dg67fxtYC^Z*I1IxQhP1TlH+R{s#jzIh4&+ol{RoV1 zT0cQv@t36N6qprT*EM=Vc;TGa`Z%gT(QtDyf|^I@Lz3Y|y<|9#+oJtfkzlad#SIps zKoEXt@K`@vB%yL!53n~{L!w-u{`micTH&rzYcu*FPP$=0yo`HteuUr_&T?AUA^GK# ziRveY)zjPKF-AW&zm+ZsXyb7ZDP5Bh9fk7APpc)Z?FHS+}4htL}x^k?YU zf2yTGFq$27!gkD7H|v3qWzGf<$a?$|&`Mk1MehU7!%omL)3!Ru7^4Y#MYkTn9WOWk6XFl-}R zZU4$CBxiDPXEWE_YCLI?hxL2hyS_XMG_zTczX7a8d0UO+RkkVA!rabQrN zh4Uj(T!kb!oI3zVML40p2dMU-g2xG7B2RlRaZkh;hrjD44sw)_MSV5OCkYfcz%LWI)@Gvb}0|RSTeW`{CmCUwkE9!dzDuU|ZOo4YivVZ#9 zGNaJCEV1UxWX(+ZP=oq`u#2-ezWWVyBl%GTsS=I)-(u;H4QyS;W{7~=b)|}dH5VU8 z1J0Ze_%$7DTgqK3U+^e$Y2EldZ53OXjpr4kL7=_k-$*M}GTA~iiZNeE&DEzY_(qyfb(nXtwq_pvo z{}m@u_S}j|_LOL_+MinU*~0uUx!ma#+JAr{N$Ni%`0EJ%CW5~;u;y}ZB7ufyyPTUy zBpjMr7{$LEdKd*BNSgok7=zr20)bt+TcU@evt>wljik&0as=93xf>0AcJgR{yeZ0E zTi;cVqrUgTFSGzAU)$Lc>260G5UVX7{)&*EhOSKc9TTzAX)Ev$@-$jb;eysc$SqZ}B?l|ngxAwDm9aq%) z4rXL{GkTi=s2gTY76W&EXGi=l@rl~R$7#FMvw!L=*`_O>mFTn&yWYNQTj=_kD3E5K z6~Sj4*!P|TEzQpew!u4@eb@4VGNtIJHnj70S3bis?yMEu%yWSz5O%LUQIUz!?G3tO z?KuR&PjQzsy6g^=At3a9-YeqEQTmC|k?wY2H;oPi`2h}h|C*RVZzYX8>P_=@YNXb> z?@mi*Tc#D3L%}?qIZ}-@vaZ$3X?eDhS|WI&&ALXwq_km<$k=dE^gEW!e$@sD43fZ> z`e`z{&q$MrH*b?3z=3lua!KPPm+`t|itdfg)?;&iT0-1@&N%AhCHQhba3_WCAHf#_ z;d2dJ1-z1N-=(6iHR_?e{@eoE<=r zhO{q1OOjT_(I{MF|N68IOpt;>S8GxKAc(|0TejSCcIgU*+&iYG?BhH zQ&51;8ZeH&?*o}G!}|jHuc*9zP+Hl)z6X&s`0V>-1L*-GS)yHLeiT47ch5l*aui<7 zt0jh+Ouu-v;X3B1gifS{GOOTk#nAzD8tFl=INC5(%{IsA=G5gV)kq)k7U_)ONz5|Q zs0@oY&vZH~JD`vR!ZwTJWuXT4J#0z4E!%vN!9C+3M&)dC7~j@oXpR#wCAqq;2~A6| zEnQSDA&KPbWt$Pv-_~yLjcSFX5{R?|IDhf};QYM7Ea#^ebx87Fpi{#NlgP4y(I|;{ zI#XjXXnuBgI~uXMT2eggP}m?$-hA-#m&h9fkNoRq`w-st?kO?J4c(B}L|89l-#mRT zVS|PNo4}o7$e))$v)KG*U@WPN!#yr;p-L_){06s!sAu;}pyf8JQCPen^oRkZUB-^t znlX9_hF!j#mraSQZ!m5hP1xLND6`n)sMFK9o@{C!VEf1>?PGtisUE>6MC7`RY_hd@ zC7Xx1A0-M6LX=gT*piZAOFjuKUkMiC9oY7(k@p7Cel;5Azd{-M2^IFa2FvNlP!(W$ zn3f^I&d&h(S9E_B=q3!TKz@yzPTMOKOSt-Ju)r{^6|Y#R-8fF%x=|jjw^mU%#o1NS zW@>eH)96tZR8p&xsHoc>9q5wNR7 zalN{3pH}Z$4v1m5k1}g<+p{%IoyJaR4e<50Uf53*Z-vE4sM*$R-qavXj*;=C#z;$R z&joe+Oi(%t$%%EGwl)mCMc(X*T2*M`7_{01)jyI}4>Nd{R^2dqcVXzdh2PL>aZ+8h z?QMpsvyb*$(Mi+%$<|ZTDh0l|F@kON{-jD`o|wd$Cs~-aR~ct*u9C|W!KES#^yt9X z8Ps0IzRmy$*Ke=YYHWqUK7s%WJB5{&ajP+Rr^R+IBleqXQ{(IHdu}*jKL!nOVQVu0 zJSOycyPz}q7|=rBVKuXGzm#NHb$Vd5`)rZ7;P#wCbJ8V zo747kfS|F zgBK%PBEeH={NJ{p#Zr@~L1zX*gViU1NgV_YIu)T;sfa?s-6U!-xo^&f!U;YJ@2y=k z!xMt&lU{>xN#}`nQS@7vgN>}k*t6PuiL`~Sp-fZmctoi77447E9mg&2-0@sg@mgtl z9>7G6Kj7FGF@?dlcO$tASYZ$Lg99yB-s3xh(kSWn4eV$Vd7asP(^okTgT!Iwdi@

>OHSTF+xzWm{f>FH!R9C_LVNohT zT1{Jm$9yjEv4+~<%<8lO9Ioq{=%`Sf+-i_h%mpY_oV*ZVqL|-OB~dZ@5O8wa)eIX= zu0=wX(By;Cev9p4^##^?o^^Iip4Fn+hkHRM4mY`r1sTi1mH;xhB+K+KLjBSOpPS7@ z61yUsyR2RH2yKCu0+P;OplRJw22%gtmgob3vYG_bxpO~%ir5VhP3SF>ItJIjSF|}O zsGnn<&2^SskS43;8x7mP1w+shy`NBm%XrqF=k=lVKL_ZvhT#7&nws&|BKT8r|0v0Z z?H!8VsPs57S39h%{RBi_zReP6XO|f00>Ik=Mmy_2m~t7k!s=6&^!IuB9z3T3v19qM z8ZQLRr6BPDNIVnS*^=&m#bPTjt|d0D34WUADUCSTrrGdqKdCpqD`f5UQlRy=@UK^QwO&qf0!k%7aymwUU#lypNs7Awq};TTDZor&5-S3t~pT}lF3ox7RWmVaQyE@ zyPP0xLi6JLP}*YY`wi+J1OIx9=b=8-DH5**2<>U5fM`3)&Z~#&(s3U|OIlIRSE2n9 zB&n)a&sG&s&_b^h@eO5)i-L18Gj!g+snIzMv7)i2-K=3ZP1WcrGD91?ajL=i^L3W+ zsB>1|UTN1DLinzx9kOWS;p1AOF&J^SIz);VzY`+|wWXF6h9F+S zo{P0Ohe3}0Z#O9bq5pEa$sb2&iQ&?!t54M4AnCti5gOspxBZ~+p3|cqmeYJ&Cjh50 z1y(;tAvwiTK5P(-5#&B*NqcuxM>i0+iYlt##w=|Zf_bV;%uw768@Q9c3)F-c&fVrN zePb#SG(5uo`Vs#7uOL%!X=n0(2~Z~gR|fUJje3sHKe_(vzd}3B>wxUessM#q4Ksz? zY4%)Gg`G*yt)@(&m!eoh-HxEYxZ-U;fxPx7w;1H+HG~qke!2}{i!;o=EVZQnCM3x9 zf3inS`?sv-211{q;#m8!hHU@FD~?R)^DJVDpMEN*K{k~Q$J0h3jHCU8_mG<{S6cy$ z+g;(Ow*w$)b{K8i9}FYX<+lGDw*SrYEU_uv((*HwI5FXJqEq^30XD_-MRdTqq#u4q zVfTNjA+ZGMih%UhUP$ul$ZDXjpgCf#`~Mbp*AEkv%&}1I|9Va4eUGA6kz6vz4B_zK z38?X)ryqRvbN4gHk=>zDk_h7cS0mxPtYZy$w96l0AVZ&6&DVuIM5L~+r}L;LXh5#a zRI|lGv|NgmQ>J^U5`@zKk!B0G3TF$bGHF4XNXtL)26nq)$iQ4+*g6s3-Ae=Uu^@%- zKqSA2*?OK8wRh8C?nJdh?pFXRN_^Fze%@^6n|Ow+`!M|}elVR7jjf0Stxh2QBCJvv;FLa^PM@a^PgF1;RJ1zW+DSy^ge8TlaofoKLvW)YSb5 zXmW|B-Yw`)p~$-QOFhsdGV!!-%hv%3Tqlb>QSjQwR-K=gwqNxg+d842Mo8r1;{;3_ zk{ZMREju+h2S9swx`5Ix3JN9RHHeQpY!~u;_c(V6H?T&hhrPie@KY(RSBE|$q21{E zaWJ5#XWuo*#j5)Z)cc_2_W&NjZz7aB-=Q(VEPUhI%I^THaN70k{ckHVqq$&sDl0}e zhab!acPoL7*CAH}$XZDJheOKmTgE=u-5np^k`>>)Ez`O6_wD-mkU55l+K3I=|H+AJ zlb#p6y;H~7oQ*7G7m&gLMM0B79E$xuU>UoJ#%sXn!jAruF2t#Mun5{A>>QN2lIedG zq)DHi#Ah<)Pp!;}`e&$@b<;j^+PQ)J(m=g?S#sl2_B*8x z*o(q;LnycU?5r0frHx1?GAu~kEwxpQEIA3QonKgq0&Iw@L*{Df_=2ggM6nwr^sU%N z)f05F_SYbJWy{j?H^AZx&?VL*11Ez|>JG713*$scK7R0ljI4doTRSdZdQE8mWS_Zj znEh(QF|9lMulP24#*LX%0;gKO2wu}RT5_co> z;NMKg1Tt_OYG-H!|D7NbYJy6LI`QhLpiMs!Y#X24G&DIjv|;1q_=d(i>V}5kbE+xC zZ7;lLM$iXdhzM0$Z#XXq;dD8#wPkfCy`xdj=-Ft{H@-i%n51o6u6L8ieNRt;k{=1NKwD8eW&0qj)se z3~)UD{xp}ceyg_SJo^=$O^xspjF>huun|M&I~4=xMJbp~N(we}xPFNzmq80j0gmgW zfHj7b0+!|j8!>dg8a;4cpMlBVy1g4tqt(*D1V9SbpK6-aU~*cGCssl`G!tW(8Mq`! zBrH+dk9oEq^K84HDF}V=5KT*0NLa$NkT}MD8VJa42i_etm%qx{O8zR!U>Ar5bI5-e zS^rt5>baJI_(w*^>@x9m%~&@86Bg+rhrgX57ogEVE>528i>JoAT_?8$S7|f_9|JFM z6P)B6%Oo-tX0T=F%lIiB3Y8&apa&Xc0vVsD-R*8l(Fxc|5}E2W~|pn8m=Y zgQfkPiM=g`5)sNOa!175BZxKw-1rVgmeDbv8w}izYSKM|YrBHZI&f=)iN8U7s$Pj^ zOVHvofClaNLC5_IzbMG^RhA4a2S_wP#S2=kVg-syB>EvB>Y2m;3|QsM#RJO$R+uXW zc-GuD$Vql5V|s}dh%31TkpGHBh2GrK#9zhxFZmqkBt9qa!W}l}bC9mq>J>+sTuq`u zJpfZom5=O^Y!oHh8*>hSq8$I)`wvcgDg1$lXcp059zcGUzdQ>3hhoMl$&QGI+4P2=(i@KQs8R^Y z4SdrI`OCQSg1}v|KljYlVOC#;hTlRT19u}?F84!~WiY2qb91yM43!C(zk%#c|O#k+o`PYXobmOk!&o(zHwP}IJIw#Ge#K=w%2HY)7cNn{^(s7 zQ`6p|^>kYsV&O4X-1vztzYeM04YfjD3~iRegxu;yb4+4S>)ETV&^CBLi{JE@u(qm{DcVRKr>nw3LezJki##cq~^#FNlP@Mu$%~k`PAq75zu1R1&dFL^*tI6iF_;h1K=OJ&{BRuB0t;~-TH=4ez

Z~Hzk(WT6woNK=nfsUNn}0~jFvT>*IG57iFHosQRCj+Z`K4uCk^)N zI3jQJqm!A4-f7&ubb5tAYhDgf>=iqPI^)eYdR+wq+foD=z3a7okeab@7Afa zBm_zgZeYRiw#*y&Gag?Hl#rS&~s@FmajK8VkK(eX0ksu$9 ze52v$OovZsSlC-}=|AOVR%`xKvz8i>e^Am}VI(&AMV{g~(gc+v}b+O%`FNk@4n!n%`aT!n<3ux~PXpb@h%*C9Md*f%XcT6n>O@zRqfd zbhiQ3)e#fyCDMLs;We&gHRpk`>JCftXGCR^2Z+SgG(-YMT6S4-r4}ez@&Pf4EK;J} z;n0pzgF5##Ex-!%95u_i62%KAgKe0Y_^;4L0>yN$l4wg;*0o7^Apw8}ws?cZW79R)4Ea#u&*^fl0 zQLuJfT_K{!V*|eh?M8doqXL>fy&`U+nyZWC41$VEh^VD;r^&>{RpeoX?)l(mgIsVt zAElc1rU2?m#TJ0tS55=$@`FniM(q{~>X$M~I7YSX$qQ=IO0<^4k7=iJs@*{Qe~{B& zedsk2R!@3&Inucmc=XFX3k(+$i4;zIdIcdPf8=1-RUv#T^2`em=L@hJB=s98-8STllh@ zgkvEGT_5TthG#Crhiem)6GL0JPI)e^W-ohyc#QoIM%-N?17vVKbJTM`JIJCUvhaFa zcOe=rja`EuJ#`NY$SbVGy5=2|aT6o{3fvJHpBNjT7@xj~ubo%Z7#M7#dN(lkdW~aX zucKa!{1G}^!#J$YC-xhWY=S;&#h|}=YSJEkk55gF);@yeUOcl$ZSD;vP{{W4K6ABY P^8EOTk=KrQN3;J6j^DHh literal 38400 zcmb__37B3*mG)h}tz)9{jDjK(#*jcTVaXu71OhqRXy ztxnag`(E{nB}?ET2ZVRo5)snhq7Y%hSl8@v$k(w zr#8xB-N1NOEEyXcu~t^+E7lH=Obm}^`Na6zZWf+~21blJsf`-hRxyy3>d0=*CjL=@ zwt}@*G+sJ3F)%SaHj0Y8xaDJP*t5hx4bdALCppxRK#S!JJ~xXM_%~~U=o~;ZK$^VH ztdf51Yco*Ym8AQ!YUAnqs1X!)s5U)t;q^%yXE-pr5{TJTnl>u_Gy@;v0o>rvOcb-K z^ybYYxjE$H=`}v~IbDtDw_~;60~cPGw2_bDRjWsayK8{liQ?IZF=)W+bt)0&Qbc^6}_HA^~?s?Cb%2GnG(!gz&k@l zv;g*PgB$#LuKlgE^T3e0QTE_~jKq<*Dhnne?wXfCZIR@^o3esrq4)h&Rv^8;p9P9vq<|s=?6GnqF$vfz^SLktwXA-(IcaDEyo4k`6yR4&Ov$Iy|0DhME)QbWG)`-;3&aLo7{F zT#LG^D~`BSmT?e>*~Dc+yWnZI?|zCsn3zX~2i9c8U7yM12B+BaWZXddMzY`jO>~bL zXW2xc=dHn1EVEcBjdFIJ0A(j-`*AVXGS8^s)#GDhL;b_!<6W4jXvlsr5Hv>rlZo!; zDRiw(E=KEAkUYKVZPYJ5=Cvz8CY#xG0yx3EjJ}<{+#r!YQETcE47^lE!ZUlL2%a%) z4-h&X+yrF*CIXV2P3M}*Ob<+v%d*`|klh!BoPl0An+%+TN`;?sfP1l)%b86@N?5o@ zSsdXs1RN2$6p*YGP~aLODk9TshDXmD=}uU3k?v*3F3JegkR_arN*Zz0 z6RMaz$VjimvqbuKfKu~20G=W16LZu8C3F|sLZ&gBGTn?i>D_Dk3ac?quX=U=__&2w z)A+#JkqOFRVtjbr@W2TAWM%BnnKNk_Sg~g9_{w0Wy<*}lbZ)TACV&#wRRA@y_W>l< z;hv@UT8)$2IhI^{J23LHv^dVZ5PLaq1*Z3dqQ?0^1V0FH9vPt&X77oLjVM@26P)ec zgjEa_iWZ)=s}0?xRZB@<%dotX=5uvDBYo$;s1+kU1k+k!8?wPMOa8lbEN5Mm?+$Z; zMN5brl)Wk?((8fVoX3F=$|}tNnw9SXLiRX{Hpb>gufIDooMe68t{cFTe|{98MEEg) zjd>^^Me#EfA_!7j zKrwuiK{@ht$1uhE5ZY_2M&SQ5*5>&)-k+4DbK35o$mPu#L|lF`f?Fc^B?HOYBGehb zfyp^|o*7x4#54J&C_=dVf>nD~N5>}m@t3<#XA-pV`J~2}%_yiK@D-43%E(eH&i@__ zv^JUCz{-^tr%;)_+xARh5FfHRW-sf`cS9dp_cs7a7PlFc@20s$&KQnnD%HFd$Zq%H zqrlg#MgeM-4oiU2BRuUCES(g$P!o3$ncz1gcqhP}Sj)gYE69J@+!AdFiZ0#g2NV+g z+wH++O@m{$c^p_h#w0A?&!?F2e8cBuI~g!42c4zp0VyW<#&`BOqj@OJ0q zmKOMpAC*m_iqGG}ND}`&5xf_m^z(g#^2N%sK7wkc3OOy4ahg6Jxce^fnd?IR^l~$S zO0FK+8y#4Ymk;K(Y112>!^x{8;eU2Po9+;{TE0qlgz<)>iJq~P*405z|l zMDV8u=EoY#lFUqTjLPG!GGUvn1Y_H37>01X#(c8^y88|oQL_QNjQNV@Fg{4YI*U@GKU7 z9l_rKlnrvN<37f(QS7}X$SK(mz1(y8uys$k#4{zoz>K5R*LqH-djOFy8vD*EF+z5J0xGE&3QcQ3u{b*dq*EPqf15gP`VeqBt@qAk(c_ z9S*1d0Uh$=Q8JR`Er8;UfkR*?*7g~gZ-U3=2*LSP1R<&X_^8umHV>=Hvc$BPlgf`d z7nf8eHIs^7zhGKRE+)}`nL~*Y@mebBU~9{-1;%n8S@d`e>d1P%a4O8fu+J#$fN*V^ zFGF!&NJ~Jefr8eYKOLatfdG_$j;ALiXDDct&a}e602S8L>r)OH9%oTjM+1lY@i8fX zn$<|tYc{MxK7Ax`dY?W@#JkM}!p1XLtZYb_)W$(BrVT^$LyCyX(Y6*Wl_=+6Irf-(hdz; zEnqF*%?jvs?m7%nq|uTxSc1f7}cD5NlJI?w&I=&9IMv0Mq6CaDWg zAg2B32jN z`^1w5IfyK8MwF{Ueb)$Nlk=>|5!8#<;ThRD{w-cd^CWNdlo-AJ3zYnH!wc)TWHaTS zLJ*Ev!8QiuvxOv20VVT48%>)3FhI@!RRHCPuLfvur_83qi)GGh1{#imedLQ+A*!e) z`+hf`Bci&zF}!SZt4`3U+rrt);;2$YAk9GvC1o1$7(g+-8lcp34nQew+@Rt;_R>?g zJ!C*=mS1GdJIHT|N*9=lbMas(#Zp0NEW$ox)SmDvT4$WPYGS8P;SeNDCTL)(ju$9% zTe1|OI9T%fP(hAun$iX^Aw9eX419PGlvkrxxc^KLMSlxro8|KXQc_%|8*FL1Ihmol zIrVebNTs;Ypd^aU7^M-GZAijt&k1v4tiN`DAek_*KTLB_GRS$&=6OXfp+;rOz^T#m zz^$hL27sFW`36;{kLQo0xY-KJA*ap`vdXSSu^gsZ+(ZyXG*3cuF&}qc4_w8Zf%U^< ztNQJt!Qk0r!-JJquCh&gCwxNi1#>UiC=*=fPu@-Rs*lR=4{vwrgoy~EQ?6>dBxIE* zu$+zLmZDlnQEkLzBq~NxzJbi&gbCbEgtq{^3sI){q!rmJK;QP}r#G}z3!PUIItD#u z2#Aoy8}NuJ75BuBu#Oy(QW!1n0TkTh0(wcn`H=$mrQn(0G1yZ9r054z99| zD4HnPAM?n5HV38dh~$R=&e%g1Zo~&1@%p?Bv3M9oIuCJx+Q(`ml4vp_?Ynr~P{j;w z6q&i74Eh(3pq(7Y{?iMDmKHV}|k+GWKMXt&R%Fp+FNio~3*!n4fjeG$AGpv>w0 z2IY4vMq+s18&EZ5Y_gh!xhFhiCMzNVV#?J%2vGcNj^H&0md}9ZP?yb~hw>p5nhKyQ zGas;;8Z*-zAfa#h3@h@xp_QEGFAlCpo4^knL=NPuGbIpu=(Ie1$oe=Q*1X#Me^u?e zQ;42iE{fZOf{MEc?vLT^;>8gD&Cc{uP{(F;ELxbN;KzWYD0l-vMM16&w~JZm$KqfM z|0FBqne-N>X2rMJhN5A@#=jOf;gk6Vc$hL%hg8lFF>w#W($c)rGrrO@KFL|p*2Q?7 zC1WhZr}@i})2Qevp#AMJ^*89?=!>TE}Wq| zcZ$K5hE&oPZUQ|Sz`q0J@k#kqfDWs2Hv717ya;YePlEcgdnlifY9=zfvIM{+1r~~+MejjLx+phqWC4Lp4QvI(1R0jQZgRC#@3In^|A@af1jj_~q8*wPI+X1#U2E?CbFJqU@0IQ+m8&;FV)a2Tb28lz_YFTK!Z-N+K z7L`K~e4;&}#v#E})~?(Vz^#duS*40WeI@TWjdX`5`t3GO<@_FLR#1ij&c#lZ9jZ&I zTki6luCmdn5Gjj0$WdY%MsLlUvB8kO86~FMnQahX1D=&OYG%%XNrP@oLXu`u89_C9 z|2LANZ6^Yv9nU86YuStbtUQrmLR-%X7MPQ5-3?F{hX_`#p$U8k;JE}5S<3T5kn+i= z?KB-9dl~{)X71U`^EFHyOj0%^z85Or_(b@LU@-K>^Q`2ttLR^f%JXS5P>b8318ReE zw$c6y^Adx~i!cc$qyGHC9*aS+C%F+fjm~O9FB+m=BEt5Q@z=-klj-@0@GV1jiqg z2o>Pm&Iy(2as&j0IQJ^}Peh1@?%yVso8us1);X8PI0&O?c^ycQ0(BIJpi`9}L9<$j zh+VKr%DYotRN;OqWi&rX%8ebKIig)RFq%0t97*nBj3H17WDsI`V+(DVOuiV!CMVDG zMol%6PHZjo$+lRZ5=E49xg`pTe!fiTbAUAig?3`pv=C4U32EBgYDz+rY_X!e#hR5p zamz*dmbajpVL<4lMw^Ak2GOcTP3YtkIOQk&EI%K4#r*P3HC{Eh*&q}d6bDctIVit| zW}FGo%JNNBn%V3+O|l)#BAwMoqPRJAiGsGoxv{b~K^YWrK(qWVxZ$-(+z{x!AVn`D zF$Kc^MMqv&qkon3H_RIKb=nDF(mnjBvb*Z5+`Fev#d{h?rQz8cQ?$XAl**ZC4l8r;ev2iU~$aa&gY z-X2SFsQh6ou=E3G|iq=o_!jYr$9O|pSXjmHbrHz6_$5D3EyhdFqdr4s*!g3Mmx~Kn#V&Q`mvEw3p_5 z2sg*tWrR?mbNL6>{tC}=WvOLjevzx>VMvOj< zeevw0Vq;$p9><{}`Bv@t#3~!qN&=phC$r-3NM(>qu1F$Rt;{zxjefBk29a9+K7tfl zGM7WFsd1>*LGSV$TN$GLH_;zC22=Bq$c!^ckIiJhnobpoX$LS@?1k9%k!;abD9 zOG>MJG!Dk#iGq8Ln<9~!Ah5<#FM4=U??@O8q2yRiD+_Ry8o~)`(lXRIAu>t1xQ=R_ zVhCylfyYyBdancICiak7?uE|vxO|$`HN+PepMqU=o}k620Glo{!|S)P7Dpj8(4|2k zEC85T&`LEqA*`ej=Ae#3V8`GM?))IyYl7pYu#GjC{D`6kwX&c$*2OStEe&yo!5U`} zAB7Xb^8sslf)MH-{E$N>BvA-U&_zO61TYc8IyE^Vtb-7Aio&fx5`|^~QI;Epq)O)u zS#Kc;#|tS2@35wBV7z+|e z<920@2}{b9T1C7m)%8U&vCb*Dy_QAb_gEKwb!}lpwNv{P>QTH9_%Oc$>Jcft?CTlR zQIHd@BYQMW&>Gl{r(b=f)Tem9rw&oONJ|I&M?CkUekB^1>9JtC2i|*o6p)#6Eg{uo z@vOvbGeHzfJcGT11W=Iex&-be0DCdUmjpc+o4N@5IV-)0q>m$MSaCUIMdO3sS+q=7 z6d2XjvwEbOA0+~sg6?KLrQZ1Vf=Pb`BzT~r2Uy;TATv$6~5s|{-r}oO0u@6;toNNr~t6M-4cMsC43rf8q^Yx#FCq0x{k!edJ9p%160^m<1>KRo+FUB6Ay?FpM1bw^-iCShXJF3 zf{P+Br~`*G2Q3_hICPAFIO={71UPp8Oah2!&Q!$wKp}qwc)QW`2ib+-N`MN9U4Z<3 z5Haq*f9Fkm`*Oej!4{`7rB>`usRpxN1_p2MiFxA|<4HF;i&ud^9$FT!1}Lsa0P>i; zSY=S-7N{e8D9pQ{Y2C*J+kG<-k~9}&mg#p-iec;MkI|tC3z%^SSF`m%-|Z2i#Vfju zfeTsuYJy}d2FIFq8oRQBRJiKS^7zN0ifMl{_yb;gR&jkd%L2K}eKSTmrMdLG7rLb+T*Ta<}YKc+W@tIm9z3ua=*t1ck zBn8$f0Vg;Z-ePTAgUx3L`qH2x-kU*2QhG}S--^m-ry2~Mqt=>>q|ARozgQhE^cELd zb*fDF8&}gQ)UfUAO3r1rN@dtfp8 zoL1y|ci=>oNgPk0wp1caA!gCrn72wIZwFO@?=UDoHdPziwxWHxbafFbdg%%mn-X2| z`gIT2a~C>`e`Hv^*Q)g{eQ0dle$=UdyJTgZ3Mj_qK-U3OW^_G3$>qZUqg;FkCzs+q z;Iql;X+l7^?Ay%(Pe`2I{Ou|CKV?vS2v5BHfK0B}E#ln&W|RFk(eWTv`#mZOZ$9e# zQRrr|jvr_ORZSg}$hxA!e%ivvK_Vyk34px%S^O)&U0C}`gPL!V4YyFe7YfcA?KI~m zqvplT8^i+aCi_nmyb90P$+45eM{}_J8|)!XAf-}sM45gRil)!8=sRb`37Q6Eql}?>kYE;b5qFjSi-z84ko`T2sVx z)7~*VHee?D0E%O6w#ST@kF`sX>R8M6t9_R5?74C^CQ86Xf#y|l=F#n=V5HzLU`)*) z@7$b%zi3eNDzKNN``MYO{j}mGw_?5GCEl?l@lq!I#Cj^|Qu|ORUp5ksr&|Elb+RQ+ zVqdiH!-+;Yv0WnE$BWFl(i4bmi`O#(aPw2-<|`ON68b7Yxxm*9YI1+-C6q|p+ISPX zd7FgwC9CMUxZG;h)p)*kbZBg3W#u!dC9o16m29LuM;#MHa?m^pJyePEOu=^ z1nziewDCN4MN#8Xduh%&EN0&T8MiQKRgk4D3a(|Ve=kds*fDBiBrzVaInFm-N6`mM zNRwB7itpfAmhxSIvXt)ul%?EbP>Ux`RDQA0o}2f!fPlFamjh~`z~WC^DHaCtB+EFJ z1)N1dZr&S>&)&Q%bn4DW!Z$TQk#X%A)UYg{4=VcJjVr<+o;@EjUcAvK)S3|(l2S-l z2k&!g`l1nuuCPEiELd3GdMRvM`l2%CTgN7Rp{1a6zkyEf{{>KT-wKf1FTNdZ-pQ$w zB`!?&+KhnGyp!uu0sC?5GQ}$oa7e9ONL-O+0tu4eg8tYDxVwpV5X?k4dEXTdal+-I zRqjgYBMoU}rD1n2mGV6!pN2&Sp%NU@SHXFdC)~6^OEv5Z!or2=U zHMybEp&FKxC5FFLIKeglts4DKu$$V?=(|Erx$wX0QXV}HUs>4x^>dF^ZA)3#3s4V)(3BnGyrExw zFRSYks0cyZ(EpTRiav*0kxfy1CCrlJL#wKHkp&cvKp`uw;wb&uMkp>@=!(E2dpLY| z1GDI@m*JW5H-7NddXd$&mexk1?6KyxUV`GK^Q?>k(lLUTchH9KQ{ZJk~fB7-=YX+dbM6;(YZ z6S%h8Q7zjDte1maKZ>_ok%hCVKiR|7pkw(Om4;U$%9jinL`T#}Bt8YSy4D*}aHC%` z31z@2XAz(A;HeROS_GetZf}H`Ep`E3xF-y`_$eL~T$x4EUTl8@wJ598DTPnW%cod< zn1#LHdGd*@5oj%N$tvO9t<){i?;22U;WVCsN=@#W5#$NJYIlmY&oWTSY58n|&{*ph zxV+nZ0&1XG9xFLjR${)DRk(Jb934&v%200Ds+50c4^t%aq}LMne;zOnztJroMz}SJ z;tq;r7XzJ0o*ThkBRD&PyBXN}5xYGP;H1dNyTtU2ksF;x}y;0TW!Uv7jT+X$yBQb@~xl~j2V^}c*iZI zzs;KMzgmcXC2M9$YlQ+S?0gmHw*b##e_;f%>vXmIL~vgNTMO9@8-DG&QpLcUi(jJy z?c`z~OkmqBDtCr_!J}}aW?zKi8Ht~~8($svkJ|2X4yv%tFTYHX-*4%M895IeE4YoB z(t@+l0Su}j5*>?Y1;I#gh%i;qPs&M*LhFJgt6GUcc~7FX5p92_m<~Xtq>I$qfyj~_ zh+Nr$$YER(h18@ybyJZ zc0j?QbYjP6OUHHcr3TKLLgk5Ec?|k!*2eyxwgk=8uQb{+2U6R9?5A6_^u2UGbqR!E#=x*v~--T1d{ zx5qV2I%muP+egM(Y%xUrLKeCqthg;q?W-+jl#9^XJ`%zvOX|pJ`Jd7+F?8icVMUAZ zacQx5(pqGE)F-6SVjB*t)6()}fCcr4t*BGpsQ`CD#EZ#b8>nqM_$j?w5D?nD_1;9D zsNbQ{?jL$>zXF3K&j)!KlQDg5BS!f$i{fwwNUPz^4WZ$=eTdtHmanj3ak-&E$nyDoreU`ap`gw{PZ>P1cobTmiQ2^AM`$Yg zRRN?n*_mNc$VTyu#RC7fM_`cppkfs&%r%_#!Co3D^qW-TsoF}S(S-3r7x-;^TkVKM z>O$i)iLL}9jY<+`3klX+ysWYFs2u-SWxefCBU!WDA3R#RC>9g3!&KZW0*YPdXhKKR zUDUwY0HuLpfC@RU0+?vPEh;TkQv>m}Y4Z|P1`SLiEvnxjAfsf05ib25B~s({)NDqa zPjYA%0+zDn%Im3fF?9Q~s206N;2e|f&?L|XqXmGZ!UlhGLH7@U)P5&0-OB-h38uG( z3zG>NM)TsxH73`78^@vQp#h0!D%V**xOPKR6Es-&w#=Hea18?DTLD?M7^+UC{VpI; z-C-$160{BLiXpJqLdF>-7Yuq?R}u)J*!G*i1791J698pWYXQon)&Z;s!cSRU8}Xz4 zZ+lvqgh;kfCl~5f#tqi4S++lEKzn1w(Fg1=^EJ$g@$<{o~{i5Ffpb%fb+LL~G z4|)2z`+;Wr+pynK-!eON)L&zNxvy(u$6Fx7%uWPzSlVWLJ66i1wZbRJh-DdNmDDU{*5-9w!gbY*B&p(#u5hOLLf^JNG zgh&wHP-c9W;$};;KyP<=Pm6ibo+U(vCT2ygr(=jV{@Ra?xfiRKBn+bEaumO^BI-I0 zdrVb6?T3M<0j@)jZ(HF;@vgGLsw%EBYzNg(EwR0CD_yUfBd^%^NX)rFu=6y4zofjVQ~I zkz)xe-e!ffWm+Gs#652|ko#hB9Z!iVEsc2-=Hps|GFs@U6pZ_-WsDL0VJDiIw(gB6 zpBw8v+#-*D&5KD51$%T5+^F!*TyJYYk*$TFv9$kd>8#$r5Sad#if4G9HQ+%Y&8t!6 zy8+6K-UE=oVpYD^pw2?t*(TI7g(?t)J9{^am&OB#&fcA3&3;*~nFrxxSF#=*l~R-d z+lIL)vm0D$I1qIWs=c@saPp(C1sg-Jf5>FP`@6mjXw3)Rh3pPC4H=P_%hw_0ax+Ns z{gTdUc|onb#%eo@tx$&sARm4@ixERnla!*lU?#3xq2Rd!B}6K&#opoVlZk*sjkvpO^F@PC&B`C>2o&NEt#T;9ki=c(o&nY}n!2QD`VpC=738qeM+~E{$>)Jv>iwo-2WWX-%{5 zAd}GrkU4aiKFD6Ccb+RbXuT)N*PKTKgK#%CN4H^`4Y_oN5?{eH=ycQ!`zddC z!R6!wb}zG{`EA>HCyp67L z6R=2*u0e7goC{J*atTr*cR$c(?^CXiI*wzE&WIIe{=h8`2P`M*oClD~y%ZYjTo9gV z{9#M`X{!&$KVS#hiRllb56)s0jG4tM_}AB-#Ol#SMt(Cunf@06Y7$!j()4v~$*#$j z2`w@50%|HQLnNEM1qAf#PVVpu63yPqYAZUY@mXybSw-tVAptQy2?%1*k$eLXi?#vz z7u*&mbxnRup=Fj!9y^n19v~zw)R$U7mUGND0;GwsWAB>_JnRS`O?=xS-$j*2vTuM7@!b+FjC$DkjH-IHv#f+ zp~Tu)JVv_Mi+6rZ@NR%xVHI>tWxjkzSn!mO4%E4yQ-nM__e19y+><=Ji->T~&iySk z)!ox|-Wl?F3J_pkx-sc+FH%1s%m6}zqp<@`5tc0#&^*=Liy2Ltv0@r#S~0imJch9_ zfG+!0nXzil&ohJP|F(jLu3TQs%&|INswxJ}$@KQL7z}RK`CZih??415Kt<=*R$H_# zORav3W04YMALphkuyO=y1p&_uL~}#Hi_^;Z{wt0t`Sc93Q^pJ)$SL&g zP$T~|JTsn(Xd9;3p}#;Aao##}=FVP>(NY;QBDz9B{Ma8QWx4cHD!x zmf94!K*hrdCmb8IZ)X^&f>!4@iG`xAre!UUlh(qszP`9_Bx*pU>RV7JWR+rUimk>e zK$aXL3N+_Mtkg_F{b?u`qIhQ2&NQtCTAqc1-zoFzZK}BMS`!(L<7E7*B2nA|!_jZ& zb^>~D#bLDVR2)#9dJO8@y{4lD5Jg=_oXp;St^BHCwDteV@QX)V^01BKe>m@RGh6JY zu6j$eAm=0np?NahIUc^LU#`@8@;!TYOUpeGyw||KW6WZd2J$RiKbc>3!8EqZY& zqT9nPlzSj>yB*~t0NGqehdV^{zL!-+({~)3=UPd>ax_rM6hGStkc3GndE3=QCnbQ* z8jC_jbDbNeTAD%78Of88)_YM|4v{ieAome5vsE&oPd2d}x~3glfSISpghC7}WU&1r z!)aZdFpN%YCof^w`W>tGUwS%==#H$xL7vn!jYU|mzGFPj7SLAGa34Tf!4D(&qX_=k zKw5#nz=rwD3~D(x{dcnb?2VLi<7GN8FE4+jLz@EG+23D``H+A$rzF%U9wk1ju(;?Pu^$M|^ zQf|zjpq0hy)2U=5Fo{0PP{@_Ru$)fTYES&A%$?6ZfM%tRKZ)Q^0ZQLL1Gp8FFMke@ zhFksuAOpAdX&i7%v`fbpD`@|E$x8bthkR|R-CE^EcMF8+1#yxL%9@V5vPLZW!heJ@ z70($;$PG0ab3peC$K(K#D0uuV4%~H6QvJJL94JIXpv^RSt#Kee!9j7d6 zqDm==-gxMWehe%cgj(V(k{#qEx*`}AIKL>kEJ&$r;e6B*R#`4heIN9F`Zm{F=2%k_ z)-*cC&>jtwEv~38rZV@Q36%RU)?!8~VURtlLvIG^?F^%8-yK75MuAS`y!DPSKH2NL z7R?MvOd69PPoHLd&PVjoRWA+WAl#C1z0mZd+_mVE6QCDYz|OR?pwj6fu&3a|(R#+2 zB#DoLZr%?{{J$`$OtnBHuB9dtFw%OjEw#$c(mV1J**rr?%mSw87&WNxnz{v`c>!8( zskh9r+9|dHa*1s)q02U+vWbF*3!J`>p|}CXx*#CVt?yQ=)Vqi6)E~#3UVmSqR*;TK zc0KiXi#6+|wbqI0^~ce+Pk%slS~95b-*>k%v0jYXcdlOow%U{bjMe^+h;#v{+&LNq zk>p6t$9p@P&_P5zEy$Xfx?2MP@mftS&^v8Kv!J39BGegukn3nl4m260%ZC7JiFg>G z)&(YNLijaml_>lM;4)pm#;l!LXk5yON4&|nzzJ!~uk69S?5@eFa(m|gK~8<}xl~v^ zMM68`o-PpyBBDFI;)G_wy#Tkc_ zL3=xT)Vk;S%T^C$?!W!Z^kBa=<{ const & p) { return p.second == domain0; }) && !implicit_args) { + if (!nested.empty() && + std::all_of(nested.begin() + 1, nested.end(), [&](std::pair const & p) { + return p.second == nested[0].second; }) && + !implicit_args) { // Domain of all binders is the same + expr domain0 = nested[0].second; format names = pp_bnames(nested.begin(), nested.end(), false); result p_domain = pp_scoped_child(domain0, depth); result p_body = pp_scoped_child(b, depth); diff --git a/src/kernel/kernel.cpp b/src/kernel/kernel.cpp index d7dd91407..fcfbddd9a 100644 --- a/src/kernel/kernel.cpp +++ b/src/kernel/kernel.cpp @@ -21,100 +21,25 @@ expr const TypeU1 = Type(u_lvl+1); // ======================================= // Boolean Type -expr const Bool = mk_Bool(); +expr const Bool = mk_Bool(); +expr const True = mk_true(); +expr const False = mk_false(); expr mk_bool_type() { return mk_Bool(); } bool is_bool(expr const & t) { return is_Bool(t); } // ======================================= -// ======================================= -// Boolean values True and False -static name g_true_name("true"); -static name g_false_name("false"); -static name g_true_u_name("\u22A4"); // ⊤ -static name g_false_u_name("\u22A5"); // ⊥ -/** - \brief Semantic attachments for Boolean values. -*/ -class bool_value_value : public value { - bool m_val; -public: - bool_value_value(bool v):m_val(v) {} - virtual ~bool_value_value() {} - virtual expr get_type() const { return Bool; } - virtual name get_name() const { return m_val ? g_true_name : g_false_name; } - virtual name get_unicode_name() const { return m_val ? g_true_u_name : g_false_u_name; } - // LCOV_EXCL_START - virtual bool operator==(value const & other) const { - // This method is unreachable because there is only one copy of True and False in the system, - // and they have different hashcodes. - bool_value_value const * _other = dynamic_cast(&other); - return _other && _other->m_val == m_val; - } - // LCOV_EXCL_STOP - virtual void write(serializer & s) const { s << (m_val ? "true" : "false"); } - bool get_val() const { return m_val; } -}; -expr const True = mk_value(*(new bool_value_value(true))); -expr const False = mk_value(*(new bool_value_value(false))); -static register_builtin_fn true_blt("true", []() { return True; }); -static register_builtin_fn false_blt("false", []() { return False; }); -static value::register_deserializer_fn true_ds("true", [](deserializer & ) { return True; }); -static value::register_deserializer_fn false_ds("false", [](deserializer & ) { return False; }); - expr mk_bool_value(bool v) { return v ? True : False; } bool is_bool_value(expr const & e) { - return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; + return is_true(e) || is_false(e); } bool to_bool(expr const & e) { lean_assert(is_bool_value(e)); - return static_cast(to_value(e)).get_val(); -} -bool is_true(expr const & e) { - return is_bool_value(e) && to_bool(e); -} -bool is_false(expr const & e) { - return is_bool_value(e) && !to_bool(e); + return e == True; } // ======================================= -// ======================================= -// Equality -static name g_eq_name("eq"); -static format g_eq_fmt(g_eq_name); -/** - \brief Semantic attachment for if-then-else operator with type - Pi (A : Type), Bool -> A -> A -> A -*/ -class eq_fn_value : public value { - expr m_type; - static expr mk_type() { - expr A = Const("A"); - // Pi (A: TypeU), A -> A -> Bool - return Pi({A, TypeU}, (A >> (A >> Bool))); - } -public: - eq_fn_value():m_type(mk_type()) {} - virtual ~eq_fn_value() {} - virtual expr get_type() const { return m_type; } - virtual name get_name() const { return g_eq_name; } - virtual optional normalize(unsigned num_args, expr const * args) const { - if (num_args == 4 && is_value(args[2]) && is_value(args[3]) && typeid(to_value(args[2])) == typeid(to_value(args[3]))) { - return some_expr(mk_bool_value(args[2] == args[3])); - } else { - return none_expr(); - } - } - virtual void write(serializer & s) const { s << "eq"; } -}; -MK_BUILTIN(eq_fn, eq_fn_value); -MK_IS_BUILTIN(is_eq_fn, mk_eq_fn()); -static register_builtin_fn eq_blt("eq", []() { return mk_eq_fn(); }); -static value::register_deserializer_fn eq_ds("eq", [](deserializer & ) { return mk_eq_fn(); }); -// ======================================= - - void import_kernel(environment const & env, io_state const & ios) { env->import("kernel", ios); } diff --git a/src/kernel/kernel.h b/src/kernel/kernel.h index 9c6edbd6b..b142288ce 100644 --- a/src/kernel/kernel.h +++ b/src/kernel/kernel.h @@ -29,15 +29,6 @@ bool is_bool_value(expr const & e); \pre is_bool_value(e) */ bool to_bool(expr const & e); -/** \brief Return true iff \c e is the Lean true value. */ -bool is_true(expr const & e); -/** \brief Return true iff \c e is the Lean false value. */ -bool is_false(expr const & e); - -expr mk_eq_fn(); -bool is_eq_fn(expr const & e); -inline expr mk_eq(expr const & A, expr const & lhs, expr const & rhs) { return mk_app(mk_eq_fn(), A, lhs, rhs); } -inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)) && num_args(e) == 4; } inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); } inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); } diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 66cf7a16e..db1b56b45 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -8,81 +8,82 @@ Released under Apache 2.0 license as described in the file LICENSE. namespace lean { MK_CONSTANT(TypeU, name("TypeU")); MK_CONSTANT(Bool, name("Bool")); +MK_CONSTANT(heq_fn, name("heq")); +MK_CONSTANT(hrefl_fn, name("hrefl")); +MK_CONSTANT(eq_fn, name("eq")); +MK_CONSTANT(refl_fn, name("refl")); +MK_CONSTANT(heq_eq_fn, name("heq_eq")); +MK_CONSTANT(true, name("true")); +MK_CONSTANT(trivial, name("trivial")); +MK_CONSTANT(false, name("false")); MK_CONSTANT(not_fn, name("not")); MK_CONSTANT(or_fn, name("or")); MK_CONSTANT(and_fn, name("and")); MK_CONSTANT(implies_fn, name("implies")); MK_CONSTANT(neq_fn, name("neq")); +MK_CONSTANT(a_neq_a_elim_fn, name("a_neq_a_elim")); MK_CONSTANT(iff_fn, name("iff")); -MK_CONSTANT(exists_fn, name("exists")); -MK_CONSTANT(nonempty_fn, name("nonempty")); -MK_CONSTANT(nonempty_intro_fn, name("nonempty_intro")); MK_CONSTANT(em_fn, name("em")); -MK_CONSTANT(case_fn, name("case")); -MK_CONSTANT(refl_fn, name("refl")); -MK_CONSTANT(subst_fn, name("subst")); -MK_CONSTANT(funext_fn, name("funext")); -MK_CONSTANT(allext_fn, name("allext")); -MK_CONSTANT(eps_fn, name("eps")); -MK_CONSTANT(eps_ax_fn, name("eps_ax")); -MK_CONSTANT(proof_irrel_fn, name("proof_irrel")); -MK_CONSTANT(substp_fn, name("substp")); -MK_CONSTANT(eps_th_fn, name("eps_th")); -MK_CONSTANT(eps_singleton_fn, name("eps_singleton")); -MK_CONSTANT(nonempty_fun_fn, name("nonempty_fun")); -MK_CONSTANT(ite_fn, name("ite")); MK_CONSTANT(not_intro_fn, name("not_intro")); -MK_CONSTANT(eta_fn, name("eta")); -MK_CONSTANT(trivial, name("trivial")); MK_CONSTANT(absurd_fn, name("absurd")); -MK_CONSTANT(eqmp_fn, name("eqmp")); -MK_CONSTANT(boolcomplete_fn, name("boolcomplete")); +MK_CONSTANT(exists_fn, name("exists")); +MK_CONSTANT(case_fn, name("case")); MK_CONSTANT(false_elim_fn, name("false_elim")); -MK_CONSTANT(imp_trans_fn, name("imp_trans")); -MK_CONSTANT(imp_eq_trans_fn, name("imp_eq_trans")); -MK_CONSTANT(eq_imp_trans_fn, name("eq_imp_trans")); -MK_CONSTANT(not_not_eq_fn, name("not_not_eq")); -MK_CONSTANT(not_not_elim_fn, name("not_not_elim")); MK_CONSTANT(mt_fn, name("mt")); MK_CONSTANT(contrapos_fn, name("contrapos")); MK_CONSTANT(absurd_elim_fn, name("absurd_elim")); -MK_CONSTANT(not_imp_eliml_fn, name("not_imp_eliml")); -MK_CONSTANT(not_imp_elimr_fn, name("not_imp_elimr")); -MK_CONSTANT(resolve1_fn, name("resolve1")); -MK_CONSTANT(and_intro_fn, name("and_intro")); -MK_CONSTANT(and_eliml_fn, name("and_eliml")); -MK_CONSTANT(and_elimr_fn, name("and_elimr")); MK_CONSTANT(or_introl_fn, name("or_introl")); MK_CONSTANT(or_intror_fn, name("or_intror")); -MK_CONSTANT(or_elim_fn, name("or_elim")); -MK_CONSTANT(refute_fn, name("refute")); +MK_CONSTANT(boolcomplete_fn, name("boolcomplete")); +MK_CONSTANT(boolcomplete_swapped_fn, name("boolcomplete_swapped")); +MK_CONSTANT(resolve1_fn, name("resolve1")); +MK_CONSTANT(subst_fn, name("subst")); +MK_CONSTANT(substp_fn, name("substp")); MK_CONSTANT(symm_fn, name("symm")); -MK_CONSTANT(eqmpr_fn, name("eqmpr")); MK_CONSTANT(trans_fn, name("trans")); +MK_CONSTANT(congr1_fn, name("congr1")); +MK_CONSTANT(congr2_fn, name("congr2")); +MK_CONSTANT(congr_fn, name("congr")); +MK_CONSTANT(true_ne_false, name("true_ne_false")); +MK_CONSTANT(absurd_not_true_fn, name("absurd_not_true")); +MK_CONSTANT(not_false_trivial, name("not_false_trivial")); +MK_CONSTANT(eqmp_fn, name("eqmp")); +MK_CONSTANT(eqmpr_fn, name("eqmpr")); +MK_CONSTANT(imp_trans_fn, name("imp_trans")); +MK_CONSTANT(imp_eq_trans_fn, name("imp_eq_trans")); +MK_CONSTANT(eq_imp_trans_fn, name("eq_imp_trans")); +MK_CONSTANT(to_eq_fn, name("to_eq")); +MK_CONSTANT(to_heq_fn, name("to_heq")); +MK_CONSTANT(iff_eliml_fn, name("iff_eliml")); +MK_CONSTANT(iff_elimr_fn, name("iff_elimr")); 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(eqt_elim_fn, name("eqt_elim")); MK_CONSTANT(eqf_elim_fn, name("eqf_elim")); -MK_CONSTANT(congr1_fn, name("congr1")); -MK_CONSTANT(congr2_fn, name("congr2")); -MK_CONSTANT(congr_fn, name("congr")); -MK_CONSTANT(exists_elim_fn, name("exists_elim")); -MK_CONSTANT(exists_intro_fn, name("exists_intro")); -MK_CONSTANT(nonempty_elim_fn, name("nonempty_elim")); -MK_CONSTANT(nonempty_ex_intro_fn, name("nonempty_ex_intro")); -MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps")); -MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice")); +MK_CONSTANT(heqt_elim_fn, name("heqt_elim")); +MK_CONSTANT(not_true, name("not_true")); +MK_CONSTANT(not_false, name("not_false")); +MK_CONSTANT(not_not_eq_fn, name("not_not_eq")); +MK_CONSTANT(not_neq_fn, name("not_neq")); +MK_CONSTANT(not_neq_elim_fn, name("not_neq_elim")); +MK_CONSTANT(not_not_elim_fn, name("not_not_elim")); +MK_CONSTANT(not_imp_eliml_fn, name("not_imp_eliml")); +MK_CONSTANT(not_imp_elimr_fn, name("not_imp_elimr")); +MK_CONSTANT(and_intro_fn, name("and_intro")); +MK_CONSTANT(and_eliml_fn, name("and_eliml")); +MK_CONSTANT(and_elimr_fn, name("and_elimr")); +MK_CONSTANT(or_elim_fn, name("or_elim")); +MK_CONSTANT(refute_fn, name("refute")); MK_CONSTANT(boolext_fn, name("boolext")); MK_CONSTANT(iff_intro_fn, name("iff_intro")); -MK_CONSTANT(iff_eliml_fn, name("iff_eliml")); -MK_CONSTANT(iff_elimr_fn, name("iff_elimr")); -MK_CONSTANT(skolem_th_fn, name("skolem_th")); MK_CONSTANT(eqt_intro_fn, name("eqt_intro")); MK_CONSTANT(eqf_intro_fn, name("eqf_intro")); -MK_CONSTANT(neq_elim_fn, name("neq_elim")); +MK_CONSTANT(a_neq_a_fn, name("a_neq_a")); MK_CONSTANT(eq_id_fn, name("eq_id")); MK_CONSTANT(iff_id_fn, name("iff_id")); +MK_CONSTANT(neq_elim_fn, name("neq_elim")); +MK_CONSTANT(neq_to_not_eq_fn, name("neq_to_not_eq")); MK_CONSTANT(left_comm_fn, name("left_comm")); MK_CONSTANT(or_comm_fn, name("or_comm")); MK_CONSTANT(or_assoc_fn, name("or_assoc")); @@ -93,6 +94,7 @@ MK_CONSTANT(or_truel_fn, name("or_truel")); MK_CONSTANT(or_truer_fn, name("or_truer")); MK_CONSTANT(or_tauto_fn, name("or_tauto")); MK_CONSTANT(or_left_comm_fn, name("or_left_comm")); +MK_CONSTANT(resolve2_fn, name("resolve2")); MK_CONSTANT(and_comm_fn, name("and_comm")); MK_CONSTANT(and_id_fn, name("and_id")); MK_CONSTANT(and_assoc_fn, name("and_assoc")); @@ -108,29 +110,21 @@ MK_CONSTANT(imp_falser_fn, name("imp_falser")); MK_CONSTANT(imp_falsel_fn, name("imp_falsel")); MK_CONSTANT(imp_id_fn, name("imp_id")); MK_CONSTANT(imp_or_fn, name("imp_or")); -MK_CONSTANT(not_true, name("not_true")); -MK_CONSTANT(not_false, name("not_false")); -MK_CONSTANT(not_neq_fn, name("not_neq")); -MK_CONSTANT(not_neq_elim_fn, name("not_neq_elim")); -MK_CONSTANT(not_and_fn, name("not_and")); -MK_CONSTANT(not_and_elim_fn, name("not_and_elim")); -MK_CONSTANT(not_or_fn, name("not_or")); -MK_CONSTANT(not_or_elim_fn, name("not_or_elim")); -MK_CONSTANT(not_iff_fn, name("not_iff")); -MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim")); -MK_CONSTANT(not_implies_fn, name("not_implies")); -MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim")); MK_CONSTANT(not_congr_fn, name("not_congr")); -MK_CONSTANT(exists_rem_fn, name("exists_rem")); -MK_CONSTANT(forall_rem_fn, name("forall_rem")); -MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro")); -MK_CONSTANT(not_forall_fn, name("not_forall")); -MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim")); +MK_CONSTANT(exists_elim_fn, name("exists_elim")); +MK_CONSTANT(exists_intro_fn, name("exists_intro")); MK_CONSTANT(not_exists_fn, name("not_exists")); MK_CONSTANT(not_exists_elim_fn, name("not_exists_elim")); MK_CONSTANT(exists_unfold1_fn, name("exists_unfold1")); MK_CONSTANT(exists_unfold2_fn, name("exists_unfold2")); MK_CONSTANT(exists_unfold_fn, name("exists_unfold")); +MK_CONSTANT(inhabited_fn, name("inhabited")); +MK_CONSTANT(inhabited_intro_fn, name("inhabited_intro")); +MK_CONSTANT(inhabited_elim_fn, name("inhabited_elim")); +MK_CONSTANT(inhabited_ex_intro_fn, name("inhabited_ex_intro")); +MK_CONSTANT(inhabited_range_fn, name("inhabited_range")); +MK_CONSTANT(exists_rem_fn, name("exists_rem")); +MK_CONSTANT(forall_rem_fn, name("forall_rem")); MK_CONSTANT(imp_congrr_fn, name("imp_congrr")); MK_CONSTANT(imp_congrl_fn, name("imp_congrl")); MK_CONSTANT(imp_congr_fn, name("imp_congr")); @@ -140,14 +134,45 @@ MK_CONSTANT(or_congr_fn, name("or_congr")); MK_CONSTANT(and_congrr_fn, name("and_congrr")); MK_CONSTANT(and_congrl_fn, name("and_congrl")); MK_CONSTANT(and_congr_fn, name("and_congr")); +MK_CONSTANT(not_and_fn, name("not_and")); +MK_CONSTANT(not_and_elim_fn, name("not_and_elim")); +MK_CONSTANT(not_or_fn, name("not_or")); +MK_CONSTANT(not_or_elim_fn, name("not_or_elim")); +MK_CONSTANT(not_implies_fn, name("not_implies")); +MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim")); +MK_CONSTANT(a_eq_not_a_fn, name("a_eq_not_a")); +MK_CONSTANT(a_iff_not_a_fn, name("a_iff_not_a")); +MK_CONSTANT(true_eq_false, name("true_eq_false")); +MK_CONSTANT(true_iff_false, name("true_iff_false")); +MK_CONSTANT(false_eq_true, name("false_eq_true")); +MK_CONSTANT(false_iff_true, name("false_iff_true")); +MK_CONSTANT(a_iff_true_fn, name("a_iff_true")); +MK_CONSTANT(a_iff_false_fn, name("a_iff_false")); +MK_CONSTANT(not_iff_fn, name("not_iff")); +MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim")); MK_CONSTANT(forall_or_distributer_fn, name("forall_or_distributer")); MK_CONSTANT(forall_or_distributel_fn, name("forall_or_distributel")); MK_CONSTANT(forall_and_distribute_fn, name("forall_and_distribute")); MK_CONSTANT(exists_and_distributer_fn, name("exists_and_distributer")); -MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel")); MK_CONSTANT(exists_or_distribute_fn, name("exists_or_distribute")); +MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro")); +MK_CONSTANT(not_forall_fn, name("not_forall")); +MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim")); +MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel")); MK_CONSTANT(exists_imp_distribute_fn, name("exists_imp_distribute")); -MK_CONSTANT(nonempty_range_fn, name("nonempty_range")); +MK_CONSTANT(forall_uninhabited_fn, name("forall_uninhabited")); +MK_CONSTANT(allext_fn, name("allext")); +MK_CONSTANT(funext_fn, name("funext")); +MK_CONSTANT(eta_fn, name("eta")); +MK_CONSTANT(eps_fn, name("eps")); +MK_CONSTANT(eps_ax_fn, name("eps_ax")); +MK_CONSTANT(eps_th_fn, name("eps_th")); +MK_CONSTANT(eps_singleton_fn, name("eps_singleton")); +MK_CONSTANT(inhabited_fun_fn, name("inhabited_fun")); +MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps")); +MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice")); +MK_CONSTANT(skolem_th_fn, name("skolem_th")); +MK_CONSTANT(ite_fn, name("ite")); MK_CONSTANT(if_true_fn, name("if_true")); MK_CONSTANT(if_false_fn, name("if_false")); MK_CONSTANT(if_a_a_fn, name("if_a_a")); @@ -157,4 +182,9 @@ MK_CONSTANT(if_imp_else_fn, name("if_imp_else")); MK_CONSTANT(app_if_distribute_fn, name("app_if_distribute")); MK_CONSTANT(eq_if_distributer_fn, name("eq_if_distributer")); MK_CONSTANT(eq_if_distributel_fn, name("eq_if_distributel")); +MK_CONSTANT(injective_fn, name("injective")); +MK_CONSTANT(non_surjective_fn, name("non_surjective")); +MK_CONSTANT(ind, name("ind")); +MK_CONSTANT(infinity, name("infinity")); +MK_CONSTANT(proof_irrel_fn, name("proof_irrel")); } diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 2ee04c003..4ff9b571b 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -9,6 +9,29 @@ expr mk_TypeU(); bool is_TypeU(expr const & e); expr mk_Bool(); bool is_Bool(expr const & e); +expr mk_heq_fn(); +bool is_heq_fn(expr const & e); +inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)) && num_args(e) == 5; } +inline expr mk_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq_fn(), e1, e2, e3, e4}); } +expr mk_hrefl_fn(); +bool is_hrefl_fn(expr const & e); +inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); } +expr mk_eq_fn(); +bool is_eq_fn(expr const & e); +inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)) && num_args(e) == 4; } +inline expr mk_eq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eq_fn(), e1, e2, e3}); } +expr mk_refl_fn(); +bool is_refl_fn(expr const & e); +inline expr mk_refl_th(expr const & e1, expr const & e2) { return mk_app({mk_refl_fn(), e1, e2}); } +expr mk_heq_eq_fn(); +bool is_heq_eq_fn(expr const & e); +inline expr mk_heq_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_heq_eq_fn(), e1, e2, e3}); } +expr mk_true(); +bool is_true(expr const & e); +expr mk_trivial(); +bool is_trivial(expr const & e); +expr mk_false(); +bool is_false(expr const & e); expr mk_not_fn(); bool is_not_fn(expr const & e); inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)) && num_args(e) == 2; } @@ -29,100 +52,32 @@ expr mk_neq_fn(); bool is_neq_fn(expr const & e); inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)) && num_args(e) == 4; } inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); } +expr mk_a_neq_a_elim_fn(); +bool is_a_neq_a_elim_fn(expr const & e); +inline expr mk_a_neq_a_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_a_neq_a_elim_fn(), e1, e2, e3}); } expr mk_iff_fn(); bool is_iff_fn(expr const & e); inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app({mk_iff_fn(), e1, e2}); } +expr mk_em_fn(); +bool is_em_fn(expr const & e); +inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); } +expr mk_not_intro_fn(); +bool is_not_intro_fn(expr const & e); +inline expr mk_not_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_not_intro_fn(), e1, e2}); } +expr mk_absurd_fn(); +bool is_absurd_fn(expr const & e); +inline expr mk_absurd_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_absurd_fn(), e1, e2, e3}); } expr mk_exists_fn(); bool is_exists_fn(expr const & e); inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); } -expr mk_nonempty_fn(); -bool is_nonempty_fn(expr const & e); -inline bool is_nonempty(expr const & e) { return is_app(e) && is_nonempty_fn(arg(e, 0)) && num_args(e) == 2; } -inline expr mk_nonempty(expr const & e1) { return mk_app({mk_nonempty_fn(), e1}); } -expr mk_nonempty_intro_fn(); -bool is_nonempty_intro_fn(expr const & e); -inline expr mk_nonempty_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_nonempty_intro_fn(), e1, e2}); } -expr mk_em_fn(); -bool is_em_fn(expr const & e); -inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); } expr mk_case_fn(); bool is_case_fn(expr const & e); inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); } -expr mk_refl_fn(); -bool is_refl_fn(expr const & e); -inline expr mk_refl_th(expr const & e1, expr const & e2) { return mk_app({mk_refl_fn(), e1, e2}); } -expr mk_subst_fn(); -bool is_subst_fn(expr const & e); -inline expr mk_subst_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_subst_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_funext_fn(); -bool is_funext_fn(expr const & e); -inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); } -expr mk_allext_fn(); -bool is_allext_fn(expr const & e); -inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); } -expr mk_eps_fn(); -bool is_eps_fn(expr const & e); -inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)) && num_args(e) == 4; } -inline expr mk_eps(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_fn(), e1, e2, e3}); } -expr mk_eps_ax_fn(); -bool is_eps_ax_fn(expr const & e); -inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4, e5}); } -expr mk_proof_irrel_fn(); -bool is_proof_irrel_fn(expr const & e); -inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); } -expr mk_substp_fn(); -bool is_substp_fn(expr const & e); -inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_eps_th_fn(); -bool is_eps_th_fn(expr const & e); -inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_th_fn(), e1, e2, e3, e4}); } -expr mk_eps_singleton_fn(); -bool is_eps_singleton_fn(expr const & e); -inline expr mk_eps_singleton_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_singleton_fn(), e1, e2, e3}); } -expr mk_nonempty_fun_fn(); -bool is_nonempty_fun_fn(expr const & e); -inline expr mk_nonempty_fun_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_fun_fn(), e1, e2, e3}); } -expr mk_ite_fn(); -bool is_ite_fn(expr const & e); -inline bool is_ite(expr const & e) { return is_app(e) && is_ite_fn(arg(e, 0)) && num_args(e) == 5; } -inline expr mk_ite(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ite_fn(), e1, e2, e3, e4}); } -expr mk_not_intro_fn(); -bool is_not_intro_fn(expr const & e); -inline expr mk_not_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_not_intro_fn(), e1, e2}); } -expr mk_eta_fn(); -bool is_eta_fn(expr const & e); -inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); } -expr mk_trivial(); -bool is_trivial(expr const & e); -expr mk_absurd_fn(); -bool is_absurd_fn(expr const & e); -inline expr mk_absurd_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_absurd_fn(), e1, e2, e3}); } -expr mk_eqmp_fn(); -bool is_eqmp_fn(expr const & e); -inline expr mk_eqmp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmp_fn(), e1, e2, e3, e4}); } -expr mk_boolcomplete_fn(); -bool is_boolcomplete_fn(expr const & e); -inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); } expr mk_false_elim_fn(); bool is_false_elim_fn(expr const & e); inline expr mk_false_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_false_elim_fn(), e1, e2}); } -expr mk_imp_trans_fn(); -bool is_imp_trans_fn(expr const & e); -inline expr mk_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_imp_eq_trans_fn(); -bool is_imp_eq_trans_fn(expr const & e); -inline expr mk_imp_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_imp_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_eq_imp_trans_fn(); -bool is_eq_imp_trans_fn(expr const & e); -inline expr mk_eq_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_not_not_eq_fn(); -bool is_not_not_eq_fn(expr const & e); -inline expr mk_not_not_eq_th(expr const & e1) { return mk_app({mk_not_not_eq_fn(), e1}); } -expr mk_not_not_elim_fn(); -bool is_not_not_elim_fn(expr const & e); -inline expr mk_not_not_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_not_not_elim_fn(), e1, e2}); } expr mk_mt_fn(); bool is_mt_fn(expr const & e); inline expr mk_mt_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_mt_fn(), e1, e2, e3, e4}); } @@ -132,45 +87,76 @@ inline expr mk_contrapos_th(expr const & e1, expr const & e2, expr const & e3, e expr mk_absurd_elim_fn(); bool is_absurd_elim_fn(expr const & e); inline expr mk_absurd_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_absurd_elim_fn(), e1, e2, e3, e4}); } -expr mk_not_imp_eliml_fn(); -bool is_not_imp_eliml_fn(expr const & e); -inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_eliml_fn(), e1, e2, e3}); } -expr mk_not_imp_elimr_fn(); -bool is_not_imp_elimr_fn(expr const & e); -inline expr mk_not_imp_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_elimr_fn(), e1, e2, e3}); } -expr mk_resolve1_fn(); -bool is_resolve1_fn(expr const & e); -inline expr mk_resolve1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve1_fn(), e1, e2, e3, e4}); } -expr mk_and_intro_fn(); -bool is_and_intro_fn(expr const & e); -inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); } -expr mk_and_eliml_fn(); -bool is_and_eliml_fn(expr const & e); -inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); } -expr mk_and_elimr_fn(); -bool is_and_elimr_fn(expr const & e); -inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); } expr mk_or_introl_fn(); bool is_or_introl_fn(expr const & e); inline expr mk_or_introl_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_introl_fn(), e1, e2, e3}); } expr mk_or_intror_fn(); bool is_or_intror_fn(expr const & e); inline expr mk_or_intror_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_intror_fn(), e1, e2, e3}); } -expr mk_or_elim_fn(); -bool is_or_elim_fn(expr const & e); -inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_refute_fn(); -bool is_refute_fn(expr const & e); -inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_refute_fn(), e1, e2}); } +expr mk_boolcomplete_fn(); +bool is_boolcomplete_fn(expr const & e); +inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); } +expr mk_boolcomplete_swapped_fn(); +bool is_boolcomplete_swapped_fn(expr const & e); +inline expr mk_boolcomplete_swapped_th(expr const & e1) { return mk_app({mk_boolcomplete_swapped_fn(), e1}); } +expr mk_resolve1_fn(); +bool is_resolve1_fn(expr const & e); +inline expr mk_resolve1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve1_fn(), e1, e2, e3, e4}); } +expr mk_subst_fn(); +bool is_subst_fn(expr const & e); +inline expr mk_subst_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_subst_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_substp_fn(); +bool is_substp_fn(expr const & e); +inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); } expr mk_symm_fn(); bool is_symm_fn(expr const & e); inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_symm_fn(), e1, e2, e3, e4}); } -expr mk_eqmpr_fn(); -bool is_eqmpr_fn(expr const & e); -inline expr mk_eqmpr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmpr_fn(), e1, e2, e3, e4}); } expr mk_trans_fn(); bool is_trans_fn(expr const & e); inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_congr1_fn(); +bool is_congr1_fn(expr const & e); +inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_congr2_fn(); +bool is_congr2_fn(expr const & e); +inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr2_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_congr_fn(); +bool is_congr_fn(expr const & e); +inline expr mk_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_true_ne_false(); +bool is_true_ne_false(expr const & e); +expr mk_absurd_not_true_fn(); +bool is_absurd_not_true_fn(expr const & e); +inline expr mk_absurd_not_true_th(expr const & e1) { return mk_app({mk_absurd_not_true_fn(), e1}); } +expr mk_not_false_trivial(); +bool is_not_false_trivial(expr const & e); +expr mk_eqmp_fn(); +bool is_eqmp_fn(expr const & e); +inline expr mk_eqmp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmp_fn(), e1, e2, e3, e4}); } +expr mk_eqmpr_fn(); +bool is_eqmpr_fn(expr const & e); +inline expr mk_eqmpr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmpr_fn(), e1, e2, e3, e4}); } +expr mk_imp_trans_fn(); +bool is_imp_trans_fn(expr const & e); +inline expr mk_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_imp_eq_trans_fn(); +bool is_imp_eq_trans_fn(expr const & e); +inline expr mk_imp_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_imp_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_eq_imp_trans_fn(); +bool is_eq_imp_trans_fn(expr const & e); +inline expr mk_eq_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_to_eq_fn(); +bool is_to_eq_fn(expr const & e); +inline expr mk_to_eq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_eq_fn(), e1, e2, e3, e4}); } +expr mk_to_heq_fn(); +bool is_to_heq_fn(expr const & e); +inline expr mk_to_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_heq_fn(), e1, e2, e3, e4}); } +expr mk_iff_eliml_fn(); +bool is_iff_eliml_fn(expr const & e); +inline expr mk_iff_eliml_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_eliml_fn(), e1, e2, e3, e4}); } +expr mk_iff_elimr_fn(); +bool is_iff_elimr_fn(expr const & e); +inline expr mk_iff_elimr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_elimr_fn(), e1, e2, e3, e4}); } expr mk_ne_symm_fn(); bool is_ne_symm_fn(expr const & e); inline expr mk_ne_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ne_symm_fn(), e1, e2, e3, e4}); } @@ -186,63 +172,73 @@ inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk expr mk_eqf_elim_fn(); bool is_eqf_elim_fn(expr const & e); inline expr mk_eqf_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqf_elim_fn(), e1, e2}); } -expr mk_congr1_fn(); -bool is_congr1_fn(expr const & e); -inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_congr2_fn(); -bool is_congr2_fn(expr const & e); -inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr2_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_congr_fn(); -bool is_congr_fn(expr const & e); -inline expr mk_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } -expr mk_exists_elim_fn(); -bool is_exists_elim_fn(expr const & e); -inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_exists_elim_fn(), e1, e2, e3, e4, e5}); } -expr mk_exists_intro_fn(); -bool is_exists_intro_fn(expr const & e); -inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); } -expr mk_nonempty_elim_fn(); -bool is_nonempty_elim_fn(expr const & e); -inline expr mk_nonempty_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_elim_fn(), e1, e2, e3, e4}); } -expr mk_nonempty_ex_intro_fn(); -bool is_nonempty_ex_intro_fn(expr const & e); -inline expr mk_nonempty_ex_intro_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_ex_intro_fn(), e1, e2, e3}); } -expr mk_exists_to_eps_fn(); -bool is_exists_to_eps_fn(expr const & e); -inline expr mk_exists_to_eps_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_to_eps_fn(), e1, e2, e3}); } -expr mk_axiom_of_choice_fn(); -bool is_axiom_of_choice_fn(expr const & e); -inline expr mk_axiom_of_choice_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_axiom_of_choice_fn(), e1, e2, e3, e4}); } +expr mk_heqt_elim_fn(); +bool is_heqt_elim_fn(expr const & e); +inline expr mk_heqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_heqt_elim_fn(), e1, e2}); } +expr mk_not_true(); +bool is_not_true(expr const & e); +expr mk_not_false(); +bool is_not_false(expr const & e); +expr mk_not_not_eq_fn(); +bool is_not_not_eq_fn(expr const & e); +inline expr mk_not_not_eq_th(expr const & e1) { return mk_app({mk_not_not_eq_fn(), e1}); } +expr mk_not_neq_fn(); +bool is_not_neq_fn(expr const & e); +inline expr mk_not_neq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_neq_fn(), e1, e2, e3}); } +expr mk_not_neq_elim_fn(); +bool is_not_neq_elim_fn(expr const & e); +inline expr mk_not_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_not_neq_elim_fn(), e1, e2, e3, e4}); } +expr mk_not_not_elim_fn(); +bool is_not_not_elim_fn(expr const & e); +inline expr mk_not_not_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_not_not_elim_fn(), e1, e2}); } +expr mk_not_imp_eliml_fn(); +bool is_not_imp_eliml_fn(expr const & e); +inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_eliml_fn(), e1, e2, e3}); } +expr mk_not_imp_elimr_fn(); +bool is_not_imp_elimr_fn(expr const & e); +inline expr mk_not_imp_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_elimr_fn(), e1, e2, e3}); } +expr mk_and_intro_fn(); +bool is_and_intro_fn(expr const & e); +inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); } +expr mk_and_eliml_fn(); +bool is_and_eliml_fn(expr const & e); +inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); } +expr mk_and_elimr_fn(); +bool is_and_elimr_fn(expr const & e); +inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); } +expr mk_or_elim_fn(); +bool is_or_elim_fn(expr const & e); +inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_refute_fn(); +bool is_refute_fn(expr const & e); +inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_refute_fn(), e1, e2}); } expr mk_boolext_fn(); bool is_boolext_fn(expr const & e); inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); } expr mk_iff_intro_fn(); bool is_iff_intro_fn(expr const & e); inline expr mk_iff_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_intro_fn(), e1, e2, e3, e4}); } -expr mk_iff_eliml_fn(); -bool is_iff_eliml_fn(expr const & e); -inline expr mk_iff_eliml_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_eliml_fn(), e1, e2, e3, e4}); } -expr mk_iff_elimr_fn(); -bool is_iff_elimr_fn(expr const & e); -inline expr mk_iff_elimr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_elimr_fn(), e1, e2, e3, e4}); } -expr mk_skolem_th_fn(); -bool is_skolem_th_fn(expr const & e); -inline expr mk_skolem_th_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_skolem_th_fn(), e1, e2, e3}); } expr mk_eqt_intro_fn(); bool is_eqt_intro_fn(expr const & e); inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_intro_fn(), e1, e2}); } expr mk_eqf_intro_fn(); bool is_eqf_intro_fn(expr const & e); inline expr mk_eqf_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqf_intro_fn(), e1, e2}); } -expr mk_neq_elim_fn(); -bool is_neq_elim_fn(expr const & e); -inline expr mk_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_neq_elim_fn(), e1, e2, e3, e4}); } +expr mk_a_neq_a_fn(); +bool is_a_neq_a_fn(expr const & e); +inline expr mk_a_neq_a_th(expr const & e1, expr const & e2) { return mk_app({mk_a_neq_a_fn(), e1, e2}); } expr mk_eq_id_fn(); bool is_eq_id_fn(expr const & e); inline expr mk_eq_id_th(expr const & e1, expr const & e2) { return mk_app({mk_eq_id_fn(), e1, e2}); } expr mk_iff_id_fn(); bool is_iff_id_fn(expr const & e); inline expr mk_iff_id_th(expr const & e1) { return mk_app({mk_iff_id_fn(), e1}); } +expr mk_neq_elim_fn(); +bool is_neq_elim_fn(expr const & e); +inline expr mk_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_neq_elim_fn(), e1, e2, e3, e4}); } +expr mk_neq_to_not_eq_fn(); +bool is_neq_to_not_eq_fn(expr const & e); +inline expr mk_neq_to_not_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_to_not_eq_fn(), e1, e2, e3}); } expr mk_left_comm_fn(); bool is_left_comm_fn(expr const & e); inline expr mk_left_comm_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_left_comm_fn(), e1, e2, e3, e4, e5, e6, e7}); } @@ -273,6 +269,9 @@ inline expr mk_or_tauto_th(expr const & e1) { return mk_app({mk_or_tauto_fn(), e expr mk_or_left_comm_fn(); bool is_or_left_comm_fn(expr const & e); inline expr mk_or_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_left_comm_fn(), e1, e2, e3}); } +expr mk_resolve2_fn(); +bool is_resolve2_fn(expr const & e); +inline expr mk_resolve2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve2_fn(), e1, e2, e3, e4}); } expr mk_and_comm_fn(); bool is_and_comm_fn(expr const & e); inline expr mk_and_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_and_comm_fn(), e1, e2}); } @@ -318,58 +317,15 @@ inline expr mk_imp_id_th(expr const & e1) { return mk_app({mk_imp_id_fn(), e1}); expr mk_imp_or_fn(); bool is_imp_or_fn(expr const & e); inline expr mk_imp_or_th(expr const & e1, expr const & e2) { return mk_app({mk_imp_or_fn(), e1, e2}); } -expr mk_not_true(); -bool is_not_true(expr const & e); -expr mk_not_false(); -bool is_not_false(expr const & e); -expr mk_not_neq_fn(); -bool is_not_neq_fn(expr const & e); -inline expr mk_not_neq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_neq_fn(), e1, e2, e3}); } -expr mk_not_neq_elim_fn(); -bool is_not_neq_elim_fn(expr const & e); -inline expr mk_not_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_not_neq_elim_fn(), e1, e2, e3, e4}); } -expr mk_not_and_fn(); -bool is_not_and_fn(expr const & e); -inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); } -expr mk_not_and_elim_fn(); -bool is_not_and_elim_fn(expr const & e); -inline expr mk_not_and_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_and_elim_fn(), e1, e2, e3}); } -expr mk_not_or_fn(); -bool is_not_or_fn(expr const & e); -inline expr mk_not_or_th(expr const & e1, expr const & e2) { return mk_app({mk_not_or_fn(), e1, e2}); } -expr mk_not_or_elim_fn(); -bool is_not_or_elim_fn(expr const & e); -inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_or_elim_fn(), e1, e2, e3}); } -expr mk_not_iff_fn(); -bool is_not_iff_fn(expr const & e); -inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_not_iff_fn(), e1, e2}); } -expr mk_not_iff_elim_fn(); -bool is_not_iff_elim_fn(expr const & e); -inline expr mk_not_iff_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_iff_elim_fn(), e1, e2, e3}); } -expr mk_not_implies_fn(); -bool is_not_implies_fn(expr const & e); -inline expr mk_not_implies_th(expr const & e1, expr const & e2) { return mk_app({mk_not_implies_fn(), e1, e2}); } -expr mk_not_implies_elim_fn(); -bool is_not_implies_elim_fn(expr const & e); -inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_implies_elim_fn(), e1, e2, e3}); } expr mk_not_congr_fn(); bool is_not_congr_fn(expr const & e); inline expr mk_not_congr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_congr_fn(), e1, e2, e3}); } -expr mk_exists_rem_fn(); -bool is_exists_rem_fn(expr const & e); -inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_rem_fn(), e1, e2, e3}); } -expr mk_forall_rem_fn(); -bool is_forall_rem_fn(expr const & e); -inline expr mk_forall_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_rem_fn(), e1, e2, e3}); } -expr mk_eq_exists_intro_fn(); -bool is_eq_exists_intro_fn(expr const & e); -inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); } -expr mk_not_forall_fn(); -bool is_not_forall_fn(expr const & e); -inline expr mk_not_forall_th(expr const & e1, expr const & e2) { return mk_app({mk_not_forall_fn(), e1, e2}); } -expr mk_not_forall_elim_fn(); -bool is_not_forall_elim_fn(expr const & e); -inline expr mk_not_forall_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_forall_elim_fn(), e1, e2, e3}); } +expr mk_exists_elim_fn(); +bool is_exists_elim_fn(expr const & e); +inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_exists_elim_fn(), e1, e2, e3, e4, e5}); } +expr mk_exists_intro_fn(); +bool is_exists_intro_fn(expr const & e); +inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); } expr mk_not_exists_fn(); bool is_not_exists_fn(expr const & e); inline expr mk_not_exists_th(expr const & e1, expr const & e2) { return mk_app({mk_not_exists_fn(), e1, e2}); } @@ -385,6 +341,28 @@ inline expr mk_exists_unfold2_th(expr const & e1, expr const & e2, expr const & expr mk_exists_unfold_fn(); bool is_exists_unfold_fn(expr const & e); inline expr mk_exists_unfold_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_unfold_fn(), e1, e2, e3}); } +expr mk_inhabited_fn(); +bool is_inhabited_fn(expr const & e); +inline bool is_inhabited(expr const & e) { return is_app(e) && is_inhabited_fn(arg(e, 0)) && num_args(e) == 2; } +inline expr mk_inhabited(expr const & e1) { return mk_app({mk_inhabited_fn(), e1}); } +expr mk_inhabited_intro_fn(); +bool is_inhabited_intro_fn(expr const & e); +inline expr mk_inhabited_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_inhabited_intro_fn(), e1, e2}); } +expr mk_inhabited_elim_fn(); +bool is_inhabited_elim_fn(expr const & e); +inline expr mk_inhabited_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_inhabited_elim_fn(), e1, e2, e3, e4}); } +expr mk_inhabited_ex_intro_fn(); +bool is_inhabited_ex_intro_fn(expr const & e); +inline expr mk_inhabited_ex_intro_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_inhabited_ex_intro_fn(), e1, e2, e3}); } +expr mk_inhabited_range_fn(); +bool is_inhabited_range_fn(expr const & e); +inline expr mk_inhabited_range_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_inhabited_range_fn(), e1, e2, e3, e4}); } +expr mk_exists_rem_fn(); +bool is_exists_rem_fn(expr const & e); +inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_rem_fn(), e1, e2, e3}); } +expr mk_forall_rem_fn(); +bool is_forall_rem_fn(expr const & e); +inline expr mk_forall_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_rem_fn(), e1, e2, e3}); } expr mk_imp_congrr_fn(); bool is_imp_congrr_fn(expr const & e); inline expr mk_imp_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrr_fn(), e1, e2, e3, e4, e5, e6}); } @@ -412,6 +390,50 @@ inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr mk_and_congr_fn(); bool is_and_congr_fn(expr const & e); inline expr mk_and_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congr_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_not_and_fn(); +bool is_not_and_fn(expr const & e); +inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); } +expr mk_not_and_elim_fn(); +bool is_not_and_elim_fn(expr const & e); +inline expr mk_not_and_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_and_elim_fn(), e1, e2, e3}); } +expr mk_not_or_fn(); +bool is_not_or_fn(expr const & e); +inline expr mk_not_or_th(expr const & e1, expr const & e2) { return mk_app({mk_not_or_fn(), e1, e2}); } +expr mk_not_or_elim_fn(); +bool is_not_or_elim_fn(expr const & e); +inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_or_elim_fn(), e1, e2, e3}); } +expr mk_not_implies_fn(); +bool is_not_implies_fn(expr const & e); +inline expr mk_not_implies_th(expr const & e1, expr const & e2) { return mk_app({mk_not_implies_fn(), e1, e2}); } +expr mk_not_implies_elim_fn(); +bool is_not_implies_elim_fn(expr const & e); +inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_implies_elim_fn(), e1, e2, e3}); } +expr mk_a_eq_not_a_fn(); +bool is_a_eq_not_a_fn(expr const & e); +inline expr mk_a_eq_not_a_th(expr const & e1) { return mk_app({mk_a_eq_not_a_fn(), e1}); } +expr mk_a_iff_not_a_fn(); +bool is_a_iff_not_a_fn(expr const & e); +inline expr mk_a_iff_not_a_th(expr const & e1) { return mk_app({mk_a_iff_not_a_fn(), e1}); } +expr mk_true_eq_false(); +bool is_true_eq_false(expr const & e); +expr mk_true_iff_false(); +bool is_true_iff_false(expr const & e); +expr mk_false_eq_true(); +bool is_false_eq_true(expr const & e); +expr mk_false_iff_true(); +bool is_false_iff_true(expr const & e); +expr mk_a_iff_true_fn(); +bool is_a_iff_true_fn(expr const & e); +inline expr mk_a_iff_true_th(expr const & e1) { return mk_app({mk_a_iff_true_fn(), e1}); } +expr mk_a_iff_false_fn(); +bool is_a_iff_false_fn(expr const & e); +inline expr mk_a_iff_false_th(expr const & e1) { return mk_app({mk_a_iff_false_fn(), e1}); } +expr mk_not_iff_fn(); +bool is_not_iff_fn(expr const & e); +inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_not_iff_fn(), e1, e2}); } +expr mk_not_iff_elim_fn(); +bool is_not_iff_elim_fn(expr const & e); +inline expr mk_not_iff_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_iff_elim_fn(), e1, e2, e3}); } expr mk_forall_or_distributer_fn(); bool is_forall_or_distributer_fn(expr const & e); inline expr mk_forall_or_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_or_distributer_fn(), e1, e2, e3}); } @@ -424,18 +446,65 @@ inline expr mk_forall_and_distribute_th(expr const & e1, expr const & e2, expr c expr mk_exists_and_distributer_fn(); bool is_exists_and_distributer_fn(expr const & e); inline expr mk_exists_and_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributer_fn(), e1, e2, e3}); } -expr mk_exists_and_distributel_fn(); -bool is_exists_and_distributel_fn(expr const & e); -inline expr mk_exists_and_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributel_fn(), e1, e2, e3}); } expr mk_exists_or_distribute_fn(); bool is_exists_or_distribute_fn(expr const & e); inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_or_distribute_fn(), e1, e2, e3}); } +expr mk_eq_exists_intro_fn(); +bool is_eq_exists_intro_fn(expr const & e); +inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); } +expr mk_not_forall_fn(); +bool is_not_forall_fn(expr const & e); +inline expr mk_not_forall_th(expr const & e1, expr const & e2) { return mk_app({mk_not_forall_fn(), e1, e2}); } +expr mk_not_forall_elim_fn(); +bool is_not_forall_elim_fn(expr const & e); +inline expr mk_not_forall_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_forall_elim_fn(), e1, e2, e3}); } +expr mk_exists_and_distributel_fn(); +bool is_exists_and_distributel_fn(expr const & e); +inline expr mk_exists_and_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_and_distributel_fn(), e1, e2, e3}); } expr mk_exists_imp_distribute_fn(); bool is_exists_imp_distribute_fn(expr const & e); inline expr mk_exists_imp_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_imp_distribute_fn(), e1, e2, e3}); } -expr mk_nonempty_range_fn(); -bool is_nonempty_range_fn(expr const & e); -inline expr mk_nonempty_range_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_range_fn(), e1, e2, e3, e4}); } +expr mk_forall_uninhabited_fn(); +bool is_forall_uninhabited_fn(expr const & e); +inline expr mk_forall_uninhabited_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_forall_uninhabited_fn(), e1, e2, e3, e4}); } +expr mk_allext_fn(); +bool is_allext_fn(expr const & e); +inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); } +expr mk_funext_fn(); +bool is_funext_fn(expr const & e); +inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); } +expr mk_eta_fn(); +bool is_eta_fn(expr const & e); +inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); } +expr mk_eps_fn(); +bool is_eps_fn(expr const & e); +inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)) && num_args(e) == 4; } +inline expr mk_eps(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_fn(), e1, e2, e3}); } +expr mk_eps_ax_fn(); +bool is_eps_ax_fn(expr const & e); +inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4, e5}); } +expr mk_eps_th_fn(); +bool is_eps_th_fn(expr const & e); +inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_th_fn(), e1, e2, e3, e4}); } +expr mk_eps_singleton_fn(); +bool is_eps_singleton_fn(expr const & e); +inline expr mk_eps_singleton_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_singleton_fn(), e1, e2, e3}); } +expr mk_inhabited_fun_fn(); +bool is_inhabited_fun_fn(expr const & e); +inline expr mk_inhabited_fun_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_inhabited_fun_fn(), e1, e2, e3}); } +expr mk_exists_to_eps_fn(); +bool is_exists_to_eps_fn(expr const & e); +inline expr mk_exists_to_eps_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_to_eps_fn(), e1, e2, e3}); } +expr mk_axiom_of_choice_fn(); +bool is_axiom_of_choice_fn(expr const & e); +inline expr mk_axiom_of_choice_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_axiom_of_choice_fn(), e1, e2, e3, e4}); } +expr mk_skolem_th_fn(); +bool is_skolem_th_fn(expr const & e); +inline expr mk_skolem_th_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_skolem_th_fn(), e1, e2, e3}); } +expr mk_ite_fn(); +bool is_ite_fn(expr const & e); +inline bool is_ite(expr const & e) { return is_app(e) && is_ite_fn(arg(e, 0)) && num_args(e) == 5; } +inline expr mk_ite(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ite_fn(), e1, e2, e3, e4}); } expr mk_if_true_fn(); bool is_if_true_fn(expr const & e); inline expr mk_if_true_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_true_fn(), e1, e2, e3}); } @@ -463,4 +532,19 @@ inline expr mk_eq_if_distributer_th(expr const & e1, expr const & e2, expr const expr mk_eq_if_distributel_fn(); bool is_eq_if_distributel_fn(expr const & e); inline expr mk_eq_if_distributel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributel_fn(), e1, e2, e3, e4, e5}); } +expr mk_injective_fn(); +bool is_injective_fn(expr const & e); +inline bool is_injective(expr const & e) { return is_app(e) && is_injective_fn(arg(e, 0)) && num_args(e) == 4; } +inline expr mk_injective(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_injective_fn(), e1, e2, e3}); } +expr mk_non_surjective_fn(); +bool is_non_surjective_fn(expr const & e); +inline bool is_non_surjective(expr const & e) { return is_app(e) && is_non_surjective_fn(arg(e, 0)) && num_args(e) == 4; } +inline expr mk_non_surjective(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_non_surjective_fn(), e1, e2, e3}); } +expr mk_ind(); +bool is_ind(expr const & e); +expr mk_infinity(); +bool is_infinity(expr const & e); +expr mk_proof_irrel_fn(); +bool is_proof_irrel_fn(expr const & e); +inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); } } diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 965553755..c41c2010f 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -232,21 +232,9 @@ class normalizer::imp { expr r; switch (a.kind()) { - case expr_kind::Pi: { - if (is_arrow(a)) { - expr new_d = reify(normalize(abst_domain(a), s, k), k); - if (is_bool_value(new_d)) { - m_cache.clear(); - expr new_b = reify(normalize(abst_body(a), extend(s, mk_var(k)), k+1), k+1); - if (is_bool_value(new_b)) { - r = mk_bool_value(is_false(new_d) || is_true(new_b)); - break; - } - } - } + case expr_kind::Pi: r = mk_closure(a, m_ctx, s); break; - } case expr_kind::MetaVar: case expr_kind::Lambda: r = mk_closure(a, m_ctx, s); break; diff --git a/src/library/cast_decls.cpp b/src/library/cast_decls.cpp index 57b52a09f..13acd55d3 100644 --- a/src/library/cast_decls.cpp +++ b/src/library/cast_decls.cpp @@ -6,10 +6,4 @@ Released under Apache 2.0 license as described in the file LICENSE. #include "kernel/environment.h" #include "kernel/decl_macros.h" namespace lean { -MK_CONSTANT(cast_fn, name("cast")); -MK_CONSTANT(cast_heq_fn, name("cast_heq")); -MK_CONSTANT(cast_app_fn, name("cast_app")); -MK_CONSTANT(cast_eq_fn, name("cast_eq")); -MK_CONSTANT(cast_trans_fn, name("cast_trans")); -MK_CONSTANT(cast_pull_fn, name("cast_pull")); } diff --git a/src/library/cast_decls.h b/src/library/cast_decls.h index c492859d5..2776d59c2 100644 --- a/src/library/cast_decls.h +++ b/src/library/cast_decls.h @@ -5,23 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE. // Automatically generated file, DO NOT EDIT #include "kernel/expr.h" namespace lean { -expr mk_cast_fn(); -bool is_cast_fn(expr const & e); -inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; } -inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); } -expr mk_cast_heq_fn(); -bool is_cast_heq_fn(expr const & e); -inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); } -expr mk_cast_app_fn(); -bool is_cast_app_fn(expr const & e); -inline expr mk_cast_app_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_cast_app_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } -expr mk_cast_eq_fn(); -bool is_cast_eq_fn(expr const & e); -inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); } -expr mk_cast_trans_fn(); -bool is_cast_trans_fn(expr const & e); -inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_cast_pull_fn(); -bool is_cast_pull_fn(expr const & e); -inline expr mk_cast_pull_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_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); } } diff --git a/src/library/heq_decls.cpp b/src/library/heq_decls.cpp index d96b03b86..70ccf29d6 100644 --- a/src/library/heq_decls.cpp +++ b/src/library/heq_decls.cpp @@ -6,17 +6,17 @@ Released under Apache 2.0 license as described in the file LICENSE. #include "kernel/environment.h" #include "kernel/decl_macros.h" namespace lean { -MK_CONSTANT(heq_fn, name("heq")); -MK_CONSTANT(heq_eq_fn, name("heq_eq")); -MK_CONSTANT(to_eq_fn, name("to_eq")); -MK_CONSTANT(to_heq_fn, name("to_heq")); -MK_CONSTANT(hrefl_fn, name("hrefl")); -MK_CONSTANT(heqt_elim_fn, name("heqt_elim")); +MK_CONSTANT(TypeM, name("TypeM")); +MK_CONSTANT(cast_fn, name("cast")); +MK_CONSTANT(cast_heq_fn, name("cast_heq")); MK_CONSTANT(hsymm_fn, name("hsymm")); MK_CONSTANT(htrans_fn, name("htrans")); MK_CONSTANT(hcongr_fn, name("hcongr")); -MK_CONSTANT(TypeM, name("TypeM")); MK_CONSTANT(hfunext_fn, name("hfunext")); MK_CONSTANT(hsfunext_fn, name("hsfunext")); MK_CONSTANT(hallext_fn, name("hallext")); +MK_CONSTANT(cast_app_fn, name("cast_app")); +MK_CONSTANT(cast_eq_fn, name("cast_eq")); +MK_CONSTANT(cast_trans_fn, name("cast_trans")); +MK_CONSTANT(cast_pull_fn, name("cast_pull")); } diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h index 32336d3c2..4e89e43d1 100644 --- a/src/library/heq_decls.h +++ b/src/library/heq_decls.h @@ -5,25 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE. // Automatically generated file, DO NOT EDIT #include "kernel/expr.h" namespace lean { -expr mk_heq_fn(); -bool is_heq_fn(expr const & e); -inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)) && num_args(e) == 5; } -inline expr mk_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq_fn(), e1, e2, e3, e4}); } -expr mk_heq_eq_fn(); -bool is_heq_eq_fn(expr const & e); -inline expr mk_heq_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_heq_eq_fn(), e1, e2, e3}); } -expr mk_to_eq_fn(); -bool is_to_eq_fn(expr const & e); -inline expr mk_to_eq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_eq_fn(), e1, e2, e3, e4}); } -expr mk_to_heq_fn(); -bool is_to_heq_fn(expr const & e); -inline expr mk_to_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_heq_fn(), e1, e2, e3, e4}); } -expr mk_hrefl_fn(); -bool is_hrefl_fn(expr const & e); -inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); } -expr mk_heqt_elim_fn(); -bool is_heqt_elim_fn(expr const & e); -inline expr mk_heqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_heqt_elim_fn(), e1, e2}); } +expr mk_TypeM(); +bool is_TypeM(expr const & e); +expr mk_cast_fn(); +bool is_cast_fn(expr const & e); +inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; } +inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); } +expr mk_cast_heq_fn(); +bool is_cast_heq_fn(expr const & e); +inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); } expr mk_hsymm_fn(); bool is_hsymm_fn(expr const & e); inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); } @@ -33,8 +23,6 @@ inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr expr mk_hcongr_fn(); bool is_hcongr_fn(expr const & e); inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); } -expr mk_TypeM(); -bool is_TypeM(expr const & e); expr mk_hfunext_fn(); bool is_hfunext_fn(expr const & e); inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } @@ -44,4 +32,16 @@ inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, ex expr mk_hallext_fn(); bool is_hallext_fn(expr const & e); inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_cast_app_fn(); +bool is_cast_app_fn(expr const & e); +inline expr mk_cast_app_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_cast_app_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_cast_eq_fn(); +bool is_cast_eq_fn(expr const & e); +inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); } +expr mk_cast_trans_fn(); +bool is_cast_trans_fn(expr const & e); +inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_cast_pull_fn(); +bool is_cast_pull_fn(expr const & e); +inline expr mk_cast_pull_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_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); } } diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 119400cb7..4bca47168 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -209,7 +209,7 @@ class simplifier_cell::imp { expr ensure_pi(expr const & e) { return m_tc.ensure_pi(e, context(), m_menv.to_some_menv()); } expr normalize(expr const & e) { normalizer & proc = m_tc.get_normalizer(); - return proc(e, context(), m_menv.to_some_menv(), true); + return proc(e, context(), m_menv.to_some_menv()); } expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); } expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lower_free_vars(e, s, d, m_menv.to_some_menv()); } @@ -760,7 +760,7 @@ class simplifier_cell::imp { static bool is_value(expr const & e) { // Currently only semantic attachments are treated as value. // We may relax that in the future. - return ::lean::is_value(e); + return ::lean::is_value(e) || is_true(e) || is_false(e); } /** diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index 979230cc6..f1b2f43fa 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -23,28 +23,12 @@ static void tst0() { env->add_var("n", Nat); expr n = Const("n"); lean_assert_eq(mk_nat_type(), Nat); - lean_assert_eq(norm(mk_Nat_mul(nVal(2), nVal(3))), nVal(6)); - lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True); - lean_assert_eq(norm(mk_Nat_le(nVal(5), nVal(3))), False); - lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True); - lean_assert_eq(norm(mk_Nat_le(n, nVal(3))), mk_Nat_le(n, nVal(3))); env->add_var("x", Real); expr x = Const("x"); lean_assert_eq(mk_real_type(), Real); - lean_assert_eq(norm(mk_Real_mul(rVal(2), rVal(3))), rVal(6)); - lean_assert_eq(norm(mk_Real_div(rVal(2), rVal(0))), rVal(0)); - lean_assert_eq(norm(mk_Real_le(rVal(2), rVal(3))), True); - lean_assert_eq(norm(mk_Real_le(rVal(5), rVal(3))), False); - lean_assert_eq(norm(mk_Real_le(rVal(2), rVal(3))), True); - lean_assert_eq(norm(mk_Real_le(x, rVal(3))), mk_Real_le(x, rVal(3))); env->add_var("i", Int); expr i = Const("i"); - lean_assert_eq(norm(mk_int_to_real(i)), mk_int_to_real(i)); - lean_assert_eq(norm(mk_int_to_real(iVal(2))), rVal(2)); lean_assert_eq(mk_int_type(), Int); - lean_assert_eq(norm(mk_nat_to_int(n)), mk_nat_to_int(n)); - lean_assert_eq(norm(mk_nat_to_int(nVal(2))), iVal(2)); - lean_assert_eq(norm(mk_Int_div(iVal(2), iVal(0))), iVal(0)); } static void tst1() { @@ -62,15 +46,12 @@ static void tst2() { expr e = mk_Int_add(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == iVal(40)); std::cout << type_check(mk_Int_add_fn(), env) << "\n"; lean_assert(type_check(e, env) == Int); lean_assert(type_check(mk_app(mk_Int_add_fn(), iVal(10)), env) == (Int >> Int)); - lean_assert(is_int_value(normalize(e, env))); expr e2 = Fun("a", Int, mk_Int_add(Const("a"), mk_Int_add(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; lean_assert(type_check(e2, env) == mk_arrow(Int, Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_add(Const("a"), iVal(40)))); } static void tst3() { @@ -79,15 +60,12 @@ static void tst3() { expr e = mk_Int_mul(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == iVal(300)); std::cout << type_check(mk_Int_mul_fn(), env) << "\n"; lean_assert(type_check(e, env) == Int); lean_assert(type_check(mk_app(mk_Int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int)); - lean_assert(is_int_value(normalize(e, env))); expr e2 = Fun("a", Int, mk_Int_mul(Const("a"), mk_Int_mul(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; lean_assert(type_check(e2, env) == (Int >> Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_mul(Const("a"), iVal(300)))); } static void tst4() { @@ -96,15 +74,12 @@ static void tst4() { expr e = mk_Int_sub(iVal(10), iVal(30)); std::cout << e << "\n"; std::cout << normalize(e, env) << "\n"; - lean_assert(normalize(e, env, context(), true) == iVal(-20)); std::cout << type_check(mk_Int_sub_fn(), env) << "\n"; lean_assert(type_check(e, env) == Int); lean_assert(type_check(mk_app(mk_Int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int)); - lean_assert(is_int_value(normalize(e, env, context(), true))); expr e2 = Fun("a", Int, mk_Int_sub(Const("a"), mk_Int_sub(iVal(10), iVal(30)))); std::cout << e2 << " --> " << normalize(e2, env) << "\n"; lean_assert(type_check(e2, env) == (Int >> Int)); - lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, mk_Int_add(Const("a"), iVal(20)))); } static void tst5() { @@ -113,8 +88,6 @@ static void tst5() { env->add_var(name("a"), Int); expr e = mk_eq(Int, iVal(3), iVal(4)); std::cout << e << " --> " << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == False); - lean_assert(normalize(mk_eq(Int, Const("a"), iVal(3)), env) == mk_eq(Int, Const("a"), iVal(3))); } static void tst6() { diff --git a/tests/lean/add_assoc.lean.expected.out b/tests/lean/add_assoc.lean.expected.out index 01ea01498..2aeead867 100644 --- a/tests/lean/add_assoc.lean.expected.out +++ b/tests/lean/add_assoc.lean.expected.out @@ -5,7 +5,7 @@ Proved: add_assoc Nat::add_zerol : ∀ a : ℕ, 0 + a = a Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1 -@eq_id : ∀ (A : TypeU) (a : A), a = a ↔ ⊤ +@eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤ theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c := Nat::induction_on a diff --git a/tests/lean/arith1.lean.expected.out b/tests/lean/arith1.lean.expected.out index d17346ec4..9feb47357 100644 --- a/tests/lean/arith1.lean.expected.out +++ b/tests/lean/arith1.lean.expected.out @@ -4,8 +4,8 @@ 10 + 20 : ℕ 10 : ℕ 10 - 20 : ℤ --10 -5 +10 - 20 +25 - 20 15 + 10 - 20 : ℤ Assumed: x Assumed: n diff --git a/tests/lean/arith3.lean.expected.out b/tests/lean/arith3.lean.expected.out index b62ac1b23..0368671eb 100644 --- a/tests/lean/arith3.lean.expected.out +++ b/tests/lean/arith3.lean.expected.out @@ -1,12 +1,12 @@ Set: pp::colors Set: pp::unicode Imported 'Int' +8 mod 3 2 2 -2 -1 +7 mod 3 -8 mod 3 Set: lean::pp::notation Int::mod -8 3 --2 --8 +Int::mod -8 3 +Int::add -6 (Int::mod -8 3) diff --git a/tests/lean/arith6.lean.expected.out b/tests/lean/arith6.lean.expected.out index d61b0bc2f..c2180f2f0 100644 --- a/tests/lean/arith6.lean.expected.out +++ b/tests/lean/arith6.lean.expected.out @@ -3,13 +3,13 @@ Imported 'Int' Set: pp::unicode 3 | 6 -true -false -true -true +3 | 6 +3 | 7 +2 | 6 +1 | 6 Assumed: x -3 + -1 * (x * (3 div x)) = 0 -x + -1 * (3 * (x div 3)) = 0 -false +x | 3 +3 | x +6 | 3 Set: lean::pp::notation Int::divides 3 x diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean index 9a3606615..a24d198be 100644 --- a/tests/lean/arith7.lean +++ b/tests/lean/arith7.lean @@ -1,15 +1,15 @@ import Int. -eval | -2 | +check | -2 | -- Unfortunately, we can't write |-2|, because |- is considered a single token. -- It is not wise to change that since the symbol |- can be used as the notation for -- entailment relation in Lean. eval |3| definition x : Int := -3 -eval |x + 1| -eval |x + 1| > 0 +check |x + 1| +check |x + 1| > 0 variable y : Int -eval |x + y| +check |x + y| print |x + y| > x set_option pp::notation false print |x + y| > x diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out index cf0d53e10..6c03b71d1 100644 --- a/tests/lean/arith7.lean.expected.out +++ b/tests/lean/arith7.lean.expected.out @@ -1,14 +1,13 @@ Set: pp::colors Set: pp::unicode Imported 'Int' -eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥) -3 +| -2 | : ℤ +| 3 | Defined: x -eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥) -eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥) ≤ 0 → ⊥ +| x + 1 | : ℤ +| x + 1 | > 0 : Bool Assumed: y -eps (nonempty_intro (-3 + y)) - (λ r : ℤ, ((0 ≤ -3 + y → r = -3 + y) → ((0 ≤ -3 + y → ⊥) → r = -1 * (-3 + y)) → ⊥) → ⊥) +| x + y | : ℤ | x + y | > x Set: lean::pp::notation Int::gt (Int::abs (Int::add x y)) x diff --git a/tests/lean/cond_tac.lean b/tests/lean/cond_tac.lean index dbdd86820..e592e7065 100644 --- a/tests/lean/cond_tac.lean +++ b/tests/lean/cond_tac.lean @@ -27,12 +27,6 @@ theorem T2 (a b : Bool) : a -> a ∨ b. (* simple_tac *) done -definition x := 10 -theorem T3 : x + 20 +2 >= 2*x. - (* eval_tac() *) - (* trivial_tac() *) - done - theorem T4 (a b c : Bool) : a -> b -> c -> a ∧ b. (* simple2_tac *) exact diff --git a/tests/lean/cond_tac.lean.expected.out b/tests/lean/cond_tac.lean.expected.out index 0646e0988..9a2d840db 100644 --- a/tests/lean/cond_tac.lean.expected.out +++ b/tests/lean/cond_tac.lean.expected.out @@ -5,8 +5,6 @@ Cond result: true Proved: T1 Cond result: false Proved: T2 - Defined: x - Proved: T3 When result: true Proved: T4 When result: false diff --git a/tests/lean/eq4.lean.expected.out b/tests/lean/eq4.lean.expected.out index adbf26673..c860de901 100644 --- a/tests/lean/eq4.lean.expected.out +++ b/tests/lean/eq4.lean.expected.out @@ -2,5 +2,5 @@ Set: pp::unicode Imported 'Int' Imported 'Real' -⊤ -⊤ +1 = 1 +1 = 1 diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out index 875c5f8ed..a823e00e3 100644 --- a/tests/lean/find.lean.expected.out +++ b/tests/lean/find.lean.expected.out @@ -1,8 +1,8 @@ Set: pp::colors Set: pp::unicode Imported 'find' -theorem congr1 {A B : TypeU} {f g : A → B} (a : A) (H : f = g) : f a = g a -theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b -theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b +theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a +theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b +theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo' find.lean:4:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture diff --git a/tests/lean/lua11.lean b/tests/lean/lua11.lean index 0f6f2247b..3c913a025 100644 --- a/tests/lean/lua11.lean +++ b/tests/lean/lua11.lean @@ -38,7 +38,7 @@ import Int. assert(env:find_object("val"):get_weight() == 1) assert(env:find_object("congr"):is_opaque()) assert(env:find_object("congr"):is_theorem()) - assert(env:find_object("refl"):is_axiom()) + assert(env:find_object("hrefl"):is_axiom()) assert(env:find_object(name("Int", "sub")):is_definition()) assert(env:find_object("x"):is_var_decl()) *) diff --git a/tests/lean/map.lean.expected.out b/tests/lean/map.lean.expected.out index 165af9ac7..0d5e86eb1 100644 --- a/tests/lean/map.lean.expected.out +++ b/tests/lean/map.lean.expected.out @@ -9,6 +9,7 @@ Assumed: map_nil Visit, depth: 1, map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) = cons 2 (cons 3 nil) Visit, depth: 2, @eq +Step: @eq ===> @eq Visit, depth: 2, map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) Visit, depth: 3, @map Step: @map ===> @map @@ -64,5 +65,6 @@ Step: map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) ===> cons 2 (cons 3 nil) Rewrite using: eq_id cons 2 (cons 3 nil) = cons 2 (cons 3 nil) ===> ⊤ Visit, depth: 2, ⊤ +Step: ⊤ ===> ⊤ Step: map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) = cons 2 (cons 3 nil) ===> ⊤ Proved: T1 diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean index 49367f870..aede4d619 100644 --- a/tests/lean/norm_tac.lean +++ b/tests/lean/norm_tac.lean @@ -6,7 +6,9 @@ set_option pp::notation false variable vector (A : Type) (sz : Nat) : Type variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A variable V1 : vector Int 10 -definition D := read V1 1 (by trivial) +axiom H : 1 < 10 +add_rewrite H +definition D := read V1 1 (by simp) print environment 1 variable b : Bool definition a := b diff --git a/tests/lean/norm_tac.lean.expected.out b/tests/lean/norm_tac.lean.expected.out index 77c67417f..807b621d4 100644 --- a/tests/lean/norm_tac.lean.expected.out +++ b/tests/lean/norm_tac.lean.expected.out @@ -8,8 +8,9 @@ Assumed: vector Assumed: read Assumed: V1 + Assumed: H Defined: D -definition D : ℤ := @read ℤ 10 V1 1 trivial +definition D : ℤ := @read ℤ 10 V1 1 (@eqt_elim (Nat::lt 1 10) (@refl Bool ⊤)) Assumed: b Defined: a Proved: T diff --git a/tests/lean/revapp.lean b/tests/lean/revapp.lean index c552cdc40..c88e0d89b 100644 --- a/tests/lean/revapp.lean +++ b/tests/lean/revapp.lean @@ -2,29 +2,27 @@ import Int. definition revapp {A : (Type U)} {B : A -> (Type U)} (a : A) (f : forall (x : A), B x) : (B a) := f a. infixl 100 |> : revapp -eval 10 |> (fun x, x + 1) - |> (fun x, x + 2) - |> (fun x, 2 * x) - |> (fun x, 3 - x) - |> (fun x, x + 2) +check 10 |> (fun x, x + 1) + |> (fun x, x + 2) + |> (fun x, 2 * x) + |> (fun x, 3 - x) + |> (fun x, x + 2) definition revcomp {A B C: (Type U)} (f : A -> B) (g : B -> C) : A -> C := fun x, g (f x) infixl 100 #> : revcomp -eval (fun x, x + 1) #> - (fun x, 2 * x * x) #> - (fun x, 10 + x) +check (fun x, x + 1) #> + (fun x, 2 * x * x) #> + (fun x, 10 + x) definition simple := (fun x, x + 1) #> (fun x, 2 * x * x) #> (fun x, 10 + x) check simple -eval simple 10 definition simple2 := (fun x : Int, x + 1) #> (fun x, 2 * x * x) #> (fun x, 10 + x) check simple2 -eval simple2 (-10) diff --git a/tests/lean/revapp.lean.expected.out b/tests/lean/revapp.lean.expected.out index 18cae24d0..e0773c40c 100644 --- a/tests/lean/revapp.lean.expected.out +++ b/tests/lean/revapp.lean.expected.out @@ -2,12 +2,11 @@ Set: pp::unicode Imported 'Int' Defined: revapp --21 +10 |> (λ x : ℕ, x + 1) |> (λ x : ℕ, x + 2) |> (λ x : ℕ, 2 * x) |> (λ x : ℕ, 3 - x) |> (λ x : ℤ, x + 2) : + (λ x : ℤ, ℤ) (10 |> (λ x : ℕ, x + 1) |> (λ x : ℕ, x + 2) |> (λ x : ℕ, 2 * x) |> (λ x : ℕ, 3 - x)) Defined: revcomp -λ x : ℕ, 10 + 2 * (x + 1) * (x + 1) +(λ x : ℕ, x + 1) #> (λ x : ℕ, 2 * x * x) #> (λ x : ℕ, 10 + x) : ℕ → ℕ Defined: simple simple : ℕ → ℕ -252 Defined: simple2 simple2 : ℤ → ℤ -172 diff --git a/tests/lean/rs.lean.expected.out b/tests/lean/rs.lean.expected.out index 9de9a95e3..79db23df8 100644 --- a/tests/lean/rs.lean.expected.out +++ b/tests/lean/rs.lean.expected.out @@ -2,22 +2,22 @@ Set: pp::unicode Assumed: bracket Assumed: bracket_eq -not_false : ¬ ⊥ ↔ ⊤ -not_true : ¬ ⊤ ↔ ⊥ +not_false : (¬ ⊥) = ⊤ +not_true : (¬ ⊤) = ⊥ Nat::mul_comm : ∀ a b : ℕ, a * b = b * a Nat::add_assoc : ∀ a b c : ℕ, a + b + c = a + (b + c) Nat::add_comm : ∀ a b : ℕ, a + b = b + a Nat::add_zeror : ∀ a : ℕ, a + 0 = a -forall_rem [check] : ∀ (A : TypeU) (H : nonempty A) (p : Bool), (A → p) ↔ p -eq_id : ∀ (A : TypeU) (a : A), a = a ↔ ⊤ -exists_rem : ∀ (A : TypeU) (H : nonempty A) (p : Bool), (∃ x : A, p) ↔ p +forall_rem [check] : ∀ (A : TypeU) (H : inhabited A) (p : Bool), (A → p) ↔ p +eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤ +exists_rem : ∀ (A : TypeU) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p exists_and_distributel : ∀ (A : TypeU) (p : Bool) (φ : A → Bool), (∃ x : A, φ x ∧ p) ↔ (∃ x : A, φ x) ∧ p exists_or_distribute : ∀ (A : TypeU) (φ ψ : A → Bool), (∃ x : A, φ x ∨ ψ x) ↔ (∃ x : A, φ x) ∨ (∃ x : A, ψ x) not_and : ∀ a b : Bool, ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b not_neq : ∀ (A : TypeU) (a b : A), ¬ a ≠ b ↔ a = b -not_true : ¬ ⊤ ↔ ⊥ +not_true : (¬ ⊤) = ⊥ and_comm : ∀ a b : Bool, a ∧ b ↔ b ∧ a and_truer : ∀ a : Bool, a ∧ ⊤ ↔ a bracket_eq [check] : ∀ a : Bool, bracket a = a diff --git a/tests/lean/scope.lean.expected.out b/tests/lean/scope.lean.expected.out index 6d58b8c31..d4c08cd2c 100644 --- a/tests/lean/scope.lean.expected.out +++ b/tests/lean/scope.lean.expected.out @@ -28,4 +28,4 @@ theorem Inj (A B : Type) L4 : x = hinv (h x) := symm L2, L5 : x = hinv (h y) := trans L4 L1 in trans L5 L3 -10 +20 - 10 diff --git a/tests/lean/scope_bug1.lean b/tests/lean/scope_bug1.lean index c65eb87ce..0e0ff348e 100644 --- a/tests/lean/scope_bug1.lean +++ b/tests/lean/scope_bug1.lean @@ -10,9 +10,9 @@ scope theorem mul_zerol2 (a : Nat) : 0 * a = 0 := induction_on a - (have 0 * 0 = 0 : trivial) + (have 0 * 0 = 0 : mul_zeror 0) (λ (n : Nat) (iH : 0 * n = 0), calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n ... = 0 + 0 : { iH } - ... = 0 : trivial) + ... = 0 : add_zeror 0) end \ No newline at end of file diff --git a/tests/lean/simp10.lean b/tests/lean/simp10.lean index 482a6534e..a180800f4 100644 --- a/tests/lean/simp10.lean +++ b/tests/lean/simp10.lean @@ -6,6 +6,11 @@ add_rewrite fid axiom gcnst (x : Nat) : g x = 1 add_rewrite gcnst +theorem one_neq_0 : 1 ≠ 0 +:= Nat::succ_nz 0 + +add_rewrite one_neq_0 + (* local t = parse_lean("f a") local r, pr = simplify(t) diff --git a/tests/lean/simp10.lean.expected.out b/tests/lean/simp10.lean.expected.out index 23ed1140c..903a56b3b 100644 --- a/tests/lean/simp10.lean.expected.out +++ b/tests/lean/simp10.lean.expected.out @@ -5,5 +5,8 @@ Assumed: a Assumed: fid Assumed: gcnst + Proved: one_neq_0 a -fid a (eqt_elim (congr1 0 (congr2 neq (gcnst a)))) +fid a + (eqt_elim (trans (trans (congr1 0 (congr2 neq (gcnst a))) neq_to_not_eq) + (trans (congr2 not (neq_elim one_neq_0)) not_false))) diff --git a/tests/lean/simp17.lean b/tests/lean/simp17.lean index facb8e33c..905907de5 100644 --- a/tests/lean/simp17.lean +++ b/tests/lean/simp17.lean @@ -1,5 +1,5 @@ rewrite_set simple -add_rewrite and_truer and_truel and_falser and_falsel or_falsel Nat::add_zeror : simple +add_rewrite and_truer and_truel and_falser and_falsel or_falsel Nat::add_zeror a_neq_a : simple (* add_congr_theorem("simple", "and_congrr") *) diff --git a/tests/lean/simp17.lean.expected.out b/tests/lean/simp17.lean.expected.out index f60787845..ce3f0ca92 100644 --- a/tests/lean/simp17.lean.expected.out +++ b/tests/lean/simp17.lean.expected.out @@ -6,8 +6,9 @@ ⊥ trans (and_congrr (λ C::1 : b = 0 ∧ c = 1, - congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1)))) - (congr1 1 (congr2 Nat::add (and_eliml C::1)))) + trans (congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1)))) + (congr1 1 (congr2 Nat::add (and_eliml C::1)))) + (a_neq_a 1)) (λ C::7 : ⊥, refl (b = 0 ∧ c = 1))) (and_falser (b = 0 ∧ c = 1)) (c + 0 ≠ b + 1 ∧ b = 0 ∧ c = 1) = ⊥ diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out index 3158f973d..df175dcbc 100644 --- a/tests/lean/simp3.lean.expected.out +++ b/tests/lean/simp3.lean.expected.out @@ -1,11 +1,11 @@ Set: pp::colors Set: pp::unicode Defined: double -⊤ +¬ 0 = 1 ⊤ 9 -⊥ -2 + 2 + (2 + 2) + 1 ≥ 3 +0 = 1 +3 ≤ 2 + 2 + (2 + 2) + 1 3 ≤ 2 * 2 + (2 * 2 + (2 * 2 + (2 * 2 + 1))) Assumed: a Assumed: b @@ -32,4 +32,4 @@ a * a + (a * b + (b * a + b * b)) ⊤ → ⊥ refl (⊤ → ⊥) false ⊤ → ⊤ refl (⊤ → ⊤) false ⊥ → ⊤ imp_congr (refl ⊥) (λ C::1 : ⊥, eqt_intro C::1) false -⊥ refl ⊥ false +⊤ ↔ ⊥ refl (⊤ ↔ ⊥) false diff --git a/tests/lean/simp33.lean b/tests/lean/simp33.lean index 6baaf595d..40d1c98dc 100644 --- a/tests/lean/simp33.lean +++ b/tests/lean/simp33.lean @@ -3,7 +3,7 @@ variable f {A : TypeU} : A → A axiom Ax1 (a : Bool) : f a = not a axiom Ax2 (a : Nat) : f a = 0 rewrite_set S -add_rewrite Ax1 Ax2 : S +add_rewrite Ax1 Ax2 not_false : S theorem T1 (a : Nat) : f (f a > 0) := by simp S print environment 1 diff --git a/tests/lean/simp33.lean.expected.out b/tests/lean/simp33.lean.expected.out index 548ef0bd1..224c905c1 100644 --- a/tests/lean/simp33.lean.expected.out +++ b/tests/lean/simp33.lean.expected.out @@ -5,4 +5,5 @@ Assumed: Ax1 Assumed: Ax2 Proved: T1 -theorem T1 (a : ℕ) : f (f a > 0) := eqt_elim (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥)) +theorem T1 (a : ℕ) : f (f a > 0) := + eqt_elim (trans (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥)) not_false) diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out index 8613cfa3a..219860a93 100644 --- a/tests/lean/tst1.lean.expected.out +++ b/tests/lean/tst1.lean.expected.out @@ -25,7 +25,7 @@ definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n := λ (i : N) (H : i < n), f (v1 i H) (v2 i H) select (update (const three ⊥) two ⊤) two two_lt_three : Bool -eps (nonempty_intro ⊤) (λ r : Bool, ((two = two → r = ⊤) → ((two = two → ⊥) → r = ⊥) → ⊥) → ⊥) +if two = two then ⊤ else ⊥ update (const three ⊥) two ⊤ : vector Bool three -------- @@ -45,5 +45,4 @@ map normal form --> f (v1 i H) (v2 i H) update normal form --> -λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), - eps (nonempty_intro d) (λ r : A, ((j = i → r = d) → ((j = i → ⊥) → r = v j H) → ⊥) → ⊥) +λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if j = i then d else v j H diff --git a/tests/lean/tst11.lean b/tests/lean/tst11.lean index 67e2da3cd..25676cc61 100644 --- a/tests/lean/tst11.lean +++ b/tests/lean/tst11.lean @@ -1,12 +1,13 @@ +import tactic definition xor (x y : Bool) : Bool := (not x) = y infixr 50 ⊕ : xor print xor true false -eval xor true true -eval xor true false variable a : Bool print a ⊕ a ⊕ a check @subst theorem EM2 (a : Bool) : a \/ (not a) := - case (fun x : Bool, x \/ (not x)) trivial trivial a + case (fun x : Bool, x \/ (not x)) (by simp) (by simp) a check EM2 check EM2 a +theorem xor_neq (a b : Bool) : (a ⊕ b) ↔ ((¬ a) = b) +:= refl (a ⊕ b) \ No newline at end of file diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out index 02af3b075..74a97ae2f 100644 --- a/tests/lean/tst11.lean.expected.out +++ b/tests/lean/tst11.lean.expected.out @@ -1,12 +1,12 @@ Set: pp::colors Set: pp::unicode + Imported 'tactic' Defined: xor ⊤ ⊕ ⊥ -⊥ -⊤ Assumed: a a ⊕ a ⊕ a -@subst : ∀ (A : TypeU) (a b : A) (P : A → Bool), P a → a = b → P b +@subst : ∀ (A : (Type U)) (a b : A) (P : A → Bool), P a → a = b → P b Proved: EM2 EM2 : ∀ a : Bool, a ∨ ¬ a EM2 a : a ∨ ¬ a + Proved: xor_neq diff --git a/tests/lean/tst12.lean.expected.out b/tests/lean/tst12.lean.expected.out index 6aaf0e525..36e123104 100644 --- a/tests/lean/tst12.lean.expected.out +++ b/tests/lean/tst12.lean.expected.out @@ -6,4 +6,4 @@ let x := ⊤, z := x ∧ y, f := λ arg1 arg2 : Bool, arg1 ∧ arg2 = arg2 ∧ arg1 = arg1 ∨ arg2 ∨ arg2 in f x y ∨ z -⊤ +(⊤ ∧ ⊤ = ⊤ ∧ ⊤ = ⊤ ∨ ⊤ ∨ ⊤) ∨ ⊤ ∧ ⊤ diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out index 81e287196..ea412f86a 100644 --- a/tests/lean/tst17.lean.expected.out +++ b/tests/lean/tst17.lean.expected.out @@ -4,4 +4,4 @@ Assumed: g ∀ a b : Type, ∃ c : Type, g a b = f c ∀ a b : Type, ∃ c : Type, g a b = f c : Bool -∀ (a b : Type), (∀ (x : Type), g a b = f x → ⊥) → ⊥ +∀ a b : Type, ∃ c : Type, g a b = f c diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out index 6201629bc..6f6deefa8 100644 --- a/tests/lean/tst4.lean.expected.out +++ b/tests/lean/tst4.lean.expected.out @@ -10,7 +10,7 @@ Assumed: EqNice @EqNice N n1 n2 @f N n1 n2 : N -@congr : ∀ (A B : TypeU) (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b) +@congr : ∀ (A B : (Type U)) (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b) @f N n1 n2 Assumed: a Assumed: b diff --git a/tests/lean/using_bug1.lean b/tests/lean/using_bug1.lean index 000525919..98abbfe75 100644 --- a/tests/lean/using_bug1.lean +++ b/tests/lean/using_bug1.lean @@ -8,8 +8,8 @@ check add_succr a theorem mul_zerol2 (a : Nat) : 0 * a = 0 := induction_on a - (have 0 * 0 = 0 : trivial) + (have 0 * 0 = 0 : mul_zeror 0) (λ (n : Nat) (iH : 0 * n = 0), calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n ... = 0 + 0 : { iH } - ... = 0 : trivial) + ... = 0 : add_zeror 0) diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index be3ffef34..62cfdc34c 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -26,7 +26,7 @@ assert(not ok) print(msg) assert(child:normalize(Const("val2")) == Const("val2")) local Int = Const("Int") -child:add_theorem("Th1", mk_eq(Int, iVal(0), iVal(0)), Const("trivial")) +child:add_theorem("Th1", mk_eq(Int, iVal(0), iVal(0)), Const("refl")(Int, iVal(0))) child:add_axiom("H1", mk_eq(Int, Const("x"), iVal(0))) assert(child:has_object("H1")) local ctx = context(context(), "x", Const("Int"), iVal(10))