From 759aa61f7069b0d0f296b77f8730cfa584a2f1c5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jan 2014 19:11:58 -0800 Subject: [PATCH] refactor(builtin/kernel): define if-then-else using Hilbert's operator Signed-off-by: Leonardo de Moura --- doc/lean/expr.md | 19 ++-- src/builtin/CMakeLists.txt | 4 +- src/builtin/Int.lean | 1 - src/builtin/Real.lean | 1 - src/builtin/if_then_else.lean | 62 ------------- src/builtin/kernel.lean | 136 +++++++++++++++++++++++----- src/builtin/obj/Int.olean | Bin 1496 -> 1478 bytes src/builtin/obj/Real.olean | Bin 1030 -> 1032 bytes src/builtin/obj/if_then_else.olean | Bin 4903 -> 0 bytes src/builtin/obj/kernel.olean | Bin 29538 -> 37764 bytes src/frontends/lean/frontend.cpp | 2 - src/kernel/kernel_decls.cpp | 19 +++- src/kernel/kernel_decls.h | 58 +++++++++--- src/library/CMakeLists.txt | 2 +- src/library/if_then_else_decls.cpp | 18 ---- src/library/if_then_else_decls.h | 35 ------- src/library/ite.cpp | 64 ------------- src/library/ite.h | 18 ---- src/library/register_module.h | 2 - src/library/simplifier/ceq.cpp | 7 +- tests/lean/arith7.lean.expected.out | 9 +- tests/lean/simp3.lean | 29 +++--- tests/lean/simp3.lean.expected.out | 1 - tests/lean/tst1.lean | 1 - tests/lean/tst1.lean.expected.out | 6 +- tests/lean/tst3.lean | 1 - tests/lean/tst3.lean.expected.out | 1 - tests/lua/ceq1.lua | 1 - 28 files changed, 201 insertions(+), 296 deletions(-) delete mode 100644 src/builtin/if_then_else.lean delete mode 100644 src/builtin/obj/if_then_else.olean delete mode 100644 src/library/if_then_else_decls.cpp delete mode 100644 src/library/if_then_else_decls.h delete mode 100644 src/library/ite.cpp delete mode 100644 src/library/ite.h diff --git a/doc/lean/expr.md b/doc/lean/expr.md index 94922e781..b3bea51c2 100644 --- a/doc/lean/expr.md +++ b/doc/lean/expr.md @@ -34,20 +34,13 @@ eval s + 1 ## Function applications In Lean, the expression `f t` is a function application, where `f` is a function that is applied to `t`. -In the following example, we define the function `max`. The `eval` command evaluates the application `max 1 2`, -and returns the value `2`. Note that, the expression `if (x >= y) then x else y` is also a function application. -It is notation for `ite (x >= y) x y`. +In the following example, we define the function `max`. The `eval` command evaluates the application `double 3`, +and returns the value `6`. ```lean -import if_then_else -definition max (x y : Nat) : Nat := if (x >= y) then x else y -eval max 1 2 -``` - -The expression `max 1` is also a valid expression in Lean, and it has type `Nat -> Nat`. - -```lean -check max 1 +import tactic -- load basic tactics such as 'simp' +definition double (x : Nat) : Nat := x + x +eval double 3 ``` In the following command, we define the function `inc`, and evaluate some expressions using `inc` and `max`. @@ -55,5 +48,5 @@ In the following command, we define the function `inc`, and evaluate some expres ```lean definition inc (x : Nat) : Nat := x + 1 eval inc (inc (inc 2)) -eval max (inc 2) 2 = 3 +eval double (inc 3) ``` diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index f56537fe9..d49b50933 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -89,8 +89,7 @@ endfunction() add_kernel_theory("kernel.lean" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua") add_kernel_theory("Nat.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean") -add_theory("if_then_else.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") -add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean") +add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") add_theory("heq.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") @@ -100,6 +99,5 @@ update_interface("kernel.olean" "kernel" "-n") update_interface("Nat.olean" "library/arith" "-n") update_interface("Int.olean" "library/arith" "") update_interface("Real.olean" "library/arith" "") -update_interface("if_then_else.olean" "library" "") update_interface("heq.olean" "library" "") update_interface("cast.olean" "library" "") \ No newline at end of file diff --git a/src/builtin/Int.lean b/src/builtin/Int.lean index 7ea445896..fe533c68e 100644 --- a/src/builtin/Int.lean +++ b/src/builtin/Int.lean @@ -1,5 +1,4 @@ import Nat -import if_then_else variable Int : Type alias ℤ : Int diff --git a/src/builtin/Real.lean b/src/builtin/Real.lean index 3fd9c420c..45981271f 100644 --- a/src/builtin/Real.lean +++ b/src/builtin/Real.lean @@ -1,5 +1,4 @@ import Int -import if_then_else variable Real : Type alias ℝ : Real diff --git a/src/builtin/if_then_else.lean b/src/builtin/if_then_else.lean deleted file mode 100644 index 71e16f40c..000000000 --- a/src/builtin/if_then_else.lean +++ /dev/null @@ -1,62 +0,0 @@ -import macros - --- if_then_else expression support -builtin ite {A : (Type U)} : Bool → A → A → A -notation 45 if _ then _ else _ : ite - -axiom if_true {A : TypeU} (a b : A) : (if true then a else b) = a -axiom if_false {A : TypeU} (a b : A) : (if false then a else b) = b - -theorem if_a_a {A : TypeU} (c : Bool) (a : A) : (if c then a else a) = a -:= case (λ x, (if x then a else a) = a) (if_true a a) (if_false a a) c - --- Simplify the then branch using the fact that c is true, and the else branch that c is false -theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c) - (H_xu : ∀ (H_c : c), x = u) (H_yv : ∀ (H_nc : ¬ c), y = v) : - (if b then x else y) = if c then u else v -:= or_elim (em c) - (λ H_c : c, calc - (if b then x else y) = if c then x else y : { H_bc } - ... = if true then x else y : { eqt_intro H_c } - ... = x : if_true _ _ - ... = u : H_xu H_c - ... = if true then u else v : symm (if_true _ _) - ... = if c then u else v : { symm (eqt_intro H_c) }) - (λ H_nc : ¬ c, calc - (if b then x else y) = if c then x else y : { H_bc } - ... = if false then x else y : { eqf_intro H_nc } - ... = y : if_false _ _ - ... = v : H_yv H_nc - ... = if false then u else v : symm (if_false _ _) - ... = if c then u else v : { symm (eqf_intro H_nc) }) - -theorem if_imp_then {a b c : Bool} (H : if a then b else c) : a → b -:= assume Ha : a, eqt_elim (calc b = if true then b else c : symm (if_true b c) - ... = if a then b else c : { symm (eqt_intro Ha) } - ... = true : eqt_intro H) - -theorem if_imp_else {a b c : Bool} (H : if a then b else c) : ¬ a → c -:= assume Hna : ¬ a, eqt_elim (calc c = if false then b else c : symm (if_false b c) - ... = if a then b else c : { symm (eqf_intro Hna) } - ... = true : eqt_intro H) - -theorem app_if_distribute {A B : TypeU} (c : Bool) (f : A → B) (a b : A) : f (if c then a else b) = if c then f a else f b -:= or_elim (em c) - (λ Hc : c , calc - f (if c then a else b) = f (if true then a else b) : { eqt_intro Hc } - ... = f a : { if_true a b } - ... = if true then f a else f b : symm (if_true (f a) (f b)) - ... = if c then f a else f b : { symm (eqt_intro Hc) }) - (λ Hnc : ¬ c, calc - f (if c then a else b) = f (if false then a else b) : { eqf_intro Hnc } - ... = f b : { if_false a b } - ... = if false then f a else f b : symm (if_false (f a) (f b)) - ... = if c then f a else f b : { symm (eqf_intro Hnc) }) - -theorem eq_if_distributer {A : TypeU} (c : Bool) (a b v : A) : (v = (if c then a else b)) = if c then v = a else v = b -:= app_if_distribute c (eq v) a b - -theorem eq_if_distributel {A : TypeU} (c : Bool) (a b v : A) : ((if c then a else b) = v) = if c then a = v else b = v -:= app_if_distribute c (λ x, x = v) a b - -set_opaque ite true \ No newline at end of file diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 15659f265..f62506aaf 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -1,4 +1,5 @@ import macros +import tactic universe U ≥ 1 definition TypeU := (Type U) @@ -72,14 +73,24 @@ axiom eps_ax {A : TypeU} (H : nonempty A) {P : A → Bool} (a : A) : P a → P ( -- Proof irrelevance axiom proof_irrel {a : Bool} (H1 H2 : a) : 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 - -- 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 --- We will mark not as opaque later +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 + +-- 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 @@ -119,6 +130,8 @@ theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c 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 @@ -273,6 +286,15 @@ theorem eq_id {A : TypeU} (a : A) : (a = a) ↔ true theorem iff_id (a : Bool) : (a ↔ a) ↔ true := eqt_intro (refl a) +add_rewrite eq_id iff_id + +-- 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)) : + ∀ 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 } + ... = R y (R x z) : assoc y x z + theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a) := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a)) (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b)) @@ -307,6 +329,11 @@ theorem or_truer (a : Bool) : a ∨ true ↔ true theorem or_tauto (a : Bool) : a ∨ ¬ a ↔ true := eqt_intro (em a) +theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) +:= left_comm or_comm or_assoc a b c + +add_rewrite or_comm or_assoc or_id or_falsel or_falser or_truel or_truer or_tauto or_left_comm + 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)) @@ -337,6 +364,11 @@ theorem and_absurd (a : Bool) : a ∧ ¬ a ↔ false := boolext (assume H, absurd (and_eliml H) (and_elimr H)) (assume H, false_elim (a ∧ ¬ a) H) +theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) +:= left_comm and_comm and_assoc a b 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 @@ -352,6 +384,8 @@ theorem imp_falsel (a : Bool) : (false → a) ↔ true theorem imp_id (a : Bool) : (a → a) ↔ true := eqt_intro (λ H : a, H) +add_rewrite imp_truer imp_truel imp_falser imp_falsel imp_id + theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b := iff_intro (assume H : a → b, @@ -371,6 +405,8 @@ theorem not_false : ¬ false ↔ true 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 @@ -464,20 +500,6 @@ 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) - --- 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)) : - ∀ 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 } - ... = R y (R x z) : assoc y x z - -theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) -:= left_comm and_comm and_assoc a b c - -theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) -:= left_comm or_comm or_assoc a b c - -- Congruence theorems for contextual simplification -- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then @@ -487,11 +509,11 @@ theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : (λ H_b : b, or_elim (em c) (λ H_c : c, - calc (a → b) = (a → true) : { eqt_intro H_b } - ... = true : imp_truer a - ... = (c → true) : symm (imp_truer c) - ... = (c → b) : { symm (eqt_intro H_b) } - ... = (c → d) : { H_bd H_c }) + calc (a → b) = (a → true) : { eqt_intro H_b } + ... = true : imp_truer a + ... = (c → true) : symm (imp_truer c) + ... = (c → b) : { symm (eqt_intro H_b) } + ... = (c → d) : { H_bd H_c }) (λ H_nc : ¬ c, calc (a → b) = (a → true) : { eqt_intro H_b } ... = true : imp_truer a @@ -624,8 +646,74 @@ 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 _ _) +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 + +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 + +theorem if_a_a {A : TypeU} (c : Bool) (a: A) : (if c then a else a) = a +:= or_elim (em c) + (λ H : c, calc (if c then a else a) = (if true then a else a) : { eqt_intro H } + ... = a : if_true a a) + (λ H : ¬ c, calc (if c then a else a) = (if false then a else a) : { eqf_intro H } + ... = a : if_false a a) + +theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c) + (H_xu : ∀ (H_c : c), x = u) (H_yv : ∀ (H_nc : ¬ c), y = v) : + (if b then x else y) = if c then u else v +:= or_elim (em c) + (λ H_c : c, calc + (if b then x else y) = if c then x else y : { H_bc } + ... = if true then x else y : { eqt_intro H_c } + ... = x : if_true _ _ + ... = u : H_xu H_c + ... = if true then u else v : symm (if_true _ _) + ... = if c then u else v : { symm (eqt_intro H_c) }) + (λ H_nc : ¬ c, calc + (if b then x else y) = if c then x else y : { H_bc } + ... = if false then x else y : { eqf_intro H_nc } + ... = y : if_false _ _ + ... = v : H_yv H_nc + ... = if false then u else v : symm (if_false _ _) + ... = if c then u else v : { symm (eqf_intro H_nc) }) + +theorem if_imp_then {a b c : Bool} (H : if a then b else c) : a → b +:= assume Ha : a, eqt_elim (calc b = if true then b else c : symm (if_true b c) + ... = if a then b else c : { symm (eqt_intro Ha) } + ... = true : eqt_intro H) + +theorem if_imp_else {a b c : Bool} (H : if a then b else c) : ¬ a → c +:= assume Hna : ¬ a, eqt_elim (calc c = if false then b else c : symm (if_false b c) + ... = if a then b else c : { symm (eqf_intro Hna) } + ... = true : eqt_intro H) + +theorem app_if_distribute {A B : TypeU} (c : Bool) (f : A → B) (a b : A) : f (if c then a else b) = if c then f a else f b +:= or_elim (em c) + (λ Hc : c , calc + f (if c then a else b) = f (if true then a else b) : { eqt_intro Hc } + ... = f a : { if_true a b } + ... = if true then f a else f b : symm (if_true (f a) (f b)) + ... = if c then f a else f b : { symm (eqt_intro Hc) }) + (λ Hnc : ¬ c, calc + f (if c then a else b) = f (if false then a else b) : { eqf_intro Hnc } + ... = f b : { if_false a b } + ... = if false then f a else f b : symm (if_false (f a) (f b)) + ... = if c then f a else f b : { symm (eqf_intro Hnc) }) + +theorem eq_if_distributer {A : TypeU} (c : Bool) (a b v : A) : (v = (if c then a else b)) = if c then v = a else v = b +:= app_if_distribute c (eq v) a b + +theorem eq_if_distributel {A : TypeU} (c : Bool) (a b v : A) : ((if c then a else b) = v) = if c then a = v else b = v +:= app_if_distribute c (λ x, x = v) a b + set_opaque exists true set_opaque not true set_opaque or true set_opaque and true -set_opaque implies true \ No newline at end of file +set_opaque implies true +set_opaque ite true \ No newline at end of file diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean index d648d86f177f5095e28399485ea88486bceead6c..7c50c8c1d497be3278ecfdef185e2d43d4096be6 100644 GIT binary patch delta 96 zcmcb?eT;j8_D1`k%xug|nI)+VlWkaD@t83HffXx=w3uwfYRzNHkdm6lzycC5nOw>~ws2-{L4HvQLuOihNk(d3d}>Z{>PD?!%q)zVC8?9OSYGj%G5~=UD~L3o ytiWo`W5SS3j*2o)$UO=4g~aPv~r85mvjQrt3gQW*defg67S diff --git a/src/builtin/obj/Real.olean b/src/builtin/obj/Real.olean index 502ad6ec3cc51eb6e000283581319d1869f188f4..476bab262d1ad4193f1b8f44690020a26b46809a 100644 GIT binary patch delta 18 ZcmZqU=-}9}m6?s1DYGP%Ve(F9UjQ@#1#kcW delta 16 XcmeC+Xye$hm6?Sxvm|x$Zf0KqEp-KK diff --git a/src/builtin/obj/if_then_else.olean b/src/builtin/obj/if_then_else.olean deleted file mode 100644 index c394d4d08fc519fb919c3693c8967ddbc4650375..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 4903 zcmbtY%WoS+7@wWZZh3@P#LGOyA+;NUTS~-J;?W099ZFL`ye`PHoi$ytSv&SRO8$qQ zXb&7f;+Ru!aOT35roagfoI%_Qcjou|yq?K)qefz+OuqTvkC|^~J;;(y-cPecO-GP! z3Ed#dE1hKH zL`4R992C{rHZuKoF`6VQ)~5~YhdaaMBV`sHrNI&FE`gvPB%6eE19*-opd{cB6D2}; zf-z_Qf?#T*-+^V=zzCopLqk7CSjP+z6}bjP4rpsZmlp0e=pZOAGl)*RxXOh78q+d!y=I_5cKAhiD1fRwBNVhCZK z{}?JuAq-m32+3&0L^%;I1HR9oX94#H`R5}yj~A)#d?c? zA+_4wo)YgVj)@V}LED}f3$3{v*4t*b2FKhDhlm1e2S+%h7R$F&>h%Gw(Knv?s(E2o4R8xV3LYf zoR530=?h?F45HAZaPtf0XsAa?-<;-|1f#Bz`VNpZ%4N*@9V4=inP=^Sr`+y1#&Pi| zIN!rWhgOZnWV2|ec`+IQJKdg|8o5u%CrRM0pjmBN!+2+7x+Tc60%18jR*v4(J@;dp zIh6Zk_0J0P$*c**i)n>M+c4r}3(HTjbvD`Sg&G~8I*Uz!$$TYefA6HJmi=N?%RV4cAeUp4W6%q3r0nUE10lCGYx;`)#iFtZRW|8Lr7`^ z=-cwVy<`?;K{~@>+q|FG({V9MyA$*Jc3!w=Ag0Vyw@1Jfs&B}WPbSSgzNSZ|Jf6~B z=D=TP;hYrGQw9-&?mWZkWKH-%BK445B;}@0 zsq`cUzj#7PuNBZx_4}boea@?F847Gw#C@O6wjg`nZawSy*VaB0^$T>$vz4u=Nr$*0 zs_io#(J%f%fix4oWoYVGYGD_o6^WlDwk1M0A$h}c66xgJ-mft@tB;@aoTVixFO|v$ zCFtyGaxqDNLhD~%lIYYo=tDh_)vjM;dPx$Yd4S?Hpr3tqAonoc@+paXF@0xw7~4NUhSYJmic+6c6rz848Tpq+*&wN3ykqdTmbW0eXE{l(tR<}- zu9jq#Dnb3h5kKFgoDrGgjQ95B*c0$t|w_rs%pNrFPY+xDM zZ7mQKCm&eK%feA2lAuHcdA2N4Ds>)oX`3y8(kuDm6b2p!Ij4Mc*Oo%?A?m4fa(gjH zo(b`=Ow@`IsLoU7UMBw|Pr-w5%1M^E=0#7h|R)AO#;6a<%s=I1E&EBqaC( zA*1*Ji--~NQ;dKW5k$~pMT10qgSFHrLPXPQtyWvK^;N$0|Nr;voVl3?^2Tdftvs)?y=_3%hmtk|@6 z_{^;18`!CXve+;W8 z?FG{0b#9&XYhIIq>cJ#EC#yHU>?k#Y!ant;hu-v|q>VEi9A6E@>@k&%ik~X*As)aD ze&(XsyH2mapX3&hkH@5)$qC5 z@-=I-!v5M%p4W$YHifqYO$SJwhSx4m;Mk@&Pqfo^qURi?--FTXK&odRzz)Ir0Ov|D zeSi;uif94s+W|NDd6NA$*?H)a_lqHl>q)YR(UB2$=pla%fL4yJ0qQe+*5czhnJ1Fu zQyLn0X!;7Zg2qBhV0h!`x~X*(0xAz|7cYupKn;hI2o56#D;5G=qs2*Q}k|6vqIvC@uzg;2~w<*ubMn))AzemQ&|s#kiv}FgiXpIT0xZg~{TMVE?(~ z@EE|-7Zq+)ms!Uet3WBqFNd1zm36e$=Q#!*UK6BI9Rl=yP;@kLf*kB=0L@XBjmtNd zvT1N*RtybV=zvi1({2~bj*%;CZuY!H&lFh8&!<`d6DrZC11gilBV#>g-3NpNP)Oc@ zg2g@C9`YQ$*R5Z*4q@vAv_r*WGFo}6bQ-sXoEoF^$f$+`XDtv~j$$4~!A{G)_>Q;w zR&GBSd}RIj@W$HcOM^%$1mkDKYMf#~b8)+PW!47t0u;#*#&T5R@;LodfH#0*u_|Nl z6=ZM)+Bh6p4VqqN)q&N)v9TGfqTix+aU%X^2c^T$i^ErFOozv_$xw5moKC4d4R}$V zW{9OpifhsE+L|LSlVv;u#BAa+p@Z-=&v$=`J(!rsMhDkr#XYxWa)X!H@?_jV`bKiV z{wBJ|jI(Si(DT+{DwbI+mPR={PJptLvi-Q2Ynf+M@Y>0ViIIWP$;n}usA$N3Fc36G z|C5Q%_Y{V$O)f_3RFHgGxt!Tl zq=dzXmc{W-L%yH)E&#*~ttU?K&DR-PeZ?<}QAg57WHsi0z{+<3A=`10yPn7dKNP{g zi{OU=-baKR1R~(!NBISVSy;wCgpRyRlRV-dUs zpcwu*z~9=U;~1t`A3$Xz7zh48YHgl>Ft^DM@tIpZHZYfBb zLP&G!mKON^6qQY)iqH3AB#Hm)5&TDh($6;x%9kj4*@|kV3V9zu#%cO^;O-u)mO7w* zdbycEEd`G3jSsF$@`n9DQf%D^P;C8k1ixuu?h>hOsLtkfi*p7y3=a%%TsxWN3s8j_ z=1U+`ntHwjoaTKd0+~K}R%-Me;4hcV!FTHUT53>NpWi=Ojgx*l!Q{LuH9hptk3*>( z<$C}%ulpnTeFO93jAcn?t~f^JNmiM#O;&=jeb+D?E0e?PCdM`lAJa4Dn*-3@_rZvo z4QM}=2L1z7ilc`j_(LF^ZG$raf(wVwv5A6-qkfDoDrK;mMk9161vQtJdWZ`4WWe{A5&8FBGDPcx5~c z3~nqvFOWqr6qz`(5)g4_63ta+!Ua^k{0>+Gf6oqPsj@Y#7Jk^@SYsHrnP`R4hd{#R zL=7p(bZb_JGoPoTLw*uUMUqDVlA#=s0|~3Pu*&>0cwAnhcsoHBCqOp=GeqjoKZUUQdUm~ z4h_u5q#W~=rq^v+gM9h~;PgJ!TgImOefV<#io|NEk;kHv`@8&c0BQBP?2!n6irV>y zq1=pu1jvv)_`R%*1FXO^1*`4!R<@(4xk>&fR^w$nY}>6}1PsX{?zbo;8lrMEN&5+) zFOac~`>mXdY?45d0j+@?-nyV)G9x_tsK(6AMHRovm_^d^EO^W@S(HXX+gg?+EtHew z7}06aY5{Bc6Ty(QL+wdB2clLMcMw3vjQmLk<@d1L!2s`#I+LFS)Qmct4#UbVh(yK7 z5S=sR`&&Prk22RC9@rD3BWV_zA%^b6%BB&{N4uu^WPqCHQvhn3@a=quca8iL^mS@B z{{pb0FiAS75Ti#U8yFuBo3K69B*wibYK~KggE4!NPMezR2V0ubp#U`{szg&-h+1iG zkwH##hXedsFU_r}&>_(rc#-DhZD{UbScxPuBx!qfqFbuYWMjIAGNBMykg_yP8DVf_ z**W)q`Ct+vTxSdQu+s|~3#Y>L@VO(q7kV^m?XFfM>hBK``zzIhGG<(p%wl90-BogJIS*}=EDn`&HvyI{_34{|7JKtR9 zqLg3dXzxvEpME)GqDyScCP;s!<&C#GI z8Z!%-TveQdF2zC^fEKoCG7#B31IuT&6$L5_vKD0YmsSUqD;A+-OLK)_jW? zE3CQ$Eb&Zfc4(B!gp0F6n`UZ{%0?X)>?=#KI6son{C$vkzM-}8p43GOzKZw3B6uw) zi+7N6Uqmgp&pj67h$MyWeU@&FHYU5`v9iY;j61=;7@)*`Hb4cRml#yMlDIDgILbK0 zq!Y2apors1gB(Pbw^x*_Lj5a1cDmn+9C5fskV1`&2&bi6>B z+mfXK#liIElna}J+_@N8Q7Q>#Hwo8{of z(TOz!_Wpk8oQct)+ACLu8+%`Px|ycarngZhcg&xBlV0^v`2$tKX=Pf1qCIz_Q?998 z60*hP3z$+bzAaa3enGh&ShDh{b~_(s_sj)c&Y3BH2hr zq2WoS14kC^4?P*BpS4R-L+7f1=na=A+ z6L(yi3LfjsTxB&4W_EFaguW$ImEQ%ekpu6>=rLg{fJwooy&uCT#q*xCx)k5zJ=J)FG7zg_wA#VQFbz?HOO~ z8K35?XzOA;&N7BiOAAI6QjLI?=yDPC&DdR>=@yRSOm?0QT!CVNooyEKtPk3Q55U;j z`^+%73uoxgono-15=+{`$3ailcq>32pIFLcKMup8)~ShB4z0hGld1uI8r0$&68Hw3>9a54lb zpM2U*)A12jX71<9DGd_`la!4LbM$hDMUg_P1f%A6r2fcKNd`4 zN(v!lMhRq!Pg%q7@$9mO1%6F}`pRFTg*hg#w3ZL! zd1oln@n)H%hC(lm_Xxn|BoRP09xqUrKLwI{YKp%@MKHpt!Sz%4OqGjjk}D8SM8R>2 z9H5&Qz!Mi(k$)7R=R8enb`v12SNRc+LraG_VC}Kd zx%??>f5=(}0vT5=_412cvr_TAS=&t9qE9q2ok=#UWi!2MC+jJpQI_zVxKWlce)~w~ zt`_N_EZvyO_Jthe&Xnil@GK!x)X`7#F>7h<<6JKv<5o}xsT|s^#=iiCxMo}IppO2% zS?vh5_UX5l))QiqwriTRwinD4h08K1b_}f~* z!Q(g_%(u!L#VQ-rN&=phN3-JZOJ$JD#1QM1`54vmL<}Oe91y_+2||91@U6uLwT|?2 zSsVq6g`{;voEsM_E;N*BzS7#=Mksa?Pf;7{1WHd0m1$2u?va6nYYopXN2~MEIs$_y z3hp&-ic}X^>zQ8k@S@(4Fd70)QHH=_5<@tdZ1_o>9GRq+T}PS83`0;W2<%L`>Aen+ zo7h9#EI{W*TyEiIW=ni=@hKh)ES)E4@hJ{w4MQrtewMX33W0%=+w%gmOxEJoi}CD_ zds;815ZIAIV8`GM?))IyYl7pYFv}WDvZAO#t<>w_rWmj|ILonq{a6%vpT2~;1 z<_CV*tb`;AVJV4JRu+6Wlvu*3np{X2g%EU#!rU{7LVE*ImK%knN@qt|Zy^cC3n>Qg zu%;$&1coq(mQo(rwvOa{G++d2&ax%Gzf-U{nteITV+by^vh^5(C_trk8jP`E&`aZX zZH);_%8c3`Ya)=Fi(+D(Gf4DW7J=VmUG&wBg%Q@teH{?PRbHmmqy+$-$K+c02LRSK`855P0p#&t@p6E2vsVD**KUY$ ze{G@oYpb^p#5X^%#i`7w75g))!7NM&Gc(v0o^)Nsllk>Gt z>o%w(dmzsH5qr$$>q^DpCGRyUKB7DK@kI})W1kXs5LgE9f^|b@%2pESPQrA-}YRQClyJ__QH*N+Ql~x(|l#Exxj8cE^}J zyKr*w`jVH$^Gx?*qxI!Lk4I{{fmw``b(-8n1lJna`f@`}OkP`h$Kh^J%IDC}zvw8| z*n>M`1!J?sq97@E#>!M6(a$94Np~l4&C=a zKepp--oag^S$OsQG>}Wx!>LLJv@(I`Ti4c48|vYqYn3a*K9|IMsOLOuNYsOG-SO*N zG#Rq8FzBb$1r|m_>PK$<8jK-^UQ2Km{fHv4w2H=Os!CzIw<|@|lKtZ|wMKe-=2fw0 zt4>J@Y*GSFa4@{Znq7m{+(2I%RK$A&$Vf^TMet%&y2VOz4xMA}TJ=epuSUOE9eoX{ zTdGX=)ls`rsA1cuD?v+HHz0+=X@Fw#jRa>=rKe7D>9rQg@p*SKQLoF1Pi<2Bd!{|` z6@5-em(A|Li7JygcB8gbBJ`KN84TYBQj*A}5yU%{{J4hWW%mK~dD7KpAotSMTdg|L z6|Z0Sa6K0e5|>NE!QX53%>#j-H~)n6ZK zrEXZ*8xj#_cAZk6adDH4Ai{;h4l`g;yuj)6hsZCeRd($J;m=y3LEW3>B_2bw@# zQ>P@duBmW~^Xg~ucc?vxwI4R9daZ1@jp{`xIBT>sZ?9el-~z@=u>iZt z?nc2&@4DLxQJ8P z0TAug+eOJ=8*pEphvp;Ee7TZe_@xbnns@17TAEQ3OhND!EuJfT$1GQAT(Ya^c)Wb9 zU4m4%6{N|_#4Zf`ejE^C!Yc+o%{p9rcQ2&lQys7wGX!hyJQTSPWcjwt#jFYBGL!MW+ilM@`)1O0|vaQ33m@Wg~cm zjPbX6SV-V`CX!E0zGZFhZlaxYG7(PRcZEZoaJi^mtR_9%pDr61#I?R<1NuH4eIhHl zUrNu!$I%B?;aq6h0CmKO**=(VasWtC9*~bdaahoqlvcypT!y_Pf>EFr7(JVD=MG7z)D3In8d&;dvw7hMNK$zyDC})i{eSvqkR~9YZ44a#SRcMNetpI zqe^j>-;u$3RJ9P^<8TdXAD*IQC8~~SqFAL`7B^ec(TI|jK;ex(%2IaBQ*otWRXQ`n zEPhg0*|p#HQ82LLCj_l<-vzQ2U}eAU!(qJTORR9-!K)j^Gp)iV*N^%y04DNcKqZ9T zemcPEI$vbgf-;(zH_hM+S4155tx;Ae_kI{E!{C#^0pNAgx;W&Bi zx0`V6!Yrdv#+)UI##}*hu|7oY)i#`c_P-Bhh{T!^klRnjw2EJ$S>gEC5&Z86{!avd zV_^F{cKaQ`O^}vs$9+B*xG=FaC{IJHVwxdC9mwx3KwSi(DSp!c#P{;1E`f>=G>iUc z1XJ|E%BmPz>;MS%LyUIzimD^)s&|nEEl))uE3M-w{h2KkKZ33ZJhF#l4lyvkUTt55 zXU5<7fv@&6tgijc#z-YPV$EwGkK%-eo1;ZOa0z`#GUP4Xbk^uPi`$}k00kzS4b)jk z1oAxKEVH7poYXv)%57f&{29sx>KlM1mj1t~74F(x8l}w^hSW3;0S@AxTIQnV928jL z+PLRDVDGf>(^FIzSwl~AQ=q>H6K;q%SqHAN*7m8uiSdy^oXoVT%ronHOeV0U-cc>H z1lG+M?Q|4x!ifHBHj9VtVP?>=d`%u1-$U#&1q96vD4qh>k+m~mlx=%f?BM6$9N3Mu za|~>6fS4_I0iMsVI4BSa6)4gjgyEr@S)DfCJ~1z$(=ZF(w6yOXc~pt45or5ll`w3B zmt%Nay5v__mV2X8llzkhJ~o1niy$`fN>0l^B?yhRZ=+DKy1B&z(27{exQFTRws>t7 zZX75_htn%>m~_~xl(6L)5_!~XiThUqjKdq;;$ei_n^1g)`hJ3eP9*zAaK8xdAHgRY z*#0`Z9SCrf)D0WV+83at)!z+h9tzxUa4wiHf&6wO1OF9e<)0bujOqVTR{dGBdoZ|> z;>no6`LXuN5qye)HLIS-X;LLKts2NYr3=RVB&!O%;}+7R-4|?fLA+M3B3#R57sT;$P7L!?Z8(!34J5z8m#>$rk_u zMJ}xmfzUN5W84`W7`NRe5&+tGc`HG_=+YN6qPOx@2K-Fx$4gNQ22~J=j>WTrU?dR7 zOhG>?Cou}`^OCG;H3sGNoc2bv{RhQ_72XN&=m_#;O)_5+Yne?ji7Jn^+Rlu3NnVQVu3B4YYGD?CVbx(4 z?nvI&lhyVQY9>cl+4nGFQ8|IV?QCu>0b3*QrQouI`cR={I-EMw>980mr0K+t&z6qE zNPGily%f(pktelAt6D6H9M_E%BpK5~o;e z>l*8(Ip`wTdqGfYHK22>HIK7hhdca;R0mdx&lZXG6<|s?zXDyor1Ce@I(BEiF&8=d7R}PX{RFodNJ5u3kF;qP_E1DBv@l=l5zs7T)2l_X>HUB?Bm_ zALzBigZ||Ca4%yrrcc|5QNGNgIQ*IlO1woPG+0q5#KafbQ%!DIfTH;axtaAlqqmnB z_r3`&S@pdR)IfY~T3v{4K?9qRHZ*S#kWq@4@nwcS^$(Wzit|Yh?P6eQVW8UU zsq0k2_i_MWg6V_otCI;DMs-2t8k6f> z%yBqbXh7nb$#q6kbwg7VBZi&1w`BxTP!W79AgdNb^{I5;0!*qqEM+ULW)|y;A+Xm% z#u+6S40>5t5(qKZ&iPj8wNXjWlS$D#Wl|GBXa>S-t*-NG6xTHZAzQH1=)795GOjaN zv+R5j)f;Ojug`F#L2o6{-9`csgPzbB^v?H=IA)DCQPmcUJ&AeI0veLyLZ5^`JXhPm z%=uLLIs;w!n*yltw;o{Pe7Cnz0j8@vQC#Rv@%F?Ny)^U^mIEtBsdEUJ)$5H!XWEKh zuCxtW$ZsSzOpT)!wGSxA$u>O9eWTv7pb%fb+LJORyqY@i7|`r&hy9lNEVDyLJr+3b zYpeVF4UF$tJ6}Pw4BUXumq3bnK;iDN2d3h_xbxLIku>4+0{oPwYcwgA>cT*WiBJdP z<_3d&SFexqj_)mjG8FqUa+M6m$;a5~#?(iM1mO*3Hk2?*vp{cmcu$MD-<~Bzh9+i3 z?Ggib@VninLuphOCJdrwGm7t95p^AhJtY|y7!LwZ10d_@Y`4OV;$3CZs%ox+gX%|@ zA4Ew-U-6q7cuFzfKdrPUvvn)WH(KHR9;+RV4uk)yGZ?7G$7z~eg{EzFdA*N^Iv%UgLlYzx-oJZnqAtVtPH|bkLo%=-0Q{D zzzUpIH(>rs^{PIA+Fyu`D9ezMV+krQw!+ym1VJlt&s*^fn&LXXMytTT#=H^paV zeGW|-e}BFZe(45`}}NKlvIpTCun;tCFh!oJ}~^L|#ZR&sk7 z$!rC-xW{v`Gvc!rClcMmB5M_%k7*#Gxr@TRA9)!-&Rcg-X^0}nLF2P}lKe|Ur_&AU zYG7D^Q&vPmyLiUFsCy`BO6+*}AvdX@VEG(38ZZgxa-p?*_yVhJlL3A+ zXzL7n?)EbZ<#(fp#C#Z|P{tHmHGOFF_mj%MwTIw;`k>Mu<$#<*bU?Y<|G`jl!1n=E z?fU^X9q^@OE3pJ1aWAaHu^o7(9nQeqg>zB%wo#=s@e>EsM0X&{S@iHc!+BO)WtXqN ziX8^Z{6@%Rbb$dPp;`8_Yv)v z!!-usN99&v0adO+a^2(YS)U6bPozZXYuZ@6$MsRir5L08EGx3B<%^iUbE5940IA#o zXspZN%4a;r7br|cd1>1gpFuk`O-z3XnBnG+GN#^ZPh$1xA|t;JpiCbtyxVYp2p~;g zM`Y}pyq;&CoAq3VNH)6&1eB<|Z8{{HUCe4Lx`*>wZJVv4eK)5}%bWICI{$0okp)(= z{3e$!r>@D1``M>~$R&?vN~XD4O+r;DOQJ;i~NMV>8S zQp+Pt>dQkI+#Kg(%};Uf7_!yBAEe?uDV5#K1~}cTP`rnu<5W%D zxzRaM$xWnu&U39HhM4O=m~sNTlM~4qqr0XK7wQxQQU-*}Vx$%aG=gXLoDuB0jg#)buac`2fi0F+hM) zb-m8vZdN}a>;;6D2F5cD0H!Gw(7x2%iy2Lt&fdMLCo}D%;-v1xSQtPz!|KdfHRtD< z!Smf#&{DOH7BdU1jyG_Mv&>6$2eLRT_(^wrKYGDMy4z7eWmI&||AZA=vDFmn%i>dq78@?)}M-ct(r6`Os{sbHs5SN9;2@I+=;+-3NdkBNpe^=I0uk`?Btx zabUKKy%*ODRx+8H0|z#c>Dv3 zouJm#IY@MWjN&Jd0`DuOin|s~7%YyH#S5|;=l9mEFIw#e^xlfYXnUwQpgQ#!)YXYf zwBp}G6ipqWPxpWQVuu5Vj{fu78oI@~=M7hs_8APj-4fF7gF-6a?jX6uagKo1Y zuZqF7YX?jnz0Z1=8X_~)Ap+*KBLwdA3bB)`RjlFnmC9oEIh#as)4-t6Xcl}m#}zaB zTQMIv1CX)4##E`}mryJ4%K)Y1uK>J{xL*aR)bVQonPkMf2>K_WHMaVIM*G(rIodxt z67C$4~>p7+~@`r&Cj1O$n;F0-2dZ> z8L5Op#^u5sui4Hps`ltN$JXE+68vQ`#UIz0sT6nr>Z&p4AL@lnv#H$Z7ozm+cHc?^+`|i~cURX1(FmIr>M0U(#XX%{&M*_Lr@$}2g=dN6+W@sxeg~jL z@?C%u3Af%1`*S{pT8dYr`j?w=p^@VVxBUr(hf de36(S%l*bihu8V1so^X?d3^PAN5_V<{|kl)F17#w literal 29538 zcmcJ2dz773dH1{D_nh}2CR~gXg-Fmafq*fB$fXKGqL7IVg2pOxIhmQ9fsx5fm`orM z{G%!t>sQ1!t+Ey^s2H%KP{ryh%FUwER_Ic^SIeclHCKJ~C<4No~r=*5yc1 zsUe%S+xVpfbtOwJX`MMeJ2E>lJ%s{S-hUe_j;!#jC3@2{B!?0bsG07|e7hXQ@1hN& z%K+^Q(&TkPKj|y3C_wd4l72?fUwPgtRf58S{Z)@&b8A+|5spl40%GyZw)KjicH~1m zfE)ZQK(er(-ty%nw~Txo(BNa$d8$OagZkS&e$6de9r>8pyk&Btw-v~PcBRI1|Gj^r)oiC1trkiKCyLnD}{i43^iZ+vpVsE2@XFcQfd zP_(#{E#n+oZ{0S!6=CZ%)I-H$GFf@9bQ-sXoIXaEl2LUB&RQTejASWA!A8SDe5YD@ z%h?Y)AKy0B+uqmv>L^kQ!T1@s60aE0Tv?YF7B!&tNU|=B<)p;nH2ihI>mpgH!qj>L z8Qg$6c1KpDrq^0=WOZb6at^C#cT`=j!S7;8-u=?leH)c|_sE+JH73ewU0<#nM0K_y zRwgOVMZGP3j<{BqaUzJ>z-2;9kXss>pJN#l^W?H%pk7DU0zy*i} z_*r>GRi5f)!~zcUDuA*RK+&TnEK`bUy3`ib7U#8tV}%*hLd__vtRIc#b=DyRQt^6& zB#$>}A#f^Z3-Xo;8qMX?L15?%mZESt8zW&7IJ?{j=|YmD@)T!xpp;c{Fqc`0SHSE@ zE`7$X;(T}|el8e7${@2b1ZK*Hv0Jm?{Bn@|@6{Zi=> z5i9sn81`GO#ALqt;_l3h*|^OpBiklt3rJyhX5!L`5h}E(7@T*ZJ^SXYF*3S!+svkU zjdCGcwAkbwY)tT-05!BL0TSz!z|z~T#7piHo85zTn$1h=$@rH?gM==}=HRFomXm{%^3lz`yancar`#C_h9l zZw4qXKb%1MGZAh3;!?#+2|e zD^VcYtX(Nk285x-(V`b7;=>f{U$P0oPbBb@02j0LPJj!ew1&Vv4a>s>=6`&H`je~YLQ2_7K5bNx(}e(x<7%RH_-XX63RF1eaeeQF70)D+qcXVE^5~;f=nrJ zw`d5hu=S7v$g{Nn1&|n)%)xi==bBhh)<3>`t;9DM1I*4b@_7*L9mTCR$(K-| zaXpy8za^HjEXgbo$0!`K!i;UQ5{>PPhT&P6>1~~!ytH@BzzA-eYBZqzY#R7O zC=^EzC-5JDaFTV-aN`!CX63No%YWH2!2qW=&0UEl{c6o8^8<+mV+lpKWvkm=@D zSKut*rD#C&D-=oojTGom|DM4ANZ^mrU<(m`0`L-o{{?U;>2%n}fi}5mZ`cPVf8&s9 zGru4!*{SIDWiDcC;BfvQ_9!VL?x2z&9>?9#h7ehlU5BQOdCerK@JEIa)(>_bvn^j8 zLvcY!t3j!SMArOsfKuBp407+*z7OOK1&MT~dH!W6$n+_POzNeqo(ml6C&r}zwi0Q2 z>yFJ>J)Z`g!G}E*ad8-;hZc^R)lx0LWK)8_0w}BhH9(E&HvkVi66qf!Apsc-TfLiw zse=v3Q?SD{uwAT2!bUM>JY^+8#y#6y?IvKz)YI;YLZTr$nhB-tO3)Wr0p#w=Ni#5p zg0nms@N*!#wnrSkuab zyKN_1Who7w+HubS$BY>c>k4-}5uOR~j-)e^6)UJOsI#3z0I{2pTM&u8$Pm3VIJDro z8TMCGz3$U7I+A9h5u&F~DkLlHMXb{+G|c^oiay=`05!}5kiRduhI=1l*iasYz?^Zcm!y5K?Dcy-25&o@&TEmk}D$v%wer$~_05hQv8o!^dLK zYYy)29vY;%4IrCq4!lTn@-|d=l1LIml6Fw%vkWa)XSNO98|$VdWK!rju6rC7^zLEG zfIC&m;1D2521@`+2G0j5860Ymdz8&!GEdWblMFcA0oMCGBNm6-yTtZ^wt|fTJWj*+ z7@BA51ppOGUI_4>6hIhTGP47_itDUl_YVX?A7*t5)4fZ^chl{?hNB}q$6%>$F{3xZ zpd7jl5isOLGr`Q-FM@#*n8#2glMN<{Y|1M!5BWJY1MxQrepgDyQs*OPA|1AXNK3 z+bV)cDkMHIm6}|z6BC5W(goqeTygWqbziuZ?`@BVAaO8J18a4>K$+W=r2xgwbf0%3 zI#-ap0HB7{1t>jiG^l(VoTuDsiN~c-D3flD(hgJ3A1q~9XtAd4$7F`;$JFJnkxKEQ zL5nDiE|W%_w$Ha>uRSl!+39ZMx;7gyu-`^=&|;8dUdr&7*`^wKTb0w_P$k7Mg^pCt5-$;cRaEWyt10djl)U zErqp`!nzn8Nm!ErdFSXh8&uv%ge?F+gg8@PX-UDVUBLkLc!12)eI=oFXem=bj4UZJ z45_>=HH1SrNJ@dUybVy;h`YB~CPXJ(rRhb1T-ajtD3B>2JNm^B4(CT%?QR}I0T;;R zL#hJk$f(?!5)}AW;A`r;99TDFI&;?!BGbI3Bkh)t*N}%8jXfVln&X~MtUcRp-|@6Tqu(YtMNc*ly+a<4UN0!HaaAw4d5!f7iD{l zqxj4+q6=4vZx zFteK@B(yD`w8Y&Et++o#fjFQi2z-wfk^}kb0tp1DL7ag4dH6q8;(6G5vHAbz#_N{V zXoB|@oG{88qk_s05j+mn_SAybT5JqaPzPsJKo$l62*`?pJcv^igo%|midpE#;$V$m z*&Ml%-onLMxr=p3S|)7#wzvtOWH6gM(tz~q7!!{`8&1xf0^^$k<2yMj+PWA|qhyS| z4ISFTU|e=)1T;xk^bE%C@_0XSl*h9%#^(=p3@8^P8&_JG6+-~V-af1iqq}f~{^ThI zTPm@lE!+fpGJp>N_ zg6njti%h8JJAmF%9}s_0yp~NUKPoGB_i?M#*cnr^XF}>Ebw#UXqW(Ssy1Xu`Uf$52 zP*ayMr-H8n?Apg3)$|=QDWu^gzB^=v1NfVSpK5*Qv_$bzOrmHjJH;uWH4-e6_su zk*{pk)Z|MnsdG!+R{^%seOlyJ*ITv{hl<9Z1eUHvJKS)%hgcFcgfDL95k>`Micc~4 zYsmW;yeuq3puXyZsNsxVd>;7^BmY25^8V%-q`E>Y_4iGH%|T+yQ-6GZTHOF7wbT$F zK|zfFvm@JP@$EvN9Rgtu67}#AqulNd(wBYd*2AgRyPguy%oE5?rG1lEUZWudj`Hzl`YTqoN6QQeo2y#JqLpBPC5E3aol8h#tXV zu(KvZpef1_eguk{Aut~e;YW!dYS}kb9986yl(Je7d?4p$aHt|TqK6jZ=Ene=q2p&( zR*5gg$L|138wejCf5?*P_47;@NeGP1T95xHnrA}z74l(!SN$sLS;oPJK}3b$FeH1W zD1;NFFwZnWeuS+~Ep@yrXo#T&@2$icI;(y`d?a27KLMOVU-LyjIn-R9gs>V-Bm~k+ zLTK%;D(SklKZM|FlxcaCqR>JV%5qb@Qeg-ggM}m<2x)?^&IcH7m;p3Xpd-cprvQ@K z;`8~G)>?v!2Vz2#2-N2oVxUelR2XYpQ}-LRA4L6ykubZ6)CVgV$on8!4XP!3;e1u> zLMaN1)nWL9Z5AkBLc(E}Y%++kqk%)7m_)|r&Iw`6l&IVmR7*0NX4BS7g6@bI3FaT+ z#uHkZ7FbwJkn41B0iexp7`IE7as(CSu~;UBw$v#u>X9iHA8AS2oVi62Q8)ek(oM5H z*3nuhWD8q_M(02YcTxHKUM@0K#j&9|@LG0q66h?qJP(qEr#Op3f2Ot!Aa*9s5%pH& zA;;DlK)SyEB|#(x!CqB@Bb z+|1txB+!WKM^s`^>NrvFhOD;WYA34y~Ac!U+UdJQ#k@zT1SvvYYU z+T|P~2pB3mq{2WCv$eUL`bLD*o2S_SUOFth>_`ijI zs_SF(r=cI)-8NrTjbco?7_{H5t0K8vJ*$XAO}!+6$FM;|Jv{Ph-5~WKtPWJqi>)|Q z55BG6qyLmok~iuji}x=@7t+sh1n1FDBA^*5<*6z?*Bb0f3AI8matrc8t&tubiphLl zl_<6PDM^7%O2CN@h9l8EXz-RuUm8@zI|*bYrQb>5%MEPZl4~$FPEOU*ks5PyH{373aDm)AshMARD z0+X-c{EI8(*^s6jJ{c)rW5rq-jZe?mUqt9WEm>Kkatai+26`hvt&H9TP;xm3V3JE{ z;N?kuOP&4|&RsC|yDXtXkU7l?~S@=9EuuPyk5U z&qHzu9Zyr{Y1bh@|ADu>?+&&3L3Z^4#{F~8{ z6buJw9}V`3yHkseC|#|1*+X3xr=p@Rw&E;a%7piu^pxZ_H`! zNpVkAlC$A7hMi=M7NIv6X%yKfA!t>e4FWu9Xipjkw(BNw47fUz#Myg#Y$XDe0J~+i zv=SL`JG_g!9StG!&9iPs_$b)3V?9sxBxQ;^5lxqyZ3wl!4JN}Wj7{4VI#(vuU2KY^ z!DD&6m8sJ>xgn4ZvYcb1tJ!K`kmX41Aeg-%PVu2J-h5s~o38z9AKbRId?)g%emU1cDl_g9rEKf5MYH0y)9;g?UX#P@iRPXIFV3USTJxw-5yWIXpgNG(RBlz z%*4M|k0i#_EmNMx>1zhAuEu~B_>eK<5jUas^~B~RFgOaMxBBj!$FB*~PCjG~_ z_zuwVGrOjBx%zziqB1a*x6eg#9p%m|G|BxsEA?`JFF?IBdcvUgxg084;zWh(cA&J+ z<@~hU#hQ?=6B2mNb4~sNC~(Lw=;$P*5sAj&_%P^7*;HK=_Tm3lqEdkEeD@QcB)Eu4Ek z+JO&*S6)ynf;^~hQfHE~A<@m+f43+6OfcyBYp{5(N<{w~DCC`E=8X~-DDwrYFuxAW zM=%JkcEZ;tmMu>Jdy<=+B{??#l7I>k7W^mUyNGW|oBiKAgeo@5h8Lz$h}-)Xu3B?* zlm+IeYIOH-3S|weM<}|3&_VWB4KkJ8f-3FaZcX4v2(GB?S4n+yk;W~0^$V1`e+EXr zM#5smPL%eNzw^l-=6Oz{P7Ak>A}^+HOW?-{GGzQGK_qBe-9VN;i+q!%3A^9nzBap= zjJF5ot!!f=+!TPd-4Q%$THDnhJJIJd+0(xb>;wp-IObj36$yy6cGTp-z@WJ!1iK-E zx3iGo9SQu)1b!lcpER)MjZ66{fE8>}7ZT{b>Y=c;422Asi0Iu>%i7kli8_Q*apWTv z%~8p(t**8|VHpO&*8Y8n$L6A-JRw9mTH^`UtlSqprMD#YemM%SNbCKZDAqzX2Q+K) z-gLjpL8m9=aw6VEX}giX$isY4{&i{TKK8GEmhuEG$-ItgsrQ4?RXCOqRsHcE_y2%f zo)ANXkPkp<1!30|<4&-i_#(5mra~cidUN=KS$gitSIWyHccCfT*9Y`>?Hi$no6yv$ zYIsbrn@;btR>Z2Gh4wn)N18svVZj|Buo04XQ9ar z2xZF>Z<}clp7cDDy9ce%*6pY*Ety9g^^;T@&#L~;wUXi0Z^d;L2Eel&@6{S_)1`2Z zygPS5)qY4IIvIZ&idN2C+0WGn8Z8RW0q&)e#h_#Viuy(K=>Z6k?_7UFTZw-@-HA0i zQ|_!Fi;>i)BU#h1X^M+?^Mi*2^!ijJSZ~%REkpVeOJs5odHwP*fqmR^@nh8(jP&3RI6ZoYBKA6D2HL!j& z?6mxQfc~*55d6oJ1W}a*<(<%~m}bb3v4I6%?A8k*G{tXQ2d(Xj@8PB{K@}lr9{tY= zrf9<{b&lHm!YpJ`AK0&YA6Za?MMEts?Z?pvH1mbxe?U_N9@)dQ4>vHqJgCQ!XZ%gy z;?##&S$$}uC)hV}_}ONCc*D&%pqf5_{c(4SGIVZ`4CirMqfxI$g25Kueikx;90eR0 zd})6q(R!nD>oMTZQ7%w>{~y!}cP*&aX7p*HOAUkKg%is8v8b$HgXB;oGkX%%I9d*h z_6qdl1H_xn131~JkL?#CgE*O~v396W?AN2%XAi0_#N}_cA0GTT+C-*jPSb znYlqH?%D>dnVU;M&^!l;q6F6eK45$!f!|Evw-Wem1M71jW{X{bD}H}oA`<#gM9XFH zvg3)hDCVk8tJk=%{+gA?QP|>o?-#O0pf3Gll`w3BADZ#$bv4GY_B|A8od1--M-%v1 z0v|WfFHWBz2#wY6uYrNt&Ck7nHl#uh6&mK#^S)WQaX*wCPVeu#XcQ&#UCYdo$X?GS z{!NZEV)Z$G@&J4uk`GWM-#5^UeXuFrkvU zRt;oq{FCbb!!nU~y^yv)ak5w2G7zmYYvzM)|Ah(nxR}x?YZh)?>G)2sRZ1Yc4;72I!_93u`*qwv@}DS-(G^$ffl~30;HA$Lr4Sl!5}pB^m?HZ_rWr8z0eXe=C>!Duwn;ur8Tk zV)h`m9v;Ll!-HI*512@x;khnnqhdLQLsJW*s9+#*6#mB8=95kKze>zZjM^W`gBza4 z)^@tNg@DbG4_`%S$q;@WjKm7J<9DI6L9Q~{l@8pQx3f%-1H_da^&)^g8LXZSPy%=k zKyDn%Ck*QBPYqKn6v&hxQimrAT4bTO{7I&5t<)Qbz0PV|udrqsgI;BxX@%*qzr(*| z%X%H|@bjz=7k}}BX~S}KL&A}+?wk?3L9cUQJjR46rxjo)JuKx)pZ>s*e+=3cx-}tB zB#p?x6(v?|MQ1UDO_tPuq zQ9K9n$~zpTOEC7dvFyCqvK?4KXVst@7xm6Q2LxtaBQqqjTBhpz$6VhKmOBG{Q^ z#ObDsYFR$>8!g*8fCi7zdxKvAkT*!xQ2;Z8UrmG82j6rN|G_uVrjUeB0XqDwSYJGB zW^Is+%;|2F!T9~di2hohjP}*81!`waM1x91U1-dcD59jCgMP`kZ2CH=SrcS^gth3q z4C%Gclq%#9E7O2JDa|yHUO}{% zpjp(wc^FsoK@b@w6Pz~kKXOBT>VHMqH;pGdw4-NJ+%0s}ciVg!OU9F0blF4hv+dAM zpp7wNP+1_Uut7cPvJprf8qES?(i$?%5YR5j253#%ha|2sxXy*CH8ddc%;mc1f@|M3 zHF1LFi=9bS;u?j#)RWzbq5h$C=mS)DoXQYH=drF70tZcGhs zQjtqyR6=9WJ3lz$$yVMcs=g`z>BPKb0S!qZ#OH6Ykmp5ihkx6mdKKy=saFG3_&Xh7 z=6pBQC;-!K2&BCvnBonYDF$ii4Fx+^j8bE++4eH-xF2}x0LNgRTP*Rt1Xo#OMSZR^VfTi6w?0Uc zO1=`dh+QLJ+AFpZ`&|?p?Vs7YrPZ4(@qU8CChsS22H1=!-(Uw6+v!%#xYYS3^qd8k z3~6;l`tCp^8be|=Q9soh76>?XnZWtstm$Zi#AuI z9rT~hE8F0#eLBXkrCxqzCN`2Rcy>^TJ lAC&$Dp)&URu@Gb*s0gr?lZVV6`5!I1S5Iv^9sjT9{{m=Tz4!nC diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 0f405df64..1ae8a955d 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -20,7 +20,6 @@ Author: Leonardo de Moura #include "kernel/kernel.h" #include "kernel/io_state.h" #include "library/io_state_stream.h" -#include "library/ite.h" #include "library/expr_pair.h" #include "library/expr_pair_maps.h" #include "library/arith/nat.h" @@ -557,7 +556,6 @@ io_state init_frontend(environment const & env, bool no_kernel) { io_state init_test_frontend(environment const & env) { env->set_trusted_imported(true); io_state ios = init_frontend(env); - import_ite(env, ios); import_int(env, ios); import_real(env, ios); return ios; diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index cdc5393be..72c05cbad 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -26,8 +26,10 @@ 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(eps_th_fn, name("eps_th")); MK_CONSTANT(substp_fn, name("substp")); +MK_CONSTANT(eps_th_fn, name("eps_th")); +MK_CONSTANT(eps_singleton_fn, name("eps_singleton")); +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")); @@ -80,6 +82,7 @@ MK_CONSTANT(eqf_intro_fn, name("eqf_intro")); MK_CONSTANT(neq_elim_fn, name("neq_elim")); MK_CONSTANT(eq_id_fn, name("eq_id")); MK_CONSTANT(iff_id_fn, name("iff_id")); +MK_CONSTANT(left_comm_fn, name("left_comm")); MK_CONSTANT(or_comm_fn, name("or_comm")); MK_CONSTANT(or_assoc_fn, name("or_assoc")); MK_CONSTANT(or_id_fn, name("or_id")); @@ -88,6 +91,7 @@ MK_CONSTANT(or_falser_fn, name("or_falser")); 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(and_comm_fn, name("and_comm")); MK_CONSTANT(and_id_fn, name("and_id")); MK_CONSTANT(and_assoc_fn, name("and_assoc")); @@ -96,6 +100,7 @@ MK_CONSTANT(and_truel_fn, name("and_truel")); MK_CONSTANT(and_falsel_fn, name("and_falsel")); MK_CONSTANT(and_falser_fn, name("and_falser")); MK_CONSTANT(and_absurd_fn, name("and_absurd")); +MK_CONSTANT(and_left_comm_fn, name("and_left_comm")); MK_CONSTANT(imp_truer_fn, name("imp_truer")); MK_CONSTANT(imp_truel_fn, name("imp_truel")); MK_CONSTANT(imp_falser_fn, name("imp_falser")); @@ -125,9 +130,6 @@ 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(left_comm_fn, name("left_comm")); -MK_CONSTANT(and_left_comm_fn, name("and_left_comm")); -MK_CONSTANT(or_left_comm_fn, name("or_left_comm")); MK_CONSTANT(imp_congrr_fn, name("imp_congrr")); MK_CONSTANT(imp_congrl_fn, name("imp_congrl")); MK_CONSTANT(imp_congr_fn, name("imp_congr")); @@ -144,4 +146,13 @@ 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(exists_imp_distribute_fn, name("exists_imp_distribute")); +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")); +MK_CONSTANT(if_congr_fn, name("if_congr")); +MK_CONSTANT(if_imp_then_fn, name("if_imp_then")); +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")); } diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 6ce37104b..d5d9f9438 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -72,12 +72,19 @@ inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr 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_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_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_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}); } @@ -233,6 +240,9 @@ inline expr mk_eq_id_th(expr const & e1, expr const & e2) { return mk_app({mk_eq 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_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}); } expr mk_or_comm_fn(); bool is_or_comm_fn(expr const & e); inline expr mk_or_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_or_comm_fn(), e1, e2}); } @@ -257,6 +267,9 @@ inline expr mk_or_truer_th(expr const & e1) { return mk_app({mk_or_truer_fn(), e expr mk_or_tauto_fn(); bool is_or_tauto_fn(expr const & e); inline expr mk_or_tauto_th(expr const & e1) { return mk_app({mk_or_tauto_fn(), e1}); } +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_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}); } @@ -281,6 +294,9 @@ inline expr mk_and_falser_th(expr const & e1) { return mk_app({mk_and_falser_fn( expr mk_and_absurd_fn(); bool is_and_absurd_fn(expr const & e); inline expr mk_and_absurd_th(expr const & e1) { return mk_app({mk_and_absurd_fn(), e1}); } +expr mk_and_left_comm_fn(); +bool is_and_left_comm_fn(expr const & e); +inline expr mk_and_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_left_comm_fn(), e1, e2, e3}); } expr mk_imp_truer_fn(); bool is_imp_truer_fn(expr const & e); inline expr mk_imp_truer_th(expr const & e1) { return mk_app({mk_imp_truer_fn(), e1}); } @@ -366,15 +382,6 @@ 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_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}); } -expr mk_and_left_comm_fn(); -bool is_and_left_comm_fn(expr const & e); -inline expr mk_and_left_comm_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_left_comm_fn(), e1, e2, e3}); } -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_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}); } @@ -423,4 +430,31 @@ inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr co 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_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}); } +expr mk_if_false_fn(); +bool is_if_false_fn(expr const & e); +inline expr mk_if_false_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_false_fn(), e1, e2, e3}); } +expr mk_if_a_a_fn(); +bool is_if_a_a_fn(expr const & e); +inline expr mk_if_a_a_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_a_a_fn(), e1, e2, e3}); } +expr mk_if_congr_fn(); +bool is_if_congr_fn(expr const & e); +inline expr mk_if_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, expr const & e9, expr const & e10) { return mk_app({mk_if_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); } +expr mk_if_imp_then_fn(); +bool is_if_imp_then_fn(expr const & e); +inline expr mk_if_imp_then_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_then_fn(), e1, e2, e3, e4, e5}); } +expr mk_if_imp_else_fn(); +bool is_if_imp_else_fn(expr const & e); +inline expr mk_if_imp_else_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_else_fn(), e1, e2, e3, e4, e5}); } +expr mk_app_if_distribute_fn(); +bool is_app_if_distribute_fn(expr const & e); +inline expr mk_app_if_distribute_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_app_if_distribute_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_eq_if_distributer_fn(); +bool is_eq_if_distributer_fn(expr const & e); +inline expr mk_eq_if_distributer_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributer_fn(), e1, e2, e3, e4, e5}); } +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}); } } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 18d005588..c30e4b17b 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(library kernel_bindings.cpp deep_copy.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp - hop_match.cpp ite.cpp heq_decls.cpp cast_decls.cpp) + hop_match.cpp heq_decls.cpp cast_decls.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/if_then_else_decls.cpp b/src/library/if_then_else_decls.cpp deleted file mode 100644 index 91dfc556a..000000000 --- a/src/library/if_then_else_decls.cpp +++ /dev/null @@ -1,18 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -*/ -// Automatically generated file, DO NOT EDIT -#include "kernel/environment.h" -#include "kernel/decl_macros.h" -namespace lean { -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")); -MK_CONSTANT(if_congr_fn, name("if_congr")); -MK_CONSTANT(if_imp_then_fn, name("if_imp_then")); -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")); -} diff --git a/src/library/if_then_else_decls.h b/src/library/if_then_else_decls.h deleted file mode 100644 index af787b429..000000000 --- a/src/library/if_then_else_decls.h +++ /dev/null @@ -1,35 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -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_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}); } -expr mk_if_false_fn(); -bool is_if_false_fn(expr const & e); -inline expr mk_if_false_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_false_fn(), e1, e2, e3}); } -expr mk_if_a_a_fn(); -bool is_if_a_a_fn(expr const & e); -inline expr mk_if_a_a_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_if_a_a_fn(), e1, e2, e3}); } -expr mk_if_congr_fn(); -bool is_if_congr_fn(expr const & e); -inline expr mk_if_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, expr const & e9, expr const & e10) { return mk_app({mk_if_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); } -expr mk_if_imp_then_fn(); -bool is_if_imp_then_fn(expr const & e); -inline expr mk_if_imp_then_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_then_fn(), e1, e2, e3, e4, e5}); } -expr mk_if_imp_else_fn(); -bool is_if_imp_else_fn(expr const & e); -inline expr mk_if_imp_else_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_if_imp_else_fn(), e1, e2, e3, e4, e5}); } -expr mk_app_if_distribute_fn(); -bool is_app_if_distribute_fn(expr const & e); -inline expr mk_app_if_distribute_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_app_if_distribute_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_eq_if_distributer_fn(); -bool is_eq_if_distributer_fn(expr const & e); -inline expr mk_eq_if_distributer_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eq_if_distributer_fn(), e1, e2, e3, e4, e5}); } -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}); } -} diff --git a/src/library/ite.cpp b/src/library/ite.cpp deleted file mode 100644 index 42fa98ff9..000000000 --- a/src/library/ite.cpp +++ /dev/null @@ -1,64 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/kernel.h" -#include "kernel/abstract.h" -#include "kernel/decl_macros.h" -#include "library/ite.h" -#include "library/if_then_else_decls.cpp" -#include "library/kernel_bindings.h" - -namespace lean { -// ======================================= -// If-then-else builtin operator -static name g_ite_name("ite"); -static format g_ite_fmt(g_ite_name); -/** - \brief Semantic attachment for if-then-else operator with type - Pi (A : Type), Bool -> A -> A -> A -*/ -class ite_fn_value : public value { - expr m_type; - static expr mk_type() { - expr A = Const("A"); - // Pi (A: Type), bool -> A -> A -> A - return Pi({A, TypeU}, Bool >> (A >> (A >> A))); - } -public: - ite_fn_value():m_type(mk_type()) {} - virtual ~ite_fn_value() {} - virtual expr get_type() const { return m_type; } - virtual name get_name() const { return g_ite_name; } - virtual optional normalize(unsigned num_args, expr const * args) const { - if (num_args == 5 && is_bool_value(args[2]) && is_value(args[3]) && is_value(args[4])) { - if (to_bool(args[2])) - return some_expr(args[3]); // if A true a b --> a - else - return some_expr(args[4]); // if A false a b --> b - } else { - return none_expr(); - } - } - virtual void write(serializer & s) const { s << "ite"; } -}; -MK_BUILTIN(ite_fn, ite_fn_value); -MK_IS_BUILTIN(is_ite_fn, mk_ite_fn()); -static register_builtin_fn ite_blt("ite", []() { return mk_ite_fn(); }); -static value::register_deserializer_fn ite_ds("ite", [](deserializer & ) { return mk_ite_fn(); }); -// ======================================= - -void import_ite(environment const & env, io_state const & ios) { - env->import("if_then_else", ios); -} - -static int expr_mk_ite(lua_State * L) { - return push_expr(L, mk_ite(to_expr(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr(L, 4))); -} - -void open_ite(lua_State * L) { - SET_GLOBAL_FUN(expr_mk_ite, "mk_ite"); -} -} diff --git a/src/library/ite.h b/src/library/ite.h deleted file mode 100644 index 9238a97e5..000000000 --- a/src/library/ite.h +++ /dev/null @@ -1,18 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/io_state.h" -#include "library/if_then_else_decls.h" - -namespace lean { -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)); } -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); } -void import_ite(environment const & env, io_state const & ios); -void open_ite(lua_State * L); -} diff --git a/src/library/register_module.h b/src/library/register_module.h index 4377b6a52..65a7cf425 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "library/fo_unify.h" #include "library/hop_match.h" #include "library/placeholder.h" -#include "library/ite.h" namespace lean { inline void open_core_module(lua_State * L) { @@ -20,7 +19,6 @@ inline void open_core_module(lua_State * L) { open_fo_unify(L); open_placeholder(L); open_hop_match(L); - open_ite(L); } inline void register_core_module() { script_state::register_module(open_core_module); diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 552f26137..a0ed03709 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/occurs.h" #include "library/expr_pair.h" -#include "library/ite.h" #include "library/kernel_bindings.h" #include "library/equality.h" @@ -33,10 +32,6 @@ class to_ceqs_fn { return list(mk_pair(e, H)); } - bool imported_ite() { - return m_env->imported("if_then_else"); - } - expr lift_free_vars(expr const & e, unsigned d) { return ::lean::lift_free_vars(e, d, m_menv); } @@ -96,7 +91,7 @@ class to_ceqs_fn { return mk_pair(new_e, new_H); }); } - } else if (is_ite(e) && imported_ite()) { + } else if (is_ite(e)) { expr c = arg(e, 2); expr not_c = mk_not(c); expr c1 = lift_free_vars(c, 1); diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out index ad85e725c..cf0d53e10 100644 --- a/tests/lean/arith7.lean.expected.out +++ b/tests/lean/arith7.lean.expected.out @@ -1,13 +1,14 @@ Set: pp::colors Set: pp::unicode Imported 'Int' -2 +eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥) 3 Defined: x -2 -⊤ +eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥) +eps (nonempty_intro -2) (λ r : ℤ, ((⊥ → r = -2) → (⊤ → r = 2) → ⊥) → ⊥) ≤ 0 → ⊥ Assumed: y -if 0 ≤ -3 + y then -3 + y else -1 * (-3 + y) +eps (nonempty_intro (-3 + y)) + (λ r : ℤ, ((0 ≤ -3 + y → r = -3 + y) → ((0 ≤ -3 + y → ⊥) → r = -1 * (-3 + y)) → ⊥) → ⊥) | x + y | > x Set: lean::pp::notation Int::gt (Int::abs (Int::add x y)) x diff --git a/tests/lean/simp3.lean b/tests/lean/simp3.lean index 991e48587..6d350997a 100644 --- a/tests/lean/simp3.lean +++ b/tests/lean/simp3.lean @@ -19,29 +19,22 @@ show(simplify(t1, 'default', opt)) *) set_opaque Nat::ge false -add_rewrite Nat::add_assoc -add_rewrite Nat::distributer -add_rewrite Nat::distributel +rewrite_set basic +add_rewrite Nat::add_assoc Nat::distributer Nat::distributel : basic (* local opt = options({"simplifier", "unfold"}, true, {"simplifier", "eval"}, false) local t1 = parse_lean("2 * double (double 2) + 1 ≥ 3") -show(simplify(t1, 'default', opt)) +show(simplify(t1, "basic", opt)) *) variables a b c d : Nat -import if_then_else -add_rewrite if_true -add_rewrite if_false -add_rewrite if_a_a -add_rewrite Nat::add_zeror -add_rewrite Nat::add_zerol -add_rewrite eq_id +add_rewrite if_true if_false if_a_a Nat::add_zeror Nat::add_zerol eq_id : basic (* local t1 = parse_lean("(a + b) * (c + d)") -local r, pr = simplify(t1) +local r, pr = simplify(t1, "basic") print(r) print(pr) *) @@ -63,7 +56,7 @@ add_rewrite congr2_congr1 congr2_congr2 congr1_congr2 : proofsimp (* local t2 = parse_lean("(if a > 0 then b else b + 0) + 10 = (if a > 0 then b else b) + 10") -local r, pr = simplify(t2) +local r, pr = simplify(t2, "basic") print(r) print(pr) show(simplify(pr, 'proofsimp')) @@ -72,7 +65,7 @@ show(simplify(pr, 'proofsimp')) (* local t1 = parse_lean("(a + b) * (a + b)") -local t2 = simplify(t1) +local t2 = simplify(t1, "basic") print(t2) *) @@ -81,20 +74,20 @@ print(t2) (* local t1 = parse_lean("true → false") -print(simplify(t1)) +print(simplify(t1, "basic")) *) (* local t1 = parse_lean("true → true") -print(simplify(t1)) +print(simplify(t1, "basic")) *) (* local t1 = parse_lean("false → false") -print(simplify(t1)) +print(simplify(t1, "basic")) *) (* local t1 = parse_lean("true ↔ false") -print(simplify(t1)) +print(simplify(t1, "basic")) *) \ No newline at end of file diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out index 2407e2647..e6e2c7f99 100644 --- a/tests/lean/simp3.lean.expected.out +++ b/tests/lean/simp3.lean.expected.out @@ -11,7 +11,6 @@ Assumed: b Assumed: c Assumed: d - Imported 'if_then_else' a * c + (a * d + (b * c + b * d)) trans (Nat::distributel a b (c + d)) (trans (congr (congr2 Nat::add (Nat::distributer a c d)) (Nat::distributer b c d)) diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean index 86eb58545..6a80d242d 100644 --- a/tests/lean/tst1.lean +++ b/tests/lean/tst1.lean @@ -1,4 +1,3 @@ -import if_then_else -- Define a "fake" type to simulate the natural numbers. This is just a test. variable N : Type variable lt : N -> N -> Bool diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out index d4c2c961a..8613cfa3a 100644 --- a/tests/lean/tst1.lean.expected.out +++ b/tests/lean/tst1.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode - Imported 'if_then_else' Assumed: N Assumed: lt Assumed: zero @@ -26,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 -if two = two then ⊤ else ⊥ +eps (nonempty_intro ⊤) (λ r : Bool, ((two = two → r = ⊤) → ((two = two → ⊥) → r = ⊥) → ⊥) → ⊥) update (const three ⊥) two ⊤ : vector Bool three -------- @@ -46,4 +45,5 @@ 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), if j = i then d else v j H +λ (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) → ⊥) → ⊥) diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean index 8b925381b..29150b07c 100644 --- a/tests/lean/tst3.lean +++ b/tests/lean/tst3.lean @@ -1,4 +1,3 @@ -import if_then_else set_option verbose false. notation 10 if _ then _ : implies. print environment 1. diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out index 19e2c027e..4d4dd407f 100644 --- a/tests/lean/tst3.lean.expected.out +++ b/tests/lean/tst3.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode - Imported 'if_then_else' Notation has been redefined, the existing notation: notation 45 if _ then _ else _ has been replaced with: diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua index 7fd69fb1b..16fd6756d 100644 --- a/tests/lua/ceq1.lua +++ b/tests/lua/ceq1.lua @@ -22,7 +22,6 @@ function test_ceq(name, expected, is_perm) end parse_lean_cmds([[ - import if_then_else variable f : Nat -> Nat axiom Ax1 : forall x : Nat, x > 0 -> f x < 0 /\ not (f x = 1) axiom Ax2 : forall x : Nat, x < 0 -> f (f x) = x