From 4dc98bc73be6772a9856a90cb90a86f82bd997fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Jan 2014 02:05:09 -0800 Subject: [PATCH] refactor(builtin/kernel): use iff instead of = for Booleans Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 141 +++++++++++++------------- src/builtin/obj/kernel.olean | Bin 25736 -> 25543 bytes src/emacs/lean-mode.el | 2 +- src/kernel/kernel_decls.cpp | 1 + src/kernel/kernel_decls.h | 4 + src/library/CMakeLists.txt | 2 +- src/library/elaborator/elaborator.cpp | 8 +- src/library/eq_heq.cpp | 22 ---- src/library/equality.cpp | 44 ++++++++ src/library/{eq_heq.h => equality.h} | 5 +- src/library/fo_unify.cpp | 8 +- src/library/hop_match.cpp | 9 +- src/library/simplifier/ceq.cpp | 26 ++--- 13 files changed, 154 insertions(+), 118 deletions(-) delete mode 100644 src/library/eq_heq.cpp create mode 100644 src/library/equality.cpp rename src/library/{eq_heq.h => equality.h} (62%) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 9cf372845..8fb67f3c1 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -21,12 +21,17 @@ infixr 30 ∨ : or definition and (a b : Bool) := ¬ (a → ¬ b) -definition implies (a b : Bool) := a → b - infixr 35 && : and infixr 35 /\ : and infixr 35 ∧ : and +definition implies (a b : Bool) := a → b + +definition iff (a b : Bool) := a == b + +infixr 25 <-> : iff +infixr 25 ⟷ : iff + -- 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 @@ -98,8 +103,8 @@ theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c := assume Ha, H2 (H1 ◂ Ha) -theorem not_not_eq (a : Bool) : (¬ ¬ a) = a -:= case (λ x, (¬ ¬ x) = x) trivial trivial a +theorem not_not_eq (a : Bool) : ¬ ¬ a ⟷ a +:= case (λ x, ¬ ¬ x ⟷ x) trivial trivial a theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a := (not_not_eq a) ◂ H @@ -223,14 +228,14 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false := boolext (assume H1 : a, absurd H1 H) (assume H2 : false, false_elim a H2) -theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : (a = b) = false +theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ⟷ false := eqf_intro H -theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a) +theorem or_comm (a b : Bool) : a ∨ b ⟷ b ∨ a := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a)) (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b)) -theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) = (a ∨ (b ∨ c)) +theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ⟷ a ∨ (b ∨ c) := boolext (assume H : (a ∨ b) ∨ c, or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c)) (λ Hb : b, or_intror a (or_introl Hb c))) @@ -240,120 +245,120 @@ theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) = (a ∨ (b ∨ c)) (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c) (λ Hc : c, or_intror (a ∨ b) Hc))) -theorem or_id (a : Bool) : (a ∨ a) = a +theorem or_id (a : Bool) : a ∨ a ⟷ a := boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2)) (assume H, or_introl H a) -theorem or_falsel (a : Bool) : (a ∨ false) = a +theorem or_falsel (a : Bool) : a ∨ false ⟷ a := boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2)) (assume H, or_introl H false) -theorem or_falser (a : Bool) : (false ∨ a) = a +theorem or_falser (a : Bool) : false ∨ a ⟷ a := (or_comm false a) ⋈ (or_falsel a) -theorem or_truel (a : Bool) : (true ∨ a) = true +theorem or_truel (a : Bool) : true ∨ a ⟷ true := eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a) -theorem or_truer (a : Bool) : (a ∨ true) = true +theorem or_truer (a : Bool) : a ∨ true ⟷ true := (or_comm a true) ⋈ (or_truel a) -theorem or_tauto (a : Bool) : (a ∨ ¬ a) = true +theorem or_tauto (a : Bool) : a ∨ ¬ a ⟷ true := eqt_intro (em a) -theorem and_comm (a b : Bool) : (a ∧ b) = (b ∧ a) +theorem and_comm (a b : Bool) : a ∧ b ⟷ b ∧ a := boolext (assume H, and_intro (and_elimr H) (and_eliml H)) (assume H, and_intro (and_elimr H) (and_eliml H)) -theorem and_id (a : Bool) : (a ∧ a) = a +theorem and_id (a : Bool) : a ∧ a ⟷ a := boolext (assume H, and_eliml H) (assume H, and_intro H H) -theorem and_assoc (a b c : Bool) : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c)) +theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ⟷ a ∧ (b ∧ c) := boolext (assume H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H))) (assume H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H))) -theorem and_truer (a : Bool) : (a ∧ true) = a +theorem and_truer (a : Bool) : a ∧ true ⟷ a := boolext (assume H : a ∧ true, and_eliml H) (assume H : a, and_intro H trivial) -theorem and_truel (a : Bool) : (true ∧ a) = a +theorem and_truel (a : Bool) : true ∧ a ⟷ a := trans (and_comm true a) (and_truer a) -theorem and_falsel (a : Bool) : (a ∧ false) = false +theorem and_falsel (a : Bool) : a ∧ false ⟷ false := boolext (assume H, and_elimr H) (assume H, false_elim (a ∧ false) H) -theorem and_falser (a : Bool) : (false ∧ a) = false +theorem and_falser (a : Bool) : false ∧ a ⟷ false := (and_comm false a) ⋈ (and_falsel a) -theorem and_absurd (a : Bool) : (a ∧ ¬ a) = false +theorem and_absurd (a : Bool) : a ∧ ¬ a ⟷ false := boolext (assume H, absurd (and_eliml H) (and_elimr H)) (assume H, false_elim (a ∧ ¬ a) H) -theorem imp_truer (a : Bool) : (a → true) = true -:= case (λ x, (x → true) = true) trivial trivial a +theorem imp_truer (a : Bool) : (a → true) ⟷ true +:= case (λ x, (x → true) ⟷ true) trivial trivial a -theorem imp_truel (a : Bool) : (true → a) = a -:= case (λ x, (true → x) = x) trivial trivial a +theorem imp_truel (a : Bool) : (true → a) ⟷ a +:= case (λ x, (true → x) ⟷ x) trivial trivial a -theorem imp_falser (a : Bool) : (a → false) = ¬ a +theorem imp_falser (a : Bool) : (a → false) ⟷ ¬ a := refl _ -theorem imp_falsel (a : Bool) : (false → a) = true -:= case (λ x, (false → x) = true) trivial trivial a +theorem imp_falsel (a : Bool) : (false → a) ⟷ true +:= case (λ x, (false → x) ⟷ true) trivial trivial a -theorem not_and (a b : Bool) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b) -:= case (λ x, (¬ (x ∧ b)) = (¬ x ∨ ¬ b)) - (case (λ y, (¬ (true ∧ y)) = (¬ true ∨ ¬ y)) trivial trivial b) - (case (λ y, (¬ (false ∧ y)) = (¬ false ∨ ¬ y)) trivial trivial b) +theorem not_and (a b : Bool) : ¬ (a ∧ b) ⟷ ¬ a ∨ ¬ b +:= case (λ x, ¬ (x ∧ b) ⟷ ¬ x ∨ ¬ b) + (case (λ y, ¬ (true ∧ y) ⟷ ¬ true ∨ ¬ y) trivial trivial b) + (case (λ y, ¬ (false ∧ y) ⟷ ¬ false ∨ ¬ y) trivial trivial b) a theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b := (not_and a b) ◂ H -theorem not_or (a b : Bool) : (¬ (a ∨ b)) = (¬ a ∧ ¬ b) -:= case (λ x, (¬ (x ∨ b)) = (¬ x ∧ ¬ b)) - (case (λ y, (¬ (true ∨ y)) = (¬ true ∧ ¬ y)) trivial trivial b) - (case (λ y, (¬ (false ∨ y)) = (¬ false ∧ ¬ y)) trivial trivial b) +theorem not_or (a b : Bool) : ¬ (a ∨ b) ⟷ ¬ a ∧ ¬ b +:= case (λ x, ¬ (x ∨ b) ⟷ ¬ x ∧ ¬ b) + (case (λ y, ¬ (true ∨ y) ⟷ ¬ true ∧ ¬ y) trivial trivial b) + (case (λ y, ¬ (false ∨ y) ⟷ ¬ false ∧ ¬ y) trivial trivial b) a theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b := (not_or a b) ◂ H -theorem not_iff (a b : Bool) : (¬ (a = b)) = ((¬ a) = b) -:= case (λ x, (¬ (x = b)) = ((¬ x) = b)) - (case (λ y, (¬ (true = y)) = ((¬ true) = y)) trivial trivial b) - (case (λ y, (¬ (false = y)) = ((¬ false) = y)) trivial trivial b) +theorem not_iff (a b : Bool) : ¬ (a ⟷ b) ⟷ (¬ a ⟷ b) +:= case (λ x, ¬ (x ⟷ b) ⟷ ((¬ x) ⟷ b)) + (case (λ y, ¬ (true ⟷ y) ⟷ ((¬ true) ⟷ y)) trivial trivial b) + (case (λ y, ¬ (false ⟷ y) ⟷ ((¬ false) ⟷ y)) trivial trivial b) a -theorem not_iff_elim {a b : Bool} (H : ¬ (a = b)) : (¬ a) = b +theorem not_iff_elim {a b : Bool} (H : ¬ (a ⟷ b)) : (¬ a) ⟷ b := (not_iff a b) ◂ H -theorem not_implies (a b : Bool) : (¬ (a → b)) = (a ∧ ¬ b) -:= case (λ x, (¬ (x → b)) = (x ∧ ¬ b)) - (case (λ y, (¬ (true → y)) = (true ∧ ¬ y)) trivial trivial b) - (case (λ y, (¬ (false → y)) = (false ∧ ¬ y)) trivial trivial b) +theorem not_implies (a b : Bool) : ¬ (a → b) ⟷ a ∧ ¬ b +:= case (λ x, ¬ (x → b) ⟷ x ∧ ¬ b) + (case (λ y, ¬ (true → y) ⟷ true ∧ ¬ y) trivial trivial b) + (case (λ y, ¬ (false → y) ⟷ false ∧ ¬ y) trivial trivial b) a theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b := (not_implies a b) ◂ H -theorem not_congr {a b : Bool} (H : a = b) : (¬ a) = (¬ b) +theorem not_congr {a b : Bool} (H : a ⟷ b) : ¬ a ⟷ ¬ b := congr2 not H -theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x = Q x) : (∃ x : A, P x) = (∃ x : A, Q x) +theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x ⟷ Q x) : (∃ x : A, P x) ⟷ (∃ x : A, Q x) := congr2 (Exists A) (funext H) -theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) = (∃ x : A, ¬ P x) -:= 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 (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ⟷ (∃ x : A, ¬ P x) +:= calc (¬ ∀ x : A, P x) = ¬ ∀ x : A, ¬ ¬ P x : not_congr (allext (λ x : A, symm (not_not_eq (P x)))) + ... = ∃ x : A, ¬ P x : refl (∃ x : A, ¬ P x) theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x := (not_forall A P) ◂ H -theorem not_exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) = (∀ x : A, ¬ P x) -:= calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x) - ... = (∀ x : A, ¬ P x) : not_not_eq (∀ x : A, ¬ P x) +theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ x : A, P x) ⟷ (∀ x : A, ¬ P x) +:= calc (¬ ∃ x : A, P x) = ¬ ¬ ∀ x : A, ¬ P x : refl (¬ ∃ x : A, P x) + ... = ∀ x : A, ¬ P x : not_not_eq (∀ x : A, ¬ P x) theorem not_exists_elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x := (not_exists A P) ◂ H @@ -373,7 +378,7 @@ theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x (λ (w : A) (Hw : w ≠ a ∧ P w), exists_intro w (and_elimr Hw))) -theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x)) +theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) ⟷ (P a ∨ (∃ x : A, x ≠ a ∧ P x)) := boolext (assume H : (∃ x : A, P x), exists_unfold1 a H) (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H) @@ -385,10 +390,10 @@ theorem left_comm {A : TypeU} {R : A -> A -> A} (comm : ∀ x y, R x y = R y x) ... = R (R y x) z : { comm x y } ... = R y (R x z) : assoc y x z -theorem and_left_comm (a b c : Bool) : (a ∧ (b ∧ c)) = (b ∧ (a ∧ c)) +theorem and_left_comm (a b c : Bool) : a ∧ (b ∧ c) ⟷ b ∧ (a ∧ c) := left_comm and_comm and_assoc a b c -theorem or_left_comm (a b c : Bool) : (a ∨ (b ∨ c)) = (b ∨ (a ∨ c)) +theorem or_left_comm (a b c : Bool) : a ∨ (b ∨ c) ⟷ b ∨ (a ∨ c) := left_comm or_comm or_assoc a b c -- Congruence theorems for contextual simplification @@ -458,24 +463,24 @@ theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) := imp_congrr (λ H, H_ac) H_bd -- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b -theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d) +theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ⟷ c ∨ d := imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd -theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : (a ∨ b) = (c ∨ d) +theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : a ∨ b ⟷ c ∨ d := imp_congrl (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) H_bd -- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true -theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d) +theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : a ∨ b ⟷ c ∨ d := or_congrr (λ H, H_ac) H_bd -- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b) -theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a ∧ b) = (c ∧ d) +theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ⟷ c ∧ d := congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c))) -theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : (a ∧ b) = (c ∧ d) +theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : a ∧ b ⟷ c ∧ d := congr2 not (imp_congrl (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)) (λ H_a : a, congr2 not (H_bd H_a))) -- (Common case) simplify a to c, and then b to d using the fact that c is true -theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a ∧ b) = (c ∧ d) +theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ⟷ c ∧ d := and_congrr (λ H, H_ac) H_bd -theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x) +theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ⟷ p ∨ ∀ x, φ x := boolext (assume H : (∀ x, p ∨ φ x), or_elim (em p) @@ -488,19 +493,19 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, (λ H1 : p, or_introl H1 (φ x)) (λ H2 : (∀ x, φ x), or_intror p (H2 x))) -theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p) +theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ⟷ (∀ x, φ x) ∨ p := calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x) : allext (λ x, or_comm (φ x) p) ... = (p ∨ ∀ x, φ x) : forall_or_distributer p φ ... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x) -theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) = ((∀ x, φ x) ∧ (∀ x, ψ x)) +theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ⟷ (∀ x, φ x) ∧ (∀ x, ψ x) := boolext (assume H : (∀ x, φ x ∧ ψ x), and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x))) (assume H : (∀ x, φ x) ∧ (∀ x, ψ x), take x, and_intro (and_eliml H x) (and_elimr H x)) -theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) = (p ∧ ∃ x, φ x) +theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ⟷ p ∧ ∃ x, φ x := boolext (assume H : (∃ x, p ∧ φ x), obtain (w : A) (Hw : p ∧ φ w), from H, @@ -509,12 +514,12 @@ theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x obtain (w : A) (Hw : φ w), from (and_elimr H), exists_intro w (and_intro (and_eliml H) Hw)) -theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) = ((∃ x, φ x) ∧ p) +theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ⟷ (∃ x, φ x) ∧ p := calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p) ... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ ... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x) -theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) = ((∃ x, φ x) ∨ (∃ x, ψ x)) +theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ⟷ (∃ x, φ x) ∨ (∃ x, ψ x) := boolext (assume H : (∃ x, φ x ∨ ψ x), obtain (w : A) (Hw : φ w ∨ ψ w), from H, diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 03585d4451006f7381f645563589c46a60c24ae3..a9ec67ca9a94c4a2fe6081ebc62e7fd97a11ccf5 100644 GIT binary patch literal 25543 zcmb_l33#1Vng0L(-v1_ut=Q2iE>o%{g;Jd^C@s)70Tt6Sbt!E{A2gG+H*FwI+B7X7 zo62I5MNpB=K@i+VM;&oMK~X?)9ClDdWKlo`DWlG!2#WK)?|Zg;bCb3{)92yz`_K8# zx1aB2d(?sdVf}|Jbq(+mEk)&?AC^|!sa0(TPu3ALUh?&miS8r z+Q_RYL^ONL@M!Po!0-@o^5Uj1;_qzV0%cV!het>fH6&7FxjVnhq7Q#(B?!*|v^ymO zG^vsFi6>?itDQ#DFKFU>)EqUU-;~CFk8b;1(nc+Nht>iydtqr@@uv)ONCrrQKa)^Q zZlpJJCdtj994~H?W6n`(M8Bzx{T|)+*`$qf3~bmqI8fgVq`pIk6itf|Mq<-AM=F!dOv_mp>sTlaS;6p}>qJibB(Qz+= zG~RS?!sF18P0}YzNhcngNFNw`c|F@|E*glZu-k_iq`oh}HiEMN66+O9H*Ca5Hq-vg z^G3}VGgjwQiJ1zD!FV;B4lZM31Er zG8aT_L%J(q$;qgGMb$rf6JojN_|Mb=Qw?GKpuZyBl|*TDTy6GfI{G+G4pTa61i z(40{#)@3z7OHs^?EKKC?fZNGIvkE9P2vUkkUWzwbeUPGeaBz$i=y*h}cta3}Ml^9E z3sQWCxkb`ZM}TZ<^Yq?h zHBzcR+G}(|3>^ww*iSiaWsJquUPfAv&eOo}Lk}gJHSA3O%;qci;W&lQ%;BtmH$fD1 z@m4@K%;kx>dlMfq?%HQ~i4j_bL>?U(*gDWVNTfx31 zXmZ44^k`=n+FX`88nx2u7=V+dCcqGY>+QptZjwu75 zhN2C;xuEH(4-OfT`22wj_p6nAS&PO4FfF^w+LU)4}t?xx4)+a>p#0WAr&!LznqxKw22964&i=h$n&GCle2Rg*8 zZ`x%^o6OHxBa_cihz~^3PL1Gc5j-8B1U>`c)lp!Y^+Ht20)QIjf4|ju`Azm+v-H)V z_gPALCP10>LlHbHf@cGSXd2IBtQtk-_@=xxMaY5MjDQyvITioeO2qqE5k8GR;=))9 z07`cr;4zycF@ong#DE=rw>HIN(w@HU60h87wt#UsMjHX%QBUYo- zv_V@2pfn{WRP7leS_zKobyBmBvkO7`S>jy8UaY+s;N%bzogEyv%uHH3Fs+9Kbb(>J zw7q87CavC$!&+NE?ALg4oo_@zJloTNp+16>l`BBSuS@_j=7J+HwHn7mnSV^e5HT%( z*q;W7hGk$VA76oXY5l1PUddiGz*PXZYog-pmCfxy)gvgFmm8(K+^Xdi1Omsj1p?N6 z$^s4k8S3qGTP{%B6NSY33_ywX*$93P;4_j1&NuAciuJu)>pk`3HjZR@)Nng&Du&x7 zu9-mJlv&>Y0!Vbq=9dFb#+Ku?z_nS>lUdqeQFycSs)4RWxE0C^Et|8%y5&EngM06uX2Y~ z0}ki^PKOdQV!nb-`lTV{D}c7lXBK^Sp^iDPx$w5U%Mkqf!FKXn($z5>=Z&-gl-f}! zntuvVrg_kye699`AZI8jE&_617MVr5ir&}~SB08ls669EEz}qx;`X<{0x0F504U|2 z1gIhTYlHHW*zGBRCr6Vg3?nK{G7w}@)Dekxk)M66{lfb3)Z;A;N4t-nwJq7o{es6^ zL-n4W@i-YDKygrrU94=5fd2%NHu=8+C?ot9pp1YJ%+K?2nQzp<)L{G>(6p3bkdk=t z@zd7keQa9>lYbXIZT<6;%;)pvb1K#BSyncC_J1Ijl=@$QQtI~rrPLn)%ClIrIM4nO z;AO2mt0b0q7Hs8N1-pG_ZAd)%#{ouxWN+{8|F$-|8@p9ANU{sumFTC^&Cw6$C!_de zX=U~t3fX|OsBG|O)XD}->axLKtTO)!y5(r!$>@$Y7%#e?HDW>C`X<|k+1e!J&oB#K z1f~=!F90%!<`sY!F_~Woa1n}0(ZrFlHly%CpI7ZejBQ)AZUpPp;MqfgnViAl+!TLS`x&JZDZ2wz zbNs2LCPGF%H6&k`)HoE`q+@i&8f%3{kM0I~421jz0FPiTw}vYTz7Vym3DTUM1Tk0T zcWDY+ZCV@$tZabPqrVk|Ww9QO`9mG}Yfi+`S#TV)OT(m)VeAR3g$;;&KZmO4wrm90WXR#?_JIpz<6i{y(b z6!W0cmI6cq2UYS%sOl@wRTg?BKw0ST04idp0aV271yB()9UwDh{wjm=zmV9g4JJF#!e!$R5QWV5sm#JSr%uJ0rL;(qrX+pxdvKT?3C9gL*XAV?%p^&&V1(yo4>jE@QXYE3On(q!Ys5qRp z2LW6zPS|E38jBSKws+vKM?5=C1DHed2ibKAngPs;p8fHSzV_0wA?9nZP3 zOB%Bxx}QS(lb5{92)L66T&C#CQo=Qy{@LLl{@{4F54Unoe$*vuF>(2_>liEc&(t}45GM*$UEMUo(jW7#Fxw|K9i z_NAyFMmO?h)C_{ct24Vm44Z`NIAb2yx&{QbA5zS@*F85g1p+MsCh>(D9B2B+K~mc7)Y9E?Ah4bMM^N=+U4kDy=z4W5%&?I8wSvzHJn4oPV5S;i!54drmSh^!0_`FSLVg;IVJDkSY1fXYd0 z0dh@~*8ytniJ-N<1^xnK*E<9U5{XZfcED)Yw+;I#D8ruRpH z#dVPhBL|%Fr9h5M=)B?vR8kP;ugHQoHN}l+Rtpia$u=YPZr(h+CS=_-G1DEHGgq*b z;~l=q(e4P0X1)o8Wx0_EGJ{4V7I)UrMrF1eV8@}dXK|-gjif29OdI=P?k(;EiC}=@ zzGx&Sl1`yB3v#|%7KsYM_g922L-fl+bUC7-_=(A-kl{2$`xZYzN1k5^ozxgS@R&>% z-61)FQ{3XUyerBI{qm(vvZ@cYhJq4M62OI&pm@k2tUnZG`O-$3_QVP8?)jKO5<7%N zs@09rGE`lrU@TF$U=PlLQcwX!9MCM_M!j6Xv3~Ldg|w$d4m6Ys2Fxkwn1sf&B;+mi zY}AU;5(|*Xk7nVJGbUsCgm~n_cMm2LA5OOlR|0%h>&fW1OqPsYr zg-{wzRp*g3gZzAgGp*#z%PYQ$z547%eLho%#n<9PNzqLiH?c<94`7>S5{|k!-!KWH zxiT9ZDsup<6LMN5_9w(qQsK@{sPbm}uHYdf>ML)K z(jwbc4vV@mqcR)Pruoa!LE6Mlk|}yaoj_@Ms7!l$zTJU@YYpFSA<-yDh4 zC{0XO3d<|exjA*Lx4MetQW|6O)R}pkk_U5E48I8`jA(>*@Y2%t(*P4Aa3zG*HR>yy zf}a%}?C4FDxwUnSSDHdN-U<^;6qHBUU?zD!53tz`*w|Gh8JJa$0g`&k2v?yZ8lm|? zDJ9fw9*wX7UBvVY023o{77a!?6-LkwgA1f23*j`~MQ(^k_l&})jMhd{M;K{9)W-y(r_M0cz%Q+Pel>`+qW*C-w4mPF!9d;( z#R5{j7N8d7+%};yTj14i9kW2W0)^E62EbN=aTqrVhL=tFg^JfQ?hX_Rm@YG{uib-` zDfp&OB=0xzt!(=(g2-Trxtpj|X0w7+7*>-#{_*JNw<3XSWxeo2g+?^HCYtPk$O+9v zI3k*ffInB0&L)1VtL1q#jN9Q>u8OK~b{a%2gEe!k`N?b>*AN zSJwkMo%H?on>zxx|2Ai(KXCFFKyCvU2)kYHR8UNObql^F+V=^1v$@qC^@;C7i|bfH zDzw#(eD%_RU-=T~HyhZq8^_fzjNQN1sypg}e{7B0e3z;%kNK$^n3eAba#`Y@+t4N( z+#bO@*rCZi+y+-3l6$@fA<5OB8Dws41DmZ@Nlz++Apwn0FKO zwrk<4NPr1YFYm~J4$z&gCBPPDk6ks%hHp8L^mcBTg`RG<3Evg^vY8Te3ckcC-wvGl zWS}Q!Y6Z?C0$J(Dv=YbK{RUQ^Or04!hql=ksQBwH2f}z?CDKrGpkN~%-_c-1~`~kp_Mm185d~ozQ-?YI?>z(&000AqP3p{PL<%V0qRERDS)$B3v*Nt zl(scg(^4c&%TV#^8_)v$>Om+LVcu~}_c1WTBGkQ>d^bT92|hlLSB z?8k3rfM)y1XL?)wgmh zoCFN<*Z@;Q5cZt4A6|<)gyvL2xz^DB3oQLWHZPc8OAv@EcL2y#ZoWY z!4I%zW4KAKx;z@ejtXT2y*Xhd%I$vuBbnkEfO7jEQMtT%ysbuUUE}SyKu&@?`0V#q zos75SC%otoLppU?6ch%l9tq42dg@OACElL_HhXGQ^f{&NAlYa#wbPm%-g>QWmZMzW zdYioWk({b)D9v9W0;MSc$ymIouWm|>74>0eI}yE3klmhRM^-a9g593C2A>a<47LpQ z4-c+wcqH{U_O^7O^yM#9s;5wGteo?EBXc{Fme=*%bZQ5BAAo{KyP8Pw*#+&2DnQ=9 z6!>=9)c`W23v{TS!e2M$uSYcxA~ev?!l&(NkHz0SE1pNFi$iN2SF@*6xgTY+=b`XU= zs9p*@oni3ok3&lCp*{2}F*@82@d9i3R{jYSn!PD%b`NcjIlg)difd?Qo-@kKudrHY z=2rsbik=6}zJsDcbgWP_%jRN7^m{(8*edCH^KseMgYIxq&OD zgN@wxDub#I)2TqMK1Pti{FIMlOXE(C(#ydCg!PId@@cV&%xFAu1l8Z{2tP3l@c)R2 z=fXtvpF`!-9ad`WC+MIY6KeHY`>H+zCAi>ect-~DWH${K3_`bpP!qm6Jhe^5ES~Ux zJn~P}^Fg_nA-l1K`-3zx6@%#+%^Gm>=Sc=tx@o$ps1AIah z<;x%NvlD~dOv*n@@d zh|HlX{sRbcUs5hiQFz)}azmD)SZB2yL^;LE>OyBNRcNwBK#4ENG%R^g?1CaOxunev z9|kHH@tf+AR2;GyY+EiwSn^s`RP_Vy{7Y7A%7y$Q8lL2LS6DQChyK*_2-_kUU*_#RGV;m#0;RCH~h+rOPSc38(3MiX#%O7Js zF$iLY0iEAVZgg&W7P&DR66XRH|Gvrpw_7nB<<=;oyx9(xQUm5?UQ-JeR^=8H-6*iR z?{WWfUrSS+i|(y*ITKBJZVU4!S^m@DaTIW(giO&Cri9VTzD7SL3S8OPQ7scB&htR7 z2gOIN$hv$|!C~asq!RXaEtb>G>%0!oi)%ajmX>@iGXX5Wb=_@*;a9O) zi35cOxdV@@|xzj_v^@^%)kt|10lBZP0JCeT>m>SHjr(m)E1Xm1<~7MDS#* zb!wav!S_Y*{b*0ac0cI>n>)8AVGHD&&=6!l(LRFg*w+4a;W|4BSG}=FUhy!vAVvOi zDs>tp(5O2-f@ehVgAv>Y)Yfq&1zBf+~-9C$}fK-xz#Bsw55dW`66sKC_STpa^7=VQp zf{?rP%O}7vX!$ISq|F#Xq+Ms`^CS3?2!7PS8sF6y7XX!Orc@(uP1+V?BHs(WWzxq0 z4#aH1Fk`l${`iNH%%qa|&&|dp3fJ=+(ZBujvY~MBG7WHaU!_b(1RAbSG4CdJ!|b6c4VN>{#g?oX&geTcBY9G zZH#Nhog4_+tiAC)&7Tx15T~GyTyzu5Z#(5gGV={o_*3}S`QMcQrTbL?XU(*N$G5cu z=sirBdZ*Lpw5c6{L6iLMWP3#1?zz$5U2v?%gAX@%*)QLJEF8%Ru0N|sx(Bo)NynxH^$rIU2(my)tW|E7<{~<@Pe&Nlcte|fzuudd@unB>5|kIx1uWqL zjbXz#&_cs^ZGku0SM007WSCoG=%9_{jpa+wwwl^8S@Z18KPIgm4Wm`Kw(JF>jSU4Ue<-7;rCn%{OpUFu zZPtatw<>y%322eJ(D;p5%BPAlc}i%7(G@ zRK}s1sZL^co_INQ>zHk2&f$QU2e`&i)ZPq)!~>_oKM@wK6R-UvVglvMn9$x z{gOTiQeBLehI`;+QBylB+LRYE6418z(g%}Reh0?6oQENnRjHQGOC zU^M3gFTaO0Z!oZS8;Tz^QmfqxEK&1jxgn^+%l_)(z($LN@1hIDrqtDgqZKivs@F$! zp33V-jq#VAdKb{;h%oE$A6X!j-;u}%$8uVAr`+@cR-rk}r{u!bNR|1q4J~(@T-3a} zIFZYH7XorhsbP5&^Iv#GkaZ>e4WpKDf)VLl$IeGR_OW^X){XW*!Empr^kFZ+GC}s< XTY$|e4jOQ8QS&zqtvw9?^N#-mxh|Eo literal 25736 zcmcIt3zS_|c|Padd+rS41Wi?1KqH13V#|OD&*-GeD>JfI2}xiH78xeV9WpwZNhT8r z0ePq(;iZ*_MG&x3A62ZV1rfw&QRL|ZDTt^bO4Qmaf{&o~|Gsa(?wLE2#I>5W*!j=i z|Nh_m-_IMyN1H=q!y}{3%>BtXjE$VyoLJw?isQ08w^}QT72}iHsY4T4aoG6yXx4#h zYgn;iWOQ<5EUQgUY-ncTYj|kXy02;uXT`CnuWcS@_>K;{b)c-VdCbT*ilM9!T{f2` z{!)Q9@+t}u&5jer2=66}Fz~5O3!gB%b zOvwOswUR#b%&ca$FC*#aRrsE`pBm9`c5A=KFZf8(MlFZNRsk`4era6srwnpP21tWH zT_|R;&&Zm!qa)4rsA$)(rAI~bo*oJ?my*A*BKdwNsu6T|t4jXiq>WNEH;$~ITyOR~ zG$XZ|fyV^%(vfl$%a?-a?gU>3a1XEDMto&m`eaE>JH%rh=>ubTuU1FHIf{6Sh*uDU z)JdX);9jWh>ST$cV z-Duq>w}Snpf#=p^)m3hfZ@xa^*ON`I&Wh%mV7-!}&j!^FS%x6B+6SOT$-tNb;{Y}d zZOn?5LpHSF1pH|AhfoD1*)Qio!+G7T!>ynw+;}RXbz9IF}$<{mJ}qu z*AimnIeM?(uwp%iuCtkE68)CONiT@lkPEWnyO)ASqt;Q`#}-5lx)Pf)tN6w@5l_yr|`CnP)d()M}b1{A{3N5jHIPjQP3?2MBTlp)g+!j57&&!hXcRQE zg&e_~0FwMdIBICc`VAASTFfIyAkgH9S?JNpF00s?U=yIUqW-fOqm1VefGZ8fnQoos zIUn@qgB9rQ23a>ir4T^!X5dZ}${wrHEI*Az@XY`>Q>M27?45^_;;~YLlpqaCh;p_H zdy4fktF@-!zB8FVSJBp|R3@j#-}^STg5l+`<_cSGtQ@zwusMmer!np_XE(5-nq34k&p1FEwJ6<49S z6om)^>H^h~HERbaCx*r_t2%WO@4>;|jesr;ZZk;e{iyFF>kRc%EX_DC#gUDKAYC za^Tyo+KY;uivMgS;(c5ucBG@Yd}V40%oo*tt>ADMrEqF#A=kE)@Wf5luC9&)vh6|mF1|OV)~!hg?@NX1TSMR z)-nWUg}CVJ=HOik1g#&I0SYPe-S**f_sVgbxrWw`YgPR{ztD@TaU+Vp*{%kRDILsG z!T=S&JORYO3*NlaY8(%x|0!8R#Iy!te;ObfmeHZ4d=1*=g!f1ATK1v=t^>G5v(-Al zSuexoQGiU&tt2;WUzOjjjFZkcfD0R>!%7P z+rT8j%E8Zol-4RA0Vusb8o_@9_>74x$8|*mZ?(!qY{~O_x9Rw>^>U(2G}n)hp4yz> z-punet{rBBjkE#uGy3-v0434CM-cfb-^G|K=WIbsSfJc!A3gxbR!v=@wGTg#=%O6E z0i+w`>`&ucB77!-{{c{$;%0$d*Cy6@DB39o;$m-|Pg$o#O3bX&M4_xhsiJix+ULMo zqTLq3+YQX;DivIh>Z}(9^Hmt8w^~hw{|rH**p<3>fS8zmA%b5tFrP~U{vNem;*TI` z%m4FM?f8#R$Vn~wD>lO(D%l`X8D;)2gSbTb3P9C6uLL!>nvDa63Uo1Z z`rJkBu$A1OJ+`7$Cb~wDg?~CC52Ih-7;vN9lPw-nn*cyFmyCb>KkP-7GbkY;nmM;NDzt1fCT!cF2ylUZXdAA|>MTBkV zH>68sGfBuiTsL%roTB-=0A-qo49bVJF$6h7K_Q=Mp8q>kSWoXyBG|6U?JsB1R=)%e z{S$K1gH|I?uRnbame7X+r`;J3WW}F-nLW6AOrn-}(&+~P_nn8b zi9&$^NbTII^hE~!Xrf{Jr~r3yu~Wzy-!n9CW4~;lK@kNm0&;#9nMJya-q=DhXg5tU zRG#somJ(wA2!)h?9H5j(;5g-e3{XSzNrUoD?Di9YXGD`I3?nK{G8|-4)Dekxk)M66 z{m}aH=;P>?1K7tex**xl{g7u|W6inzr@F7zJ>#>OM?+!OxNKg9(??iwRs=gzQN?*K~G!%e3SWnfqYJ-s-9(K)wBNt zv82@h0+eTe1yD-;8lVjDv_a0ZzX5o4JJ0shDv4*oR-UC(rFai2FSA0aiK5Eh-rX3_ zbT_uFW{_knxFgX|rAb*nrj5Y-3>4Q;*k=uNHux<-+2D5oWdqKwvcVs$GQW}Ckm|QH zx}y!Ii*Bq3gSyRiwij!=Rl35^oKSxRs2utyfLFk#8TTd&0d++iQ(Q(eTj+3st0k)wwMMQLdGPSjF_5cGex8ZowQ(J2#Hrv}d+ zMk4Vb4u_}svph_@NZH+}+Q%PVY9eGPQA0UgI2?*>(pkDq(YqNbIhyxy_&+7nid<;AsZ(3VSwzWAS{d3sL3Dc#$WqH932Q#L`t+c zObR)c3^^7H;cg+X*+&Q$nr}f{^EqeuWtB|}6ev3h=CeQf8J!e?p6QDqgFWXYEPLz% zY}w-l068%77XlP6S7s;CG=F848W{P10f8*N`p!6FOHHZsGO0@mSONU}r|9kjCWnx% zO1ITn8ZK=YGFsmCoASxzm_Gt8l8@;@uCY3$EehEsfrBdfqg3@J=qd|wrz#8mHEIymQ~Y5UbsfH)rM>yB5!Mm zykKVTu<7gkDH>u9#F15B9>F~UD(+qZP;tkI*~)GRp>4%oWC|T~&Ur5OKodGwqV8o@ z6{2oEHJ%!Fyzc=4J6Addf8*R#gRjqb1t0~b6nUd=HS#~U*hg(ppQ9#OHfpzEngCZQH*dS;X()IQRpZd zr3WghRtH2ZkS7YdPT`AqR8SJBO{Dc0MiObd2KKYlq1I?7@RyK#Gz!fZI^EKQgmGmt zfyku-G>>h**0RaPAqi@Y8W$1PJ0BOzb` zP|N0kd_j9BniG`f-1ABEzefj+x7Pxk!l3jv*i_;8sMT&Ycx{)sT->hY{pJ^1+j}sM#nEJ8nCS&k|cLz>`!Sfm17jF&jCwAQ}G2|9Pz3yhRC%{ix!dq zO=ng(l1jp{m$CL%@S`vtfUrXJ%8*~hAnZ@{wgzEySP)>;yPz5w9(JPubrWq*)_rV2 z1jbddhMTio*`pG=fy>d63l`?nTs~{#7{iLzT?kL-$6Dc{^EiMVJysN#19VvaD1)C@ zn|w?_8QtII$Nh4{j|=r_#5kZ58>HAtF-`zO4U#tkJfI>*r}1SDv|~iHKZ>FkMev-& z>I^a9n!SWraY#aY)G{SmYbb}qMW2)MOIk(FH-V)@J_(=_(;z@DZ1R%a1cUi=$9|9$f`aH z2kRpNB?0_M35rJy!g54|IbYmL)1Ez{UE5&jFR>K?)+yEMj%XRGE>kd|s9UfHr$i~J zs3Hz%7I33pGvJgzd6oh@xr_S9hSpNSsNrZ%;=`TKxS;rLRE;4M3y{c9Vc~46lRbqy z@yLY_B1|y8v`DT(rWdXgVk-}w1uzO%!zTj|f7h~#aO@a3Q@G+IGYZ$~#v+AF?upt8 zC%GhnmHFEMmXsk(u{A8*otVm*^0xYNiIa1_4i3YMzHOOBixjZaboUN`rRXou=BAGW zYD%g-z_`l(t8xE)H9lGJ)r+|UY`3K_{YTzn`%X})D!jYZi7B5-)t(O|^_04AM@3Y3 zXv1Xkuq-h&u(0TNI&KEY>#^F40UkKlio6MsI@p8T?VN0Md$${VqR?b>5kO^2c@HLI zisYqWZJrC9e6Eg{KLvc{O*gfCo;AIpx<3l)1IF1k%5G34c~6*(JDvna7dfDx*gvXiS0syFw4CCw=s%iNGOAp);WJ4 zcqbM-5#N~1@ptXSC}|feTt~G|2?@0V@9I>f8S)uLiro~Y*MdSdu{5o&CgGIn^cYEf zm0GSszc@O!HN`}8Fdb_Fd_71c=HPk>3w6}j#%PXU`HUUCu`;(zkKs#`3CG)GTT=^# zQWtQPP&WXq8f2r@)g&G`)>Z>aJ!OvTP!Y{heWeOj(&a!j#{p;&=MMo)%yACBgE`J2 zjYm<(Wmb}?W}#9c9nGamXUu8LB^;P*gwH0Yo0t4aMRiu^| zcRLZUK|{p~ctV9AtayFn<|By_%(oequkQH^7Z!AuB)g?qA+1d<5W4R;0+6SUi zT#NJ3S|HPc?Yj`LDQzs*=?9`)_vWRQnh>Rqee!p4%zXxTzft)CHf} z`nGzxt7W+PZUC6IuLg2i;tux8e9FTZzj1+7Wycv}D(BMG$8lwI?gy&pwIT zKgs*w0CGF;KVa3V_ubF^X3V-E^-K&-PD0AJ528up@fc*A7;lxFFYms6i#kOaa12Dk@Q z%P$6q%KCsPdArAh!R+N|K8oiCIUH(l8c?%DM-Bt5VRDj+Y4UdnmYIz8D413!R{}2IxX;j}twP#yp{y=1I=j?L5p49HvjZXWc z=trTs2GAnf`p*D)y;J~_c0~@5ab2LgzKK8M%wL6S<^c`i^YLk$?bGl#55VUWTEy|S zimW+Qhf&SJ5%0|F7f1P@j`9yftfGbv!$gQ0=ye4(fG+vNhy$KD)-Sd#tbRmZzZh(b zI~XJ68?S{$fbQuB8xGQZ3CZBqhpa<6JAy>H{nVEh&6iZ<(en+;14i{LOo*|jp5)Qu ziP{wEHeg}VRli)fuCFmz4^Hau1K8VRMQtA-(`Tu`R>fB-PDp>@_$RAx7eXzM;o5}| zl|l5RFCt>%sOYNfPhDxBW!A5L5R6zn4>S})oB=sNG+`=)(4l^lV#2^2%dYx)C=RlM zM_Y`W`~j$6zYdkrKa5+gsp&Z!?koUG{k*+VUIe(`N4;*cV$A5CpK@dV$?pz+CEYqV zb0LI{%m9PA{<$CueNev=Ty&(OX&DZdduR{6yo?U_`LWo^@Y?w&Ol|2K9yh}2f6Z~$ zyN(&5eiLoYlXltqC06T(>#hK~H{kiW@1U(zeUoAhfszbf4M!Lg)%BZ*L}{lYxmYV+ zWSF|#9&HX!`qO>QN2bQIuy?W>Zl?-}_cjW5>#WRV84TIc8ls}gR&+4!$?>O@sh~58 z?mkvTjHrm%V<%&HzC8@8KTM}$bya_iAm+3BPkb<2E_ZU2UJi~TtXve9Pl-)rMn%LC zq<*$7e4?@w%v}FX4@h4Y=s%0fr>H!aZwWdm^RbO2c?OtILkX8v*$F{h@OMkHn?_7R z3X-c5{M|3%U~^F={~tvDl$1h*0k)eVy8(t9k2EqBgXwwDN-)XFARE_zwIgXi5K4cF zCpOTiAjqX}u`jR$@?NHVC1%KiomH=;Ul~`*IlEY)i>uY>pk-jXCcsL?&PDzL`HOog zKXW+@lpjc;nIt7CXCr~!B9^Z-wDJX3Y*XZ245#*diu@MfS4GBwEjM1tWo0<+vVqS& z=7Loo7#JMFtBQd^_v79ztIh=mExXxm5x^df5=w|{P(0X)l1|^s#X-})`9N`S1)z*eiahP$5+0*AU*gjra|?=c zKTEVu6LrQIwjbA7QM?WX99LLoRLmlWsEYsaL)@#B`==-w^eeejOHr&+EeD3-&p;2I zwQ`|x7KU+56pck5S-Ut+OfG2=&M;7UFu#u^Xhkx39XEs}FNZ}{zgf>e3fzLzRoo1f z*h6LuVeRs@0Eb)UqCU11L(}mn(lJaqj<8B6J--hR-^@R8e^4ISgC-=oRAqc|;Tm5M zid?c3nZh(MDG`5V{KbMSz`?c*t{+Lm1Z{% z&`$$aa7HB@=@~4?D1}F3;CAo}{!8q3Y%6Omt$4*&+yu;F6j)KXq3yIyhKaS8NK4ZV z2Q(p9l`xzv5fxF;a(^&21kmXaKQth{9Kto<{rFrulNW#hL(XLUnLOvlQxyedp-G9% zS*}KNRL7aGyNjaB041r6n$z|eY5nPVSv)BzflxNdeWEbCu(v|<{;vE(N9ATXLQiivfEo0!L!ZMdoS5h7y8$%6zA}v2n+fJ! z93!&fLm-lBjjl5cOEjN?g3f85NYRX#VL;~(kQ<#_o=_rha3@6z~ z(8^ZaJHC1~0wqrBy(HbOYVyHn@og%ASaKS!j^IcH-yA{C65Z@JieBAtV|jZ67#%1$ z!FB@bkCoJyl~B56>UFmkhF{0FC8i}l8_<11FbjxJG0P53AV#1(E15L(FU`;ed_YnD zCv_V)JZBP&CkL*J;6w!1qg}JcB*2H{a|C8q-h&c8FYg5;^_9K0p!Po02K~nDV~Tz| z63ZZYGm1N@29F^Wnx|W>Q)5#E&xqieXisCeTYAu;Q(_m$e4G$uKh3Iw?0Q&fKNsGi z9T$l9Br)65Z8dIaBGu{YkpjV_Ie#=%oQ)PKc}@h+jo{lN_;v%!9@^#|1QEVz2>Rt2 zn3U)HFT}4LxU=HjzG)JTUAi43 zAaU^Qj8FehW)x@H$5dPI&_IBh6^D>JETjO#pye|(60SI%ZIOT-sC^+3E{V058raZj z>brr;)zh@L#lXn-KyR7!F@VDjlr$t9tZf1H$G-|?CY8j0s2Y&xX3s45Q4q$hW6+G8%%%=;xP&*67pqu3y^AX@Wk07@#5pj#>MoTP$ceS*J zJ){YbVJp9aX)LtnF}3rAhQIG=I`>7?eB55CTEPn9gT%i zM6BfX<9>AGRe*l!D49sQgE-c_zyRyrZ6!rgN8+64gYp_6^IvRj=gWAjyyL!{1Mbnc z4N9YN`EfMKg*O6}3qJvn6M0psfY#vzp))`EMV+^3f*P6PXpBb(PscAvEO98bg+C8+Lkj>F?SE*+rNQr zG-0{gKBzkhg^d!0D}N=V7qK|@bMGlyTVYWBELsx#IJS+bBNC~L2*3BUUOCdPMu^PJ z77(1$;thTi8X2hWe!A7*+nsgxGCBpvfQ@R&sUW4TsZ(P6t_0mWX6xyO+X2cATzn{g z??7$hhO_Onajv(@*?ZfkZs0;vaQDvWhk>5ypB4y$)DJd8MO<%XK7JIc!;oF_PrZv}W$dM#6eDkigaSohc+>dsd>j8jDWZwjsjG)ij zXX92MiJwg((c3{Ih}@K7AW=qc*z8Uhjg32K`BjGE{=FRai~6(+8(%~5)mCbaJAox?-YmBU zRrp4ren?=$q|*2TxpmEE)N=wFH)NuI2n@9R?nFK~ zmZRF;`_c" . 'font-lock-type-face) ("\\_<\\(calc\\|have\\|in\\|let\\|forall\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) - ("\\(->\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face) + ("\\(->\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-⟷]\\)" . 'font-lock-constant-face) ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face) ("\\_<\\(\\b.*_tac\\|Cond\\|OrElse\\|T\\(?:hen\\|ry\\)\\|When\\|apply\\|b\\(?:ack\\|eta\\)\\|done\\|exact\\)\\_>" . 'font-lock-constant-face) ("\\(universe\\|theorem\\|axiom\\|definition\\|variable\\|builtin\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face)) diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 846521706..74ed6351a 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -12,6 +12,7 @@ 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(iff_fn, name("iff")); MK_CONSTANT(exists_fn, name("exists")); MK_CONSTANT(eq_fn, name("eq")); MK_CONSTANT(neq_fn, name("neq")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index b43d3906f..b77bf028c 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -25,6 +25,10 @@ expr mk_implies_fn(); bool is_implies_fn(expr const & e); inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); } inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app({mk_implies_fn(), e1, e2}); } +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)); } +inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app({mk_iff_fn(), e1, e2}); } 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)); } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 687d75052..2b7047eca 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 eq_heq.cpp io_state_stream.cpp printer.cpp + fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp hop_match.cpp ite.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 05ee0ad19..2cea1b5a8 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -21,7 +21,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/update_expr.h" #include "library/printer.h" -#include "library/eq_heq.h" +#include "library/equality.h" #include "library/elaborator/elaborator.h" #include "library/elaborator/elaborator_justification.h" @@ -1372,9 +1372,9 @@ class elaborator::imp { r = process_metavar(c, b, a, false); if (r != Continue) { return r == Processed; } - if (is_eq_heq(a) && is_eq_heq(b)) { - expr_pair p1 = eq_heq_args(a); - expr_pair p2 = eq_heq_args(b); + if (is_equality(a) && is_equality(b)) { + expr_pair p1 = get_equality_args(a); + expr_pair p2 = get_equality_args(b); justification new_jst(new destruct_justification(c)); push_new_eq_constraint(ctx, p1.first, p2.first, new_jst); push_new_eq_constraint(ctx, p1.second, p2.second, new_jst); diff --git a/src/library/eq_heq.cpp b/src/library/eq_heq.cpp deleted file mode 100644 index 86d81efd4..000000000 --- a/src/library/eq_heq.cpp +++ /dev/null @@ -1,22 +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 "library/expr_pair.h" -#include "kernel/kernel.h" - -namespace lean { -bool is_eq_heq(expr const & e) { - return is_heq(e) || is_eq(e); -} - -expr_pair eq_heq_args(expr const & e) { - lean_assert(is_heq(e) || is_eq(e)); - if (is_heq(e)) - return expr_pair(heq_lhs(e), heq_rhs(e)); - else - return expr_pair(arg(e, 2), arg(e, 3)); -} -} diff --git a/src/library/equality.cpp b/src/library/equality.cpp new file mode 100644 index 000000000..94e5f4b90 --- /dev/null +++ b/src/library/equality.cpp @@ -0,0 +1,44 @@ +/* +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 "library/expr_pair.h" +#include "kernel/kernel.h" + +namespace lean { +bool is_equality(expr const & e) { + return is_eq(e) || is_iff(e) || is_heq(e); +} + +bool is_equality(expr const & e, expr & lhs, expr & rhs) { + if (is_eq(e)) { + lhs = arg(e, 2); + rhs = arg(e, 3); + return true; + } else if (is_iff(e)) { + lhs = arg(e, 1); + rhs = arg(e, 2); + return true; + } else if (is_heq(e)) { + lhs = heq_lhs(e); + rhs = heq_rhs(e); + return true; + } else { + return false; + } +} + +expr_pair get_equality_args(expr const & e) { + if (is_eq(e)) { + return mk_pair(arg(e, 2), arg(e, 3)); + } else if (is_iff(e)) { + return mk_pair(arg(e, 1), arg(e, 2)); + } else if (is_heq(e)) { + return mk_pair(heq_lhs(e), heq_rhs(e)); + } else { + lean_unreachable(); // LCOV_EXCL_LINE + } +} +} diff --git a/src/library/eq_heq.h b/src/library/equality.h similarity index 62% rename from src/library/eq_heq.h rename to src/library/equality.h index 5b92bbda8..2716d3745 100644 --- a/src/library/eq_heq.h +++ b/src/library/equality.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "library/expr_pair.h" namespace lean { -bool is_eq_heq(expr const & e); -expr_pair eq_heq_args(expr const & e); +bool is_equality(expr const & e); +bool is_equality(expr const & e, expr & lhs, expr & rhs); +expr_pair get_equality_args(expr const & e); } diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp index 2262fd260..fa9434727 100644 --- a/src/library/fo_unify.cpp +++ b/src/library/fo_unify.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "library/fo_unify.h" #include "library/expr_pair.h" #include "library/kernel_bindings.h" -#include "library/eq_heq.h" +#include "library/equality.h" namespace lean { static void assign(substitution & s, expr const & mvar, expr const & e) { @@ -36,9 +36,9 @@ optional fo_unify(expr e1, expr e2) { assign(s, e1, e2); } else if (is_metavar_wo_local_context(e2)) { assign(s, e2, e1); - } else if (is_eq_heq(e1) && is_eq_heq(e2)) { - expr_pair p1 = eq_heq_args(e1); - expr_pair p2 = eq_heq_args(e2); + } else if (is_equality(e1) && is_equality(e2)) { + expr_pair p1 = get_equality_args(e1); + expr_pair p2 = get_equality_args(e2); todo.emplace_back(p1.second, p2.second); todo.emplace_back(p1.first, p2.first); } else { diff --git a/src/library/hop_match.cpp b/src/library/hop_match.cpp index f35551d94..83e9f42dd 100644 --- a/src/library/hop_match.cpp +++ b/src/library/hop_match.cpp @@ -8,7 +8,8 @@ Author: Leonardo de Moura #include "util/buffer.h" #include "kernel/free_vars.h" #include "kernel/instantiate.h" -#include "library/eq_heq.h" +#include "kernel/kernel.h" +#include "library/equality.h" #include "library/kernel_bindings.h" namespace lean { @@ -183,13 +184,13 @@ class hop_match_fn { return true; } - if (is_eq_heq(p) && is_eq_heq(t) && (is_heq(p) || is_heq(t))) { + if (is_equality(p) && is_equality(t) && (!is_eq(p) || !is_eq(t))) { // Remark: if p and t are homogeneous equality, then we handle as an application (in the else branch) // We do that because we can get more information. For example, the pattern // may be (eq #1 a b). // This branch ignores the type. - expr_pair p1 = eq_heq_args(p); - expr_pair p2 = eq_heq_args(t); + expr_pair p1 = get_equality_args(p); + expr_pair p2 = get_equality_args(t); return match(p1.first, p2.first, ctx, ctx_size) && match(p1.second, p2.second, ctx, ctx_size); } else { if (p.kind() != t.kind()) diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 15702429d..80e29f123 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/expr_pair.h" #include "library/ite.h" #include "library/kernel_bindings.h" +#include "library/equality.h" namespace lean { static name g_Hc("Hc"); // auxiliary name for if-then-else @@ -44,18 +45,18 @@ class to_ceqs_fn { } list apply(expr const & e, expr const & H) { - if (is_eq(e)) { + if (is_equality(e)) { return mk_singleton(e, H); } else if (is_neq(e)) { expr T = arg(e, 1); expr lhs = arg(e, 2); expr rhs = arg(e, 3); - expr new_e = mk_eq(Bool, mk_eq(T, lhs, rhs), False); + expr new_e = mk_iff(mk_eq(T, lhs, rhs), False); expr new_H = mk_neq_elim_th(T, lhs, rhs, H); return mk_singleton(new_e, new_H); } else if (is_not(e)) { expr a = arg(e, 1); - expr new_e = mk_eq(Bool, a, False); + expr new_e = mk_iff(a, False); expr new_H = mk_eqf_intro_th(a, H); return mk_singleton(new_e, new_H); } else if (is_and(e)) { @@ -99,7 +100,7 @@ class to_ceqs_fn { }); return append(new_then_ceqs, new_else_ceqs); } else { - return mk_singleton(mk_eq(Bool, e, True), mk_eqt_intro_th(e, H)); + return mk_singleton(mk_iff(e, True), mk_eqt_intro_th(e, H)); } } public: @@ -146,8 +147,8 @@ bool is_ceq(ro_environment const & env, expr e) { ctx = extend(ctx, abst_name(e), abst_domain(e)); e = abst_body(e); } - if (is_eq(e)) { - expr lhs = arg(e, 2); + expr lhs, rhs; + if (is_equality(e, lhs, rhs)) { // traverse lhs, and mark all variables that occur there in is_lhs. for_each(lhs, visitor_fn); return std::find(found_args.begin(), found_args.end(), false) == found_args.end(); @@ -211,13 +212,14 @@ bool is_permutation_ceq(expr e) { e = abst_body(e); num_args++; } - if (!is_eq(e)) + expr lhs, rhs; + if (is_equality(e, lhs, rhs)) { + buffer> permutation; + permutation.resize(num_args); + return is_permutation(lhs, rhs, 0, permutation); + } else { return false; - expr lhs = arg(e, 2); - expr rhs = arg(e, 3); - buffer> permutation; - permutation.resize(num_args); - return is_permutation(lhs, rhs, 0, permutation); + } } static int to_ceqs(lua_State * L) {