From ad7b13104fcd88c9591ed09de92b4d5f53e41a90 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Feb 2014 15:03:16 -0800 Subject: [PATCH] feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes Signed-off-by: Leonardo de Moura --- examples/lean/dep_if.lean | 22 +-- src/builtin/kernel.lean | 201 ++++++++++++++----------- src/builtin/obj/kernel.olean | Bin 48642 -> 49077 bytes src/frontends/lean/parser_expr.cpp | 10 ++ src/frontends/lean/parser_imp.h | 1 + src/frontends/lean/scanner.cpp | 4 + src/frontends/lean/scanner.h | 2 +- src/kernel/kernel_decls.cpp | 9 +- src/kernel/kernel_decls.h | 27 +++- src/kernel/level.cpp | 7 +- src/library/elaborator/elaborator.cpp | 121 +++++++++------ src/library/simplifier/simplifier.cpp | 203 ++++++++++++-------------- tests/lean/loop3.lean | 4 +- tests/lean/rs.lean.expected.out | 10 +- tests/lean/simp18.lean | 4 +- tests/lean/simp18.lean.expected.out | 6 +- tests/lean/simp19.lean | 7 +- tests/lean/simp19.lean.expected.out | 16 +- tests/lean/simp20.lean | 2 + tests/lean/simp20.lean.expected.out | 3 +- tests/lean/simp22.lean | 7 +- tests/lean/simp22.lean.expected.out | 16 +- tests/lean/simp23.lean | 9 +- tests/lean/simp23.lean.expected.out | 6 +- tests/lean/simp28.lean | 7 +- tests/lean/simp28.lean.expected.out | 1 + tests/lean/simp30.lean | 4 +- tests/lean/simp32.lean | 4 +- tests/lean/simp32.lean.expected.out | 7 +- 29 files changed, 417 insertions(+), 303 deletions(-) diff --git a/examples/lean/dep_if.lean b/examples/lean/dep_if.lean index 6f28f3805..d01d9445d 100644 --- a/examples/lean/dep_if.lean +++ b/examples/lean/dep_if.lean @@ -10,16 +10,16 @@ import tactic -- We define the "dependent" if-then-else using Hilbert's choice operator ε. -- Note that ε is only applicable to non-empty types. Thus, we first -- prove the following auxiliary theorem. -theorem inhabited_resolve {A : TypeU} {c : Bool} (t : c → A) (e : ¬ c → A) : inhabited A +theorem inhabited_resolve {A : (Type U)} {c : Bool} (t : c → A) (e : ¬ c → A) : inhabited A := or_elim (em c) (λ Hc, inhabited_range (inhabited_intro t) Hc) (λ Hnc, inhabited_range (inhabited_intro e) Hnc) -- The actual definition -definition dep_if {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) : A +definition dep_if {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) : A := ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) -theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : c) +theorem then_simp (A : (Type U)) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : c) : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = t H := let s1 : (∀ Hc : c, r = t Hc) ↔ r = t H := iff_intro @@ -32,17 +32,17 @@ theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) in by simp -- Given H : c, (dep_if c t e) = t H -theorem dep_if_elim_then {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : c) : dep_if c t e = t H +theorem dep_if_elim_then {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) (H : c) : dep_if c t e = t H := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = t H) := funext (λ r, then_simp A c r t e H) in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) ... = ε (inhabited_resolve t e) (λ r, r = t H) : { s1 } ... = t H : eps_singleton (inhabited_resolve t e) (t H) -theorem dep_if_true {A : TypeU} (t : true → A) (e : ¬ true → A) : dep_if true t e = t trivial +theorem dep_if_true {A : (Type U)} (t : true → A) (e : ¬ true → A) : dep_if true t e = t trivial := dep_if_elim_then true t e trivial -theorem else_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : ¬ c) +theorem else_simp (A : (Type U)) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : ¬ c) : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H := let s1 : (∀ Hc : c, r = t Hc) ↔ true := eqt_intro (λ Hc : c, absurd_elim (r = t Hc) Hc H), @@ -55,19 +55,21 @@ theorem else_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) in by simp -- Given H : ¬ c, (dep_if c t e) = e H -theorem dep_if_elim_else {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (H : ¬ c) : dep_if c t e = e H +theorem dep_if_elim_else {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) (H : ¬ c) : dep_if c t e = e H := let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = e H) := funext (λ r, else_simp A c r t e H) in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e) ... = ε (inhabited_resolve t e) (λ r, r = e H) : { s1 } ... = e H : eps_singleton (inhabited_resolve t e) (e H) -theorem dep_if_false {A : TypeU} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial +theorem dep_if_false {A : (Type U)} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial := dep_if_elim_else false t e not_false_trivial set_option simplifier::heq true -- enable heterogeneous equality support -theorem dep_if_congr {A : TypeM} (c1 c2 : Bool) +universe M >= 1 + +theorem dep_if_congr {A : (Type M)} (c1 c2 : Bool) (t1 : c1 → A) (t2 : c2 → A) (e1 : ¬ c1 → A) (e2 : ¬ c2 → A) (Hc : c1 = c2) @@ -89,7 +91,7 @@ pop_scope -- If the dependent then/else branches do not use the proofs Hc : c and Hn : ¬ c, then we -- can reduce the dependent-if to a regular if -theorem dep_if_if {A : TypeU} (c : Bool) (t e : A) : dep_if c (λ Hc, t) (λ Hn, e) = if c then t else e +theorem dep_if_if {A : (Type U)} (c : Bool) (t e : A) : dep_if c (λ Hc, t) (λ Hn, e) = if c then t else e := or_elim (em c) (assume Hc : c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hc, t) Hc : dep_if_elim_then _ _ _ Hc ... = if c then t else e : by simp) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 057dbb82d..cce49abb6 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -11,12 +11,11 @@ definition TypeU := (Type U) (* mk_rewrite_rule_set() *) variable Bool : Type --- Heterogeneous equality -variable heq2 {A B : (Type U)} (a : A) (b : B) : Bool -infixl 50 == : heq2 -- Reflexivity for heterogeneous equality -axiom hrefl {A : (Type U)} (a : A) : a == a +-- We use universe U+1 in heterogeneous equality axioms because we want to be able +-- to state the equality between A and B of (Type U) +axiom hrefl {A : (Type U+1)} (a : A) : a == a -- Homogeneous equality definition eq {A : (Type U)} (a b : A) := a == b @@ -177,10 +176,10 @@ 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 to_eq {A : TypeU} {a b : A} (H : a == b) : a = b +theorem to_eq {A : (Type U)} {a b : A} (H : a == b) : a = b := (heq_eq a b) ◂ H -theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b +theorem to_heq {A : (Type U)} {a b : A} (H : a = b) : a == b := (symm (heq_eq a b)) ◂ H theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b @@ -189,13 +188,13 @@ theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a := (λ Hb : b, eqmpr H Hb) -theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a +theorem ne_symm {A : (Type U)} {a b : A} (H : a ≠ b) : b ≠ a := assume H1 : b = a, H (symm H1) -theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c +theorem eq_ne_trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := subst H2 (symm H1) -theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c +theorem ne_eq_trans {A : (Type U)} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := subst H1 H2 theorem eqt_elim {a : Bool} (H : a = true) : a @@ -231,12 +230,12 @@ theorem not_not_eq (a : Bool) : (¬ ¬ a) = a add_rewrite not_not_eq -theorem not_neq {A : TypeU} (a b : A) : ¬ (a ≠ b) ↔ a = b +theorem not_neq {A : (Type U)} (a b : A) : ¬ (a ≠ b) ↔ a = b := not_not_eq (a = b) add_rewrite not_neq -theorem not_neq_elim {A : TypeU} {a b : A} (H : ¬ (a ≠ b)) : a = b +theorem not_neq_elim {A : (Type U)} {a b : A} (H : ¬ (a ≠ b)) : a = b := (not_neq a b) ◂ H theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a @@ -302,6 +301,9 @@ theorem eq_id {A : (Type U)} (a : A) : (a = a) ↔ true theorem iff_id (a : Bool) : (a ↔ a) ↔ true := eqt_intro (refl a) +theorem heq_id (A : (Type U+1)) (a : A) : (a == a) ↔ true +:= eqt_intro (hrefl a) + theorem neq_elim {A : (Type U)} {a b : A} (H : a ≠ b) : a = b ↔ false := eqf_intro H @@ -429,12 +431,12 @@ theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b := congr2 not H -- Recall that exists is defined as ¬ ∀ x : A, ¬ P x -theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B +theorem exists_elim {A : (Type U)} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B := refute (λ R : ¬ B, absurd (take a : A, mt (assume H : P a, H2 a H) R) H1) -theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P +theorem exists_intro {A : (Type U)} {P : A → Bool} (a : A) (H : P a) : Exists A P := assume H1 : (∀ x : A, ¬ P x), absurd H (H1 a) @@ -445,14 +447,14 @@ theorem not_exists (A : (Type U)) (P : A → Bool) : ¬ (∃ 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 -theorem exists_unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) +theorem exists_unfold1 {A : (Type U)} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) := exists_elim H (λ (w : A) (H1 : P w), or_elim (em (w = a)) (λ Heq : w = a, or_introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) (λ Hne : w ≠ a, or_intror (P a) (exists_intro w (and_intro Hne H1)))) -theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x +theorem exists_unfold2 {A : (Type U)} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x := or_elim H (λ H1 : P a, exists_intro a H1) (λ H2 : (∃ x : A, x ≠ a ∧ P x), @@ -460,7 +462,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 : (Type U)} (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) @@ -468,19 +470,19 @@ definition inhabited (A : (Type U)) := ∃ x : A, true -- If we have an element of type A, then A is inhabited -theorem inhabited_intro {A : TypeU} (a : A) : inhabited A +theorem inhabited_intro {A : (Type U)} (a : A) : inhabited A := assume H : (∀ x, ¬ true), absurd_not_true (H a) -theorem inhabited_elim {A : TypeU} (H1 : inhabited A) {B : Bool} (H2 : A → B) : B +theorem inhabited_elim {A : (Type U)} (H1 : inhabited A) {B : Bool} (H2 : A → B) : B := obtain (w : A) (Hw : true), from H1, H2 w -theorem inhabited_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : inhabited A +theorem inhabited_ex_intro {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : inhabited A := obtain (w : A) (Hw : P w), from H, exists_intro w trivial -- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty -theorem inhabited_range {A : TypeU} {B : A → TypeU} (H : inhabited (∀ x, B x)) (a : A) : inhabited (B a) +theorem inhabited_range {A : (Type U)} {B : A → (Type U)} (H : inhabited (∀ x, B x)) (a : A) : inhabited (B a) := refute (λ N : ¬ inhabited (B a), let s1 : ¬ ∃ x : B a, true := N, s2 : ∀ x : B a, false := take x : B a, absurd_not_true (not_exists_elim s1 x), @@ -489,7 +491,7 @@ theorem inhabited_range {A : TypeU} {B : A → TypeU} (H : inhabited (∀ x, B x let s4 : B a := w a in s2 s4) -theorem exists_rem {A : TypeU} (H : inhabited A) (p : Bool) : (∃ x : A, p) ↔ p +theorem exists_rem {A : (Type U)} (H : inhabited A) (p : Bool) : (∃ x : A, p) ↔ p := iff_intro (assume Hl : (∃ x : A, p), obtain (w : A) (Hw : p), from Hl, @@ -497,7 +499,7 @@ theorem exists_rem {A : TypeU} (H : inhabited A) (p : Bool) : (∃ x : A, p) ↔ (assume Hr : p, inhabited_elim H (λ w, exists_intro w Hr)) -theorem forall_rem {A : TypeU} (H : inhabited A) (p : Bool) : (∀ x : A, p) ↔ p +theorem forall_rem {A : (Type U)} (H : inhabited A) (p : Bool) : (∀ x : A, p) ↔ p := iff_intro (assume Hl : (∀ x : A, p), inhabited_elim H (λ w, Hl w)) @@ -669,7 +671,7 @@ theorem not_iff (a b : Bool) : ¬ (a ↔ b) ↔ (¬ a ↔ b) theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b := (not_iff a b) ◂ H -theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x) +theorem forall_or_distributer {A : (Type U)} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x) := boolext (assume H : (∀ x, p ∨ φ x), or_elim (em p) @@ -694,14 +696,14 @@ theorem forall_or_distributel {A : Type} (p : Bool) (φ : A → Bool) : (∀ x, (λ H1 : (∀ x, φ x), or_introl (H1 x) p) (λ H2 : p, or_intror (φ x) H2)) -theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x) +theorem forall_and_distribute {A : (Type U)} (φ ψ : 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 : (Type U)} (p : Bool) (φ : A → Bool) : (∃ x, p ∧ φ x) ↔ p ∧ ∃ x, φ x := boolext (assume H : (∃ x, p ∧ φ x), obtain (w : A) (Hw : p ∧ φ w), from H, @@ -711,7 +713,7 @@ theorem exists_and_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x exists_intro w (and_intro (and_eliml H) Hw)) -theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x) +theorem exists_or_distribute {A : (Type U)} (φ ψ : A → Bool) : (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x) := boolext (assume H : (∃ x, φ x ∨ ψ x), obtain (w : A) (Hw : φ w ∨ ψ w), from H, @@ -743,12 +745,12 @@ theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ ( theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x := (not_forall A P) ◂ H -theorem exists_and_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p +theorem exists_and_distributel {A : (Type U)} (p : Bool) (φ : A → Bool) : (∃ x, φ x ∧ p) ↔ (∃ x, φ x) ∧ p := calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p) ... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ ... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x) -theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x)) +theorem exists_imp_distribute {A : (Type U)} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x)) := calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x) : eq_exists_intro (λ x, imp_or (φ x) (ψ x)) ... = (∃ x, ¬ φ x) ∨ (∃ x, ψ x) : exists_or_distribute _ _ ... = ¬ (∀ x, φ x) ∨ (∃ x, ψ x) : { symm (not_forall A φ) } @@ -770,36 +772,36 @@ theorem allext {A : (Type U)} {B C : A → Bool} (H : ∀ x : A, B x = C x) : ( axiom funext {A : (Type U)} {B : A → (Type U)} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g -- Eta is a consequence of function extensionality -theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f +theorem eta {A : (Type U)} {B : A → (Type U)} (f : ∀ x : A, B x) : (λ x : A, f x) = f := funext (λ x : A, refl (f x)) -- Epsilon (Hilbert's operator) -variable eps {A : TypeU} (H : inhabited A) (P : A → Bool) : A +variable eps {A : (Type U)} (H : inhabited A) (P : A → Bool) : A alias ε : eps -axiom eps_ax {A : TypeU} (H : inhabited A) {P : A → Bool} (a : A) : P a → P (ε H P) +axiom eps_ax {A : (Type U)} (H : inhabited A) {P : A → Bool} (a : A) : P a → P (ε H P) -theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (inhabited_intro a) P) +theorem eps_th {A : (Type U)} {P : A → Bool} (a : A) : P a → P (ε (inhabited_intro a) P) := assume H : P a, @eps_ax A (inhabited_intro a) P a H -theorem eps_singleton {A : TypeU} (H : inhabited A) (a : A) : ε H (λ x, x = a) = a +theorem eps_singleton {A : (Type U)} (H : inhabited A) (a : A) : ε H (λ x, x = a) = a := let P := λ x, x = a, Ha : P a := refl a in eps_ax H a Ha -- A function space (∀ x : A, B x) is inhabited if forall a : A, we have inhabited (B a) -theorem inhabited_fun {A : TypeU} {B : A → TypeU} (Hn : ∀ a, inhabited (B a)) : inhabited (∀ x, B x) +theorem inhabited_fun {A : (Type U)} {B : A → (Type U)} (Hn : ∀ a, inhabited (B a)) : inhabited (∀ x, B x) := inhabited_intro (λ x, ε (Hn x) (λ y, true)) -theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (inhabited_ex_intro H) P) +theorem exists_to_eps {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : P (ε (inhabited_ex_intro H) P) := obtain (w : A) (Hw : P w), from H, eps_ax (inhabited_ex_intro H) w Hw -theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) +theorem axiom_of_choice {A : (Type U)} {B : A → (Type U)} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) := exists_intro (λ x, ε (inhabited_ex_intro (H x)) (λ y, R x y)) -- witness for f (λ x, exists_to_eps (H x)) -- proof that witness satisfies ∀ x, R x (f x) -theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} : +theorem skolem_th {A : (Type U)} {B : A → (Type U)} {P : ∀ x : A, B x → Bool} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) := iff_intro (λ H : (∀ x, ∃ y, P x y), axiom_of_choice H) @@ -808,21 +810,21 @@ theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} : exists_intro (fw x) (Hw x)) -- if-then-else expression, we define it using Hilbert's operator -definition ite {A : TypeU} (c : Bool) (a b : A) : A +definition ite {A : (Type U)} (c : Bool) (a b : A) : A := ε (inhabited_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b)) notation 45 if _ then _ else _ : ite -theorem if_true {A : TypeU} (a b : A) : (if true then a else b) = a +theorem if_true {A : (Type U)} (a b : A) : (if true then a else b) = a := calc (if true then a else b) = ε (inhabited_intro a) (λ r, (true → r = a) ∧ (¬ true → r = b)) : refl (if true then a else b) ... = ε (inhabited_intro a) (λ r, r = a) : by simp ... = a : eps_singleton (inhabited_intro a) a -theorem if_false {A : TypeU} (a b : A) : (if false then a else b) = b +theorem if_false {A : (Type U)} (a b : A) : (if false then a else b) = b := calc (if false then a else b) = ε (inhabited_intro a) (λ r, (false → r = a) ∧ (¬ false → r = b)) : refl (if false then a else b) ... = ε (inhabited_intro a) (λ r, r = b) : by simp ... = b : eps_singleton (inhabited_intro a) b -theorem if_a_a {A : TypeU} (c : Bool) (a: A) : (if c then a else a) = a +theorem if_a_a {A : (Type U)} (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) @@ -831,7 +833,7 @@ theorem if_a_a {A : TypeU} (c : Bool) (a: A) : (if c then a else a) = a add_rewrite if_true if_false if_a_a -theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c) +theorem if_congr {A : (Type U)} {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) @@ -860,7 +862,7 @@ theorem if_imp_else {a b c : Bool} (H : if a then b else c) : ¬ a → 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 +theorem app_if_distribute {A B : (Type U)} (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 } @@ -873,10 +875,10 @@ theorem app_if_distribute {A B : TypeU} (c : Bool) (f : A → B) (a b : A) : f ( ... = 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 +theorem eq_if_distributer {A : (Type U)} (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 +theorem eq_if_distributel {A : (Type U)} (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 @@ -902,67 +904,98 @@ axiom pairext {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} -- Heterogeneous equality axioms and theorems --- In the following definitions the type of A and B cannot be (Type U) --- because A = B would be @eq (Type U+1) A B, and --- the type of eq is (∀T : (Type U), T → T → bool). --- So, we define M a universe smaller than U. -universe M ≥ 1 -definition TypeM := (Type M) +-- We can "type-cast" an A expression into a B expression, if we can prove that A == B +-- Remark: we use A == B instead of A = B, because A = B would be type incorrect. +-- A = B is actually (@eq (Type U) A B), which is type incorrect because +-- the first argument of eq must have type (Type U) and the type of (Type U) is (Type U+1) +variable cast {A B : (Type U+1)} : A == B → A → B --- We can "type-cast" an A expression into a B expression, if we can prove that A = B -variable cast {A B : (Type M)} : A = B → A → B -axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a +axiom cast_heq {A B : (Type U+1)} (H : A == B) (a : A) : cast H a == a --- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence and function extensionality -axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a -axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c -axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : +-- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence, function extensionality, ... + +-- Heterogeneous version of subst +axiom hsubst {A B : (Type U+1)} {a : A} {b : B} (P : ∀ T : (Type U+1), T → Bool) : P A a → a == b → P B b + +theorem hsymm {A B : (Type U+1)} {a : A} {b : B} (H : a == b) : b == a +:= hsubst (λ (T : (Type U+1)) (x : T), x == a) (hrefl a) H + +theorem htrans {A B C : (Type U+1)} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c +:= hsubst (λ (T : (Type U+1)) (x : T), a == x) H1 H2 + +axiom hcongr {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} : f == f' → a == a' → f a == f' a' -axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : - A = A' → (∀ x x', x == x' → f x == f' x') → f == f' + +axiom hfunext {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} {f : ∀ x, B x} {f' : ∀ x, B' x} : + A == A' → (∀ x x', x == x' → f x == f' x') → f == f' + +axiom hpiext {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} : + A == A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) + +axiom hsigext {A A' : (Type U+1)} {B : A → (Type U+1)} {B' : A' → (Type U+1)} : + A == A' → (∀ x x', x == x' → B x == B' x') → (sig x, B x) == (sig x, B' x) -- Heterogeneous version of the allext theorem -theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool} - (Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x) -:= boolext - (assume (H : ∀ x : A, B x), - take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x'))) - (assume (H : ∀ x' : A', B' x'), - take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x))) +theorem hallext {A A' : (Type U+1)} {B : A → Bool} {B' : A' → Bool} + (Ha : A == A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x) +:= to_eq (hpiext Ha (λ x x' Heq, to_heq (Hb x x' Heq))) -- Simpler version of hfunext axiom, we use it to build proofs -theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : +theorem hsfunext {A : (Type U)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} : (∀ x, f x == f' x) → f == f' := λ Hb, - hfunext (refl A) (λ (x x' : A) (Hx : x == x'), + hfunext (hrefl A) (λ (x x' : A) (Heq : x == x'), let s1 : f x == f' x := Hb x, - s2 : f' x == f' x' := hcongr (hrefl f') Hx + s2 : f' x == f' x' := hcongr (hrefl f') Heq in htrans s1 s2) +theorem heq_congr {A B : (Type U)} {a a' : A} {b b' : B} (H1 : a = a') (H2 : b = b') : (a == b) = (a' == b') +:= calc (a == b) = (a' == b) : { H1 } + ... = (a' == b') : { H2 } + +theorem hheq_congr {A A' B B' : (Type U+1)} {a : A} {a' : A'} {b : B} {b' : B'} (H1 : a == a') (H2 : b == b') : (a == b) = (a' == b') +:= have Heq1 : (a == b) = (a' == b), + from (hsubst (λ (T : (Type U+1)) (x : T), (a == b) = (x == b)) (refl (a == b)) H1), + have Heq2 : (a' == b) = (a' == b'), + from (hsubst (λ (T : (Type U+1)) (x : T), (a' == b) = (a' == x)) (refl (a' == b)) H2), + show (a == b) = (a' == b'), + from trans Heq1 Heq2 + +theorem type_eq {A B : (Type U)} {a : A} {b : B} (H : a == b) : A == B +:= hsubst (λ (T : (Type U+1)) (x : T), A == T) (hrefl A) H + -- Some theorems that are useful for applying simplifications. -theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a +theorem cast_eq {A : (Type U)} (H : A == A) (a : A) : cast H a = a := to_eq (cast_heq H a) -theorem cast_trans {A B C : (Type M)} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a -:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a), - s2 : cast Hab a == a := cast_heq Hab a, - s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a, - s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3) - in to_eq s4 +theorem cast_trans {A B C : (Type U)} (Hab : A == B) (Hbc : B == C) (a : A) : cast Hbc (cast Hab a) = cast (htrans Hab Hbc) a +:= have Heq1 : cast Hbc (cast Hab a) == cast Hab a, + from cast_heq Hbc (cast Hab a), + have Heq2 : cast Hab a == a, + from cast_heq Hab a, + have Heq3 : cast (htrans Hab Hbc) a == a, + from cast_heq (htrans Hab Hbc) a, + show cast Hbc (cast Hab a) = cast (htrans Hab Hbc) a, + from to_eq (htrans (htrans Heq1 Heq2) (hsymm Heq3)) -theorem cast_pull {A : (Type M)} {B B' : A → (Type M)} - (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) : +theorem cast_pull {A : (Type U)} {B B' : A → (Type U)} + (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) == (∀ x, B' x)) (Hba : (B a) == (B' a)) : cast Hb f a = cast Hba (f a) -:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a), - s2 : cast Hba (f a) == f a := cast_heq Hba (f a) - in to_eq (htrans s1 (hsymm s2)) +:= have s1 : cast Hb f a == f a, + from hcongr (cast_heq Hb f) (hrefl a), + have s2 : cast Hba (f a) == f a, + from cast_heq Hba (f a), + show cast Hb f a = cast Hba (f a), + from to_eq (htrans s1 (hsymm s2)) -- Proof irrelevance is true in the set theoretic model we have for Lean. axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 -- A more general version of proof_irrel that can be be derived using proof_irrel, heq axioms and boolext/iff_intro theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2 -:= let H1b : b := cast (by simp) H1, - H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) H1), +:= let Hab : a == b := to_heq (iff_intro (assume Ha, H2) (assume Hb, H1)), + H1b : b := cast Hab H1, + H1_eq_H1b : H1 == H1b := hsymm (cast_heq Hab H1), H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2) in htrans H1_eq_H1b H1b_eq_H2 + diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index ce394517b6b79456eba540bbcd1751c252363593..c7aeb2880d51a66770d1cb614a5cc34fb7c0ae0d 100644 GIT binary patch literal 49077 zcmcJ236xz`mG&LptNW@df*@#ULBT*mXbggA;>0`z41(aWRIpM>s$L3{s*tKcP}Cqz z8U&|~3@SD%2%=z%1E{pE*tQLhEwLTYw6uWQNQYf8Teed*4d|{_C%`a3$D{qFn+!0ieX%4PYf%z&Fc8$IG&d z)i{;Utluyu3^C~x8+D1YLmp2gh=POL7h{-NKXLZN=o;1Rp6!d)r=XaJV&9Y3$#}cV zuH&O?%+c`IsnIVz-rRh2&BUmA)sNqNE%D}u>ko>@T>0gsIVk?-Rn9$(pz{+{FRWYm zi#MV&+n;jpDGF2T>5ZtTQs!}t`|!FlS0ezT9La&WBt}&yecpML>nS9?cUEsa{U9}> z^C9)7A7AvLq>WxbI=Kpn+0(#s?(c4pXBCIjs*=l4mw?ppuV`?@5dKi zpR`eqiM8w2OpHwfxt}aGDJu4uG&jcIaODC$_d_WC5UQxgJ-quJVqKcS_~VP;mxSXX z49C$CV=yv0GPY)7ZQsPOG^5iV4jHH%YJtTBx5V*o0^j|Ir4kS~w6 z8fB}|71JBmud0zc82CucODS5m2$xd$@c>1Y93|@ss9hw50}NU|&MtiJ-#9TnGo70G zl)#jlqk={Hg&-ocE(3Uml;d-Y^Ep<^BAQ*uVZ)AQnE+|=mIkg_+-1tIYX`-wUpQ?PC;`v&vbdPG7bsM zr*7i_76y-C9ch-ZH8ZOZ5a%@B*b70qq5@6_DBYa_aN&Hic^TkL^Td+~v$_K1wKGBe zmSaO+G%@kFBpRO*(J{N^HG+2WS{^~lwuA_zwa7eI@^<$lQ@BEwbxDn(C{cVozS&ygjgns!M};HRz`ymZFE*g3P5NPUTY3 z2JjMiHb9FzCk>NJh#%NoY**NlbLEsxSz|MZBgaq)lX~QWj7fu@G{0Y^k`|-6Gar0k z=i{9nKOxtgRFFr4M4eAwT=WpR$$&@;MPa&0fw8%;ArdQ_WLe2rPe(j5ea`5*bz@0h z*2po2kE6JmdOiirT_$L&fLqY!Q$EK&&oIQ4M)OKQU zvsRRVys7nf5_}_Q$hw;%cs{^8&Cr@fw%~HP_pdkDg~cN7C8js5m_{->5(rsbmV53N zgmJ2%ms-Lyd6-Hlg(YfZB5fB&qXj};6myBhPF>IX0;_N3_J?Fc=8To>2gz(9cZ;i> z$|dq|1;4#34D8!le_p`FdmCK0q7Z*TQkQ3ciPe;z`?+iTuY43}NIxKu?V+&&Bw12a zkWsCgE8mHBh5Tgzm4_||xX1n|e~2QH%LhX@lBeiYYB&0S>=Lro-x(!83d`1$wVB;% zFEQXsaK?mcc8km+T_xJsLNREzDpqa-4Yg1K@4~f){%(L8`g;Is=vM)hn%)cWVRrj_ zfWM9kAz6vS_AAi7O>E&!1H48-y$~np;YzCx&SW!JcRk`Kxbjix2A>`$VAECB_vy^v2ZCTD6Lbhq7sN@(N791_bVjIb5{5}<9CLO>`pt%5hC3Z_XqU{U{z*XO8 zEY*Wz_L(?}4zA~;-~>)vb2jEw>Xw(dQ{x5Cbe46d=#@W29WIE_za-=9^6i#Qv;&<5Hn(maQQZ=sx73_g&ZHsW# z;wJ_!y-;F*gUDp{%?SQm1ixjVGuK@L{XJEZ>^6I6{<@*~85v^Q*2-g*H0A~BL%{;h zYboV-40L+_ZUny|xz;FwgJMWAC-@iGa2voz5;YNw}57+6(-$J?vk81(o<; zxR!(u0F;D32Pg?21h_}E>ce)KU%~5fG{J##CUv%OsTTD2Gi&tX+2$K>!)rIYn%fXa zy6ad5k`xSy#JSinP$}y^6v1Bt;f7$-xlzO}kfI`kH2-bYKD?bUJIFyGkl%n}1%>%F zDkQ;gBKTV%Kmv`TQl7a32s<3!BY62$x8&#hz=Rw&~3ut9FE z!XZUwTK=;#iAE0We@UL;{{hG$<)q9Z<%Bu>97_rXUrrCYV}Dd2jT!4m2Ey~P<}VN4WahY-2z1&aJW3a{zTShAkckHa0o?W%2;FjHtLP9a6F>dn5 zu_*>AAeVy20aAYQV++}z=cc@T*buaI8#_x`BwhW8?Z-idTjKf70L7N;`HyRJ?r2n- zWPTb*CIBjaA)8TzA@5`tVr;3k-+(zn3abH8>rVg;@!t&ueoy`!1;$MDdx6t4YCqsz z(T)2SVQEQM;c%d;{4{i5I9!Zw*qG(>aB*NijQKWNG!})PEPXE9AD0XW(BVQ<#JJQu z55vfVMbsjTNbWbFQ-Lrma*^DK8X)tnEKe~6{Nr>w%8s2xyHYo* zPeP$sdJ`H7f78%i-|8QODpr; zxqFe%rJ;*Gftav_4rQx_4VKjI{2jC8_?s+ISztiLK2~JCns!L{F>XO#2N7P8I)T)3$=xT2n&I%mX!$^Hs;rh+J- zlFlMFHTdi4UPWUag3dH`;CZ0c#EirH3gftg#oFZPisUwT38-oMeFi`Y!3kd=*cB%# z34)Jd4;M>ErdLm$leyf5$}N_w+(XbUH0*^|Xs+3kP=>q8kdIbMAe4$`J9a_I2Q+@#S;a68Axd)m{f|(xTTkaoC^(F zUTHf!Le(aXZV^Djrc{5qh)TW^l~l5Su#~^lY7|s>o;J2|2amZeQ{iuk3A}>V%vUfB z!b(c9Aoo2TsFM7Q2)-KN5)N&|pnL@;fa1!2WSY+oyXXql6z`vhlIw98Zj|~it`jLV zU5DcO2GNk`iVs<*6=^5U?AA#)Hq4Dg*RpmTEgclBWHYq7f(^y>Qfq@99c3$IN>+&M zPxJ1JF=TvRl+$U59}G6?NH@o1eTo}Uq+OAe?*&yA(ZVZbI-c?c+@x2t%62mLn0ABds>#&Zi~-%8|}AC||)Pbq@AB zUJO8~PB`3x^a!_&^8%Wv+u(5< zti~&IWCBnBn+wn==q~6kQ@#$M1U(O+j;Yc#S+)zi@OGfijC-cMnWT3&&l)U?tf*-g z;`atH;R%%DmkrAbHL~nb9;~c!EH)WZm?m^YkCD;>vRG^aNbTh310q)OOMt}Mor`rN zxx>SQicY_|nco(N^DwB$#1{aR=Kcnt*6j2#Eh09f{Wh&p;YhYrM-eRcCS3S6IW~Hx z;vHhscK&gOmTwqwejA8A4|d5f0w_@~1}IV93{V|tLg+KU&AayB0?)YDZfB(DT9q?! ztqx}|qqI=xnz8Yj5j%5JJCbl}G?ZV$(2Z;f<4`w3M66EFC7@GIoJTn&qya%2B*AMG zr>Cb@8VeCIq9W4m6mU*oOhwy0;|Hnj zq{=Bq1d=H%HpvdcLNA%<0%O;YxxZ7@d~uK2eby| zhf_T14Y+Q-1W0OPCDTFTzNAY2dq)1GPa#5Bz17IXRkw3AuG8>%%}u<~H4qiqos@`^ zf!I>{??;p7mk$t(^9v@K@_3)5@1$0*1Wr`Q4Y-V}PWkq2sEnFJGr8Km1X^xEq2U1X z>+$mV$RLck*aVcwKorP;6v!nq5PvdI3wqB*?ApDF52dD>EKq^wjtnZTLte)_YKPMCr0#*%)=XJZgq9th_;;;<{XJ1(l?s zDJM`1j73F%K&Qs#B3&8;>MW@PMLc_w5&Z-Pl7^!8%jMRGS)_ciAK$B@lo(mDDGaJy zZr5%qH*85M-rz;vS2 zl#IucO(yQQCVLDVb9CE`A}s^~<==ka2HZ;vAR+cYEkh%VCfJ^sSQh-Ggt_F(z7T7!6=Pr-SkCVC(5`A z*M7IZco?$UdzjYq@Eh;?Wl-D z9o;aKywo850)cxV;&TVC-O`gy^QL&z~j843zU?d7cHgpo`j^{sF7Zq8-3g;+@4%~}i2W|fPLzSZk{u;n{V zWLdVSmdbC|MqMHZ+zH`B!jdpmth-CQ({@y-Ol>S{YwNpI6&3rv2!0=+=9{|#E`mR4 ze~Q_UTT?u-Q!bB2QWLJ_PhE6nCCwL>5Z?hYci(5*t2{h zpyf9km9P=FlKW?M-k)-8DnKs(Ptb^?Drt$3J?|#-$VV#n34}Mq5|s^V1woyHGqpdK zMag0sgHk5ys#g{~vEL$l5ebRdVz$GNOX;$u<~K=1v}2*(Gehu zn?`>QFmZ%GsmV>Fe~R)@FRr7TNt%wJRuDKZm8SnZMrmRXP3jM!b7MYfwXLp{T$((8 z04zSMwi_%sb^ZWrg8R*~mWWE=#I5~+U!i+cLTe{n`+c6)PERF1a6ZgG1z#;j}mG@6_s!jI7tb=1DGgb zZ(Ii@>mJHbh;ap0P)~_>(1rX8v&E~p!nCf%T`8NM z6yVt~0We}{wBm7Ko3J?y*M44V9X5}bD8Nk1JV;t>_1yZ08hRXn;w11Yb_J++>B9C} zc2bQ*kHqN0oh0c4M|l!KeUr66(K%23~$c)E`I5qXz}^ zyOc)%75LZe05#=Dqchm6khr*{h<;gI0M|b^(hJkg9rRPsDLbQ697Vu#uPyB<(>N+b zn5%s6uC}$hl(>8l$uk;Ic!+D9s^U}v z?%0QCw@sR7sT~gzcouNCF^{~(pw{bgjmO#ezx8^KfU*Hwx1ogQo}e$46i}4k%hyZd z;d$1P=z_DXK{;{~+x6DSb%R0$k%z{=guTF}cn&~~|G5Bpdr>?OAe<9#jcvq*dqtW? zo6%Iufr=^+D6~JHQ6S+ud-70KpV#cs=?poQG#8Co`CVxeT@FkhZ7%qjN|rkUwP(<8 z_5|3mf32%T3D+x8tRT&hL)9+tUx8#1W$Srj6I3cgUF8*_cQ>hs%~avhU?iE20Vr)A zYf$SdM&M|3c(MYGN4MP!-0SIM1t*kre)nzwx35RYhRN}%HLGeb_64Eqe$cv+dO+0Y znpWfzUd`IsTui%C#aj(izDNNT3RHv!dIH)t&=Ud5ZC+?l>&6A8{YS4guL&H0g*a?| z8j#JH=iq;C2y*8!o1rPMqzsQo6Jv-D5OZ4V^BM>>N+BgWhqI05SjN6YO9sTn76jw& zY3ubMz!cs3yt%oZva`R|=gIsQ5-0cMZ~+NW8DtxU(>5;!*zQNG=MRy+UJWCAWeJI6 zoF~V0?vz@OM72wM8-)4>iaU54PVk``C8e2t*|TC`hT%3P}xjLkn7FOIj1er|-_ zlUdVA@SrS7DwYd3g1p-&<}zzFuJxLsyv#0J|3uro1WocF=2Cgk%TOy1dbvTZd*um0 z?cn-W6qi~7x6yu1&dIrT7b@ijfM_1zaC&Rqy1?pMpF@k~Tgj>CbkQ>MGFnDnCeP<|x13Fbc+>>A+JobC~{4v&Mc_nawDa5#HXq5yidK z@Q8sERUTtmu>ot?B zM^{YDj3uW9&{Om47{EL#*|^9&G{k%^<9z?#$xgXVchyp7@H zry;hB78+mSg~o`rAvY0tHWwe}b?DjN89nV4rML!(yN*$5^5wO_l{AwEwUza!P%AC0 zL+u_5tdx^>Az~3?Mt3);!;*sz$8;$Oo|kw07}nTTnP)mS5l6AHS9xKEkXhdohb8$o zfS;s38=xErJX`OHqGGJAk3<8qZ*~PbPz{g{>X)oo#tPaT115Q`g)zo19IbzmqQHFN zq9U5c&Zc+q>5Y)Aj8jE@<4#~8*$cp@MuyT_UM|iPa zw>guO#X`Fb=4;~&vCL<$LrfoPBQ2~M)H1y_4HA5Y-+ItH_p3v6w3sb>rbicNp ztUwePHR?^fKjWx~GYhWBL3iM9#kCytZ3elpdOK=6)Sd2l+Gn5!833`7wa<_a0M{2K z^jAl}C(76eBJ0u7wp~jr3sQ8MGTOUqP3@K5=lPVtO;Dg-Y_TGlt3W8u%D6L74jP|Y zKe}ek$fMGhb!zVcI?~L$07^6OHppq_J*ee$*!bSw3EaHC%_Bbak6 z9a(`1Wa-FCG*P(r8#%KETz*?XpGGL&2P7re_ebyp5xgdX*BaQ~MAKXc@cjL))Lp%% z=>vfaLE3MchbF2QbN>kRXiZ56yKG;a$mMelR|P2Y0ie7Yy)_i|)}4#PW-x|oS3gR!|;=|eEVWBaIZRn zVX!8%F0I~UaKn=|F~at{>%zA=?D^beFP;EY`DUUyk)B0!A44xr`{ zKzf@0=cy$WJv zi;}#DYmTUEK>JN_xZ+k+Dk*0 zyc31Iw1LBkaJE!@JGvqj%OC!3Uw|=M@58n7FG(>dFq5^fYH&hWYr4bK+5SKy%q0j~ z9$*YfhdM5n%uGO-C2Z0B1r!|Y=7tDSAs+$`96qyEv}H~jxBZ{M?=db=@BRN^)-Qp5 zV`@~0F9gdkptua`W!_T@Jhy!(imOok@{v?^pJDZNHzuO?eH?IIy~#WPeYHQHB-WpR+$T`{mlc`+LP~*W7QIO)+?4fsNZMQog64NoT)@cx zR|8$bxFdqls;m7<1ixxv`@2xHW6b7`~AqG{=k^!_Ym#*MqX-Qr~5bO<7e87KvZK&ISGEB2=%>Wtt7XE9@=pCffoVPyeysl%C4PKACBO!BlsHw-O}i{1`e!hY7&(%wIWsD zv+cUC`Z%HL2I~>DqFWcmRdF))%$q6cnc559_>ghyRoq_`N+(l6e}w!}5Hpy-KgHTV zNAQ0Qtc8-B3SiB|iM5XPQ-N}5eJc2ap@&i638BSRpD`#*f)BcrnumbdA{0EzQ5FCx zc3BdfZ)IV}QD20sViM&-`#12n=B&6FxCDls<#+*zxA1y{Y{;+S^+(@inAsMOu3Za0 zGRm%r(T%{?Te3VbthsR$q}2IBwF3zj$v6mTueNh@8=5xRKXpgo&33K<5sV%-Xe-MW ziulxrgeW&P!^G|<7v5`Jh`xNuK&QN#A~vNXK5u7qV6}*Kfnaux{c~raiMh$HX}9t;K$wud z7c|LR^T4OApd;5j(<;lA!9ATj((H7yuC*&@dpt4ttm_0!Y1ohQ<22lER^R)g3$URR zTh9B?(jBn8jV%y^E|+jXEVuzsN}^NBc;qle_s(W(%t!FGn~mGRtrS@|bOfIYNo3o- zfp9a1o%mX@3AMM%*LE?uudnT8)rqg!UIBlE!|$EMMLR8lMXY@i1+-{r2;yArX#gb- zy|QsQHtAIy%U)It{DAHd?rVw@gG0AohV~z!J?{BrOYF+dK%w#q6zLvZ=$g0D)cod; zKIBsDjW*{E7{|cBhcN4)9Sf_boC7>jorNut0j^O|=sq#$2+`d=&xn{m zqVnRkdSaN#^oyZ5#vGNI$g<7rn+-5WjGiQUzc>KR9W*hAciL)nmyP+fanKMp*~uhZotc&WOt#-uk; zqO6Is4nk#T9;!>qs#AeD*9-mgz-1P@e+KBy4{|Z%r~8<~Zf$! z$O(ZR%P1y$OIE7X|Ey5x5VEZL#GXK>I<%)$J`2~07t>JQA*zGWQJ)&AdkQm}ZZ6aS zp-1T%Qta#kP=2jmpVJTkiP#dq3!^2Y-dk&^yJBxs z^qE>)-8K3&1(Vd;q$=9BPrXzalBWGiQ&4BvUYAMXJKS$c56^1OfnCaD(XK>!96T z_g9i+NHq(Oct|H3g~;g)EUl^+H@Gr%ZZR08tI3N--OYfohp@ z+@TjvxUggR@*8S1J-&0E~<8J7g{X;if|GNE@M)~genhPTS%WVEbpwlpnBmjjXFW?|$A zL=vcuA}{P6DAKe*E|0MaxAvg2{GLvEf>pcKm^+(dcP^{!SJT!{tgw%)VT=4o_O)Y8 z>j>D*!#6h*8cfoFKcp1DD4>-mUAR8LIn@Cl<-KGE>8hCh>`F> zV|BSf)s=o;x}08nC2&Y7c|pU@l!!$at&oy;pc1_2I~E;lFJA)8tte&?S3=c+72J_l zeALkOhrReodA*;ZKIlkoU~z~G$mwK=azdO+M+c~iARgD02cuu6+tFJ9l5`0O&&Q;^ ztEp^=#An^Y@uwV1%q6uGMl~y9Z&Ow*9TaQ`Va6qHt7?e)G@=fu7PR31u~u4E>_&UR!ZcMSThLS!Ajr7@XNPDiXGsc8OA;qU-09Y#W-9DU#fS^0vVe1O zW^cuO^CIxc1}WDv@8vSfVzf|91>54#>>Db6U%xyP*9x}R0OaA%at*-5UU%7L^=+@B zyXM`o_qaK#YJPG+uwxGln8t z4_YAufw`U6L-BP~-h+ansusWL2GvX1?%kTYvS&|kQZ~zRqmvw3WF7TRCw6)Vj@D-l zbTla6oefYXI0v9Yh8jprz;Qn0RrKHjL-c2ey|$tRUC_~id`T1q?ot_706|!QEPBW~ zo;I$2Lq&cKtvW$Z`ICpm+pMMaAPq?~CvJ_dItU4*>JL`9S9D<*g`NVykLRIeJV5@R zL||P1HaZNnTm8<8K2m4NX=937o(DvIu#1|I)Trd)_+-O-qCS+04<6X4%(2UJshoBog#FOqHFzpy^DX5Mr<7 zfZuj&X?-<15UxAiH4I_CdN2_bnpSTe%wzAb zTBTkr)UFjKp4P9d;9g4yAEl-?s^9HEK(g*|yP=nVHk0r-njOZDIAIR!>}7>x=hNz& ztjYz4eGE}=bo#GwhUMZZhGfp$DPBxq(4LoC*rb853=Nx6D1+kKS%QkV5>3jM?*gbm zcsIa7BD}|-&N9faH(xG|hUfwdQ}!4+wk}O{gC+&XI6(UNTtKOIPU*EyK#p(ZQZZDK zmSyl3aqOJh;0O+_hnj3&Og2p;=&5{Uz-rhV{7@B{l6q|)w*{3Z;m0Q9?!qji?`vk~hSgVk~ralKjn z0@u0?zyjZmhD&0tX>LXB;Qm&`{fW-o?6N`#ba+~_*@84#J;ddE2_M#2J8wnx&%L!M zgg!sAoGARXQHlAwrW?pEH0Y}Og%6HT+Es00pRkj(k8Sft0dOhya08ydl+-3pL8w} z$Cj8-)aRp~R0K)%mfJSwhJu~kw1NIz@9+O?7yfzM8uxAbFh_^69gRL&eU4_*!$4_G zZ+TpY%If=eR%p z+OeT75)p&es(a9dcJ%LOm*2LUaQJ9!2G2cr$TJec98mo?sPUOg$q19jZL>d4%$76QxM|nkUYztH&+>7g z-Ay_pbyR{W2O^*O4X!ni-x{RX2h0CKZ8hwT`b7IFoY5>t>!oi0&X$q0XD51#9~J zzj0z}?a0*l$ja4I6Du39SsNNGa;h0bT8!}mdbXsAnNJJBan#!ZQq0;~7?e+<*PsFE zoCwwTJwe?NQ$%WlTVh(GNk2#`vTbX~z`-LcD_f5Pc+7l&cUi$HXYhD$YbIgYf?uwY zTKGv5J#|8AZf&w6TW_x`p|E)HmHecoSfipiEkpgR3b*Ls@a)_-rhEGBFW zGpolYZJJv%J(jf%<>?r+A>;YpggZ!*%uM1Ne+)OWE|=`&$>?rS(t)^@{=tnjvU3`RO70 z6bI0C8g@TD&Z#Q4lKv$m!-a|X;W|CM$J)OGYn`Ls)4;5Q>vtwPWVkzvZWlFD3 zP?Ku`<#>BM_;$*;*eVAvwt@!@1}{FKw4cMU7nx8aHMpNwB;s2rXy`MDn{THKjth)= zM>F^q14MT*S8ifFcyU9Bx1mRi^Ak2o2H$Fh5wrmC@1mkYKj}Egghn(##XeQLAlDKo ze4#iV3K@JWL~Vc6iox9hD*a!KK@VWHBF$c+yH2bxT+Ky*{NlRxbh~g14}Zq&FN!%x zoopj1x}J+l#oY4%s`mK+n=yA=5_8r(2q_1V)pdiM#8VIE4&sS=ywu0f%RvvyAN&H{ zBE}0h!h7Q7Ux?Z;=D#-Lyuhw?_9KZ2-dyX%GO{E+ZgBSl0A2i)-cFN0Fs;d zz!|(9eVBO{<64f{jD{})zje4rl|e{u@EWVkX(dKMkgk|lwb2PNS%!|+k|!Qsn)9Q& zVB6sC&~xJcUx391KV^l&;UYj`nfDyK2+lvs6SYSI0pFupNg&RsiRmd@oNl0PiAEXZ zdqqe9?qoW(Sb`Nb`1B$~egT(m#%ITxva zW1KOes2|XqqhW~u%IXIn26t*+<8<6%;2L+oP=%QrzsBU39JTX}R;j~{&02ViTd4TY zga+4HL9XUH!G|`o#%|NK?6+Bc18Z!7dp3b>cBe41g80QvfH!Wi<(+?3FaG|K-fPz~ z5$)%mO*H$C#yrr$Hk<$LpTfXFTnjt+?@;ucA*eRKDz9&H(hu08_n+kvz-+w`o#C0QSBa5)o(JQVzBXb)V1ss^&X-lAkh3>KS4NEr z9eQ%`-`FBP`rraQ+qLxJ>m;IVO+s~a3KP+X_NoVhGa*JIk2J+;9Tg2f>W?b9Itl#n$GB6^#T%9&cQUxSxFYD0|cr>JyOK{_apQmkTNT0;fZ66Y!69n|*=BZN-nh$`3 zT4(}(((G2&Q#3gv(D!Vjg9svV==uFxC~}XlMpGaX$Rbhb_CAD$III_d&wgl*TGX(R zaEH(^#MLMhZfdwcp$W_qKFfoCq_5{&v)hdc==}``ZjaJ%Ky~IZVCc|>n>|0sz!gq1 zn8W;xaH93A?Cu(WF0o^Y&U;jUn` z9>FsV9D1dB%qZ&8A8BRu#Wh@(tO&?Y2^yWqncwG_1s$r$x*mOKq^_Ew?jX~|VAnN_Hgu+s92mx%VsxE-b$)yY zkA{yjL{nO_E*fV=+Z)8zMT#$O*6N9wjw&RYW0IuOD)cU+Lxn)lSpz;qZ4pyzmeu5j zUabj$vh0}#%b+f0a2lF+cu9CQ6QydR4OOL z77hZJtu1JtXtZD?t|cLFl|%3JEklUXmpuHmvv^el9uLO1>GM{bYKen53rGHB?ghN-}F=#4(* zjoX!f3T8i+oF=^5@#vL?XL-iwH+wpy{APE8y6;OKhbPk~HQz6>_2dy6Dj}ktV47@D z$4YJVuS2_1;#mNd2e~6EglW|3Hf{!BmtWv%Vbsno#FskardDJjfAWf&vJP5L;m3|s zJ=Km^{Xghwh0~aYkyQ6jWY_RG)KY5+jd?yBI&j9TmpalV1pGF`;H8mrQ-BcSZIo|px z&oexW7CyI{oSGb&-muhJ$ zFYE`j*abXl)u6v_bYlIE&c}>qgKh})z~#sapsMqf)ZJ#=+&MT)hBlCcOQrwpA()+B zo-=@|Y_9&RgdFKGE7HK!OL!WG2Nyg}L#3=7ot_B~5)F{A7$BFNW5{{iM>FOtGbF}` zek1lv@qPO)HM}gFT0MPk@+<4T`blMQqb3UuP3hu86bTir z8zT5&fJ!YNiQtU@=kQg2%HfiW3@9`|OrL5>^3yOm;@yC!5d#XF-PhYi9M_C}G(MhH zN(Xi{dRc;S9$;zSd9+%=U31VtunuYQiv;u`Z1ysyg7m&kKiW&N<)}i9mw^B zYHzX1oG)RuZY8+T%HbDS5pVRJDXacU39B#XY2JH2(EFVAN|Sn?>iRyPjUHADiz zGfcMGC80&=+P2G#LvzZS+YOL#2Du;yYJM1`*bB55dBMJHSE-`bO{6L9k)%pS?wR92 zhnT}vhF@bTLQ+9a9y_eA_RQ}>6|_PdO;2?HLf&9>&K#d{#mHaLVP`x?%;qsd?3?qm zbHvF{*??z2!*K1}M}Anzc!RQIQpcLXsl8q~45ir1nULovRwz}rej34_0ptnM)_+Ct z0RxBm@tM}o0bV-a%KT42053;Yi#e#*JsY4Fy0~OIw3*f!#Q<3gpA*(E0%gkO83k}p z&cjNbFISX@dVSt+6r(<;8%}Ne0Gw=afXdY9^@BlUk3i973QVIb=#|dB8K}#Ft~Bv$ zTx&J+8-v_=px+ued=1F9erJVF$F+VB&<@1vLsi2cJOCNA^<^uZQWQD3Of(Y{Y)-^p zP1##lK~wq>j1XM>af{X#{on;_4>cnBVF!{ml7OC8#77p%EjPuHBoe}@VyK#D{oEcb zND#5oaQ=Z$g-B07v?DxjsR-<%x7ff7@*{Aq{7Pm}Tbx23wu?3s6?RB%_76XicO>v& zwy@S@IAF2nQeiretXM$wZex*?jL}alLw`&ngGLWX!%HDt8_JW>+pP$;0djh64*=wp z!c86rA|ABW)5el%_zn^qGH~dR`&$_|P>1g%-w-6jOVQ3vg2X=YCNn?0DKg^&{fBkR z>nZ3D0fz4cR0Vp8;wf;?JvBQ`L_L)Bg-DM=`We4n7;%@rX|G;`^`>wW%qO)Fl4d7o zM1!;#0FW9HgRwbI@6_ek)fxT@HA-1Cf{(LW8?F6o?-aqEBgi|mE)jM?t-xI)_=E^z zm7`SG-rd0b3Oj{6c9#9-Orm_CK*PgZ7ovQD74C7FLGF=5@6sV50O6gDIS%?79B}x% zpkQZ!ji>#3P0|I86DaNsJQ-;*#%x$U%aw#c^bX zkakWeaDBa=CfcJ(#%h+1(hgje>nH(0<>6#Qf{%|hBx;EorktvTf28*h7*f*GJpk8S zr{}YQ%v!9g}VK(GAy{gFbT(fLwEE_GB1r z@nJb9iXJ>a({K$>wh@J9Gbz}QNks}S4eV&}YK~;0NOGGXtfK=tp9>-8_5?9EmZ|WB zD7V2`nPd|xJepH8`t}`(m~?E)3F+jdXqj_3iX$T(R663mnQCm}P+lU61nwxLZ}~Uh zhG<=nTF!JrJrb9+ibBc<05X_=ti%vlw_#0f)9@&CbgM^$hObE$jq-Y%rEGl%pQ-La zaW$^B3E*Bo4w0Vky1+1`;p6-=69acIksIWO5}b-lcP{Ff3|d<%!)ZSgm`Vm%-f0oa z*L<}IZ9m&;wFqr52CingB?iqol@y)>@U*yiobytvXl+4w4D+^{=3_xO<52}CIl3}S zf|3O80%~|+`#7sh5o7u!-MMa&8pb+|6dh4g`J&=j@>&M`SaxvT6*JcQQ1JQlUhPvOw zQ$Q3bk*{9YpMa*%NC^`u_?oCF=AdjJ4UoIGZHVr`V*zR=J&vGdE}I6Bl!q5lf0v;e zicZ{@FGjd)Ybfw`goKcv7?FcTM28LNT*-V~f}Hut(u47lN#Y{NM6nF&RgdVNZpj5q z4y?;QkWyJVP9SQg8027UEHY4i92a}2l6$djrW|(7GBafIn1q=Gf}%tX zGz1^Wrws}|Q9%*gT0v_?0bB7=d{%;1B>~$?QG9~7KKR!E|KG2B?wtVrzWjdKv(DaY zueJ7i?S1yy=iCkJ#=BD!lk3Ja_b=Z(HF@s%^vrlxoR#Id)ml-k+^{Jd8=uIEGtb{R zepc4;4eZoGS*%|>Iz2s;6^7Q`ylzu=Zg)B>j^D6honaF#XU*#Ia~5ZztiFGLh z(ajD;k2VS-v!LJ|&tcfw@|>d_Kc|-hx)Hh21o&7KIl;LAJ54XNxL_dopRrY}JePf} zx^Ea6G^A1NlWkg^75#$%xy~Ud_eGJ&PdT1|N{Phw&cVdMm^`wV;PJrB!NqJbI&i4L z2$5k0LXV5r$Ky?GpMStTZ|Vv8kJN z@2;Ednj7D}wgAo)!*%tLW>a8Ck@>U>)e)?`XTI2jktByeA3AqZy9fQDZRL9UWgcxqd)qXcfyc zI_*+Wrvj8(aJh)CdmKQ8$8!NHJe~*e1Pa!Po~zLEG9GIvmiVNYi3#)=q!a}W8Y>hM zqF2+$E_yEO4`Ac-YbLt;;t-32`HcyZBkUAXrS;vSjCd5(- ze-SD~^;Ce8^)!HsrEq|y*YYWL;gkQC$(ctt$2vmY#sMq}9>F@&?7-H{tUf@T(|BVq zB4=8dEz;de)Gj)d!oC!6ru6s}!sK3p^7>6d{gw{d3)$Pm#J^)HARw8Qj=7e+#!xF> z%=rQtLB|r|Y<4rxmAq>Yp)7EPEL+R*%>^h?yy8|_jm0A*TeZQQySs6NGSzmUa$@#2 z(jbr>i|CN#i#1?SF(xR;gPeoYPg=F(A+PUKY+Vgyv=cQzqH{UQ4Pc_NZ;aqM081iF z1Kg=e`W1k)x%8z=0Lp6s1?i^jLJHV0t@y@*t7dZxN+)AX9TZA|$jMVeZ6rglIE4*CGb@ME$*B&OfDf|U~wY0 zD{YOtYJ*K#qpQyLS6>} zRAr3;krs)}T%wUlna$UaZj zpGEUOqPPjgr&;+afH$MK6~!$m$bWi#X2ZI3#}AL%P7H3=iV`TS(D4e2u??WCdr<^0 z26(#}TC>PbT#kAFdc9p(EFx3RY+gBoWV8ebncb?$*1^>+2;)>iFIAqJ4|Lkz616dr zwhODIy_5xr#7=8H>+QhE?H`g2nQsK8?516--)ZzK43 z0HwE&0Tk}v8RK#wkT8|~Z#h41Q40sMwcq_W6M6;}}B=h(KMcaZ_B z`cuJ8(SMtPZp!{b1iuLI)G)Knt&KNon++Xc2W5WVE^J1x-5g)QS#hic>gVhC#yel9 zR%^@0F&kq5$^MOZ@_1izDxDg{NKtg`tJ?i(i8Z#0W)y6XZH_e_dJ16KJOt!)vmTKvSor58%H2jUxMz<;p*6_82IV^`?|-3IOPBiqYDW4Iz{g1x zl-gux0LCaJ#|L!_vLBGr#T_n##6Pr)L}J^b_R~$i( zBq8T>zd)rd|H}wI0ECYQPn;V?tSK@`^KqBJPun5;-TXz#Z`i*any`!uu!6b6gG3Qg|*0MLVR@j~e% zGp&JHnS>{_pO+};qdD^zhm6iC{3sW~qUH!Su{AxUa}ggS}FC1qLI&n_99CI1R_z;KWbh9RPKFbAM? z@ECy7!9E7%cd^@JQTxd5iJ}fTTq**Z56LEP+eH}e_&J;Uw%L>pxxAK8%#4hi{0~6t zh8UzHxK7-TmL)&7ko{J#Xy`?2x$$$9MM65p8Um!U8&PnNT&sGq<+}Ms?bZnoTU1@( z_N^Qiu@Z%M`uy>BA;y+k2MrhlQV!<;dDis*+N|IMnTyj zwurG|YYc+OMh24HuSd@U!z_kG^3|vj39gyLS~uAsAgz}Iab#~I6T`2EizoDonyVE= zbPw@Q05gVdfeI>bb!KNtC#bVTWdTA3pIBt9$-V#dLu9Zz#-S-VYjS0=Z?$AXY%qUQjV5JyE2 z?26Ns1hoj6J6tRqomsu%yv*e;An&wX)Z;aU5y|KG&e)bd$%e{{{*PbjjnB`7!7w-P#d? z{ztx|7VnL)WN?;fFO1+RAU(s|n;dpAZ$Uwa3gC{#2tToZs(3Ngm4QsS_N9}0V}OTKj(O4w;q*aqa4v_Zj6%q z1vw`T$$JKB1yV?XXIf=(5p8`Iz>5iDPRQrQ0j+gYdzRSM?I$2mI3;RxZI4}Mik`Os zE1CPS-iexzKQ_ zh~7hIHOKY$CvvH9xtL1kBuFLu2T%D+jF^H7&)deg%<>rAG8O*eIrvIiGoN4>gq2hp zSwxWJ>?V*V=YDBE2Bs67@ZLFy%*dchsHXVfe3V?C!*JbAc9|8|i4;K;AF1^Zd9JwL zI;~7Q(V;3(p?OCD5xu^~W+j{Lu+OrU6F@9JBDL1ok6l)o_(azNMnTIcn;d-$WfpbX4)q$AHRwg?7Wll6IVJRw@vWO!@FX}6; z%`0Fz80X4vF0#MmhH!}9R#qK*@aeDkAo<5{_&0Omv1lwBRn4 zXsZ)u5@rr}(-V+PYSA{5qHWJVMLT&C`w*$_A=L=Vxs&S%Y7jIW7dkTBnnc)h_d;6i<5NvMwQ|CiIe-c}@2vRq}swylYmdd{x*P0C8PcTjfx7&4jqR*(@&Mn>voT$I+ zaf!u@<_r1uXHgl4i)PIi+Gze1nuE1$C9Vuqo=CHiK^Sqt1QZ#F0vV73xkLuyPX=ls zE5xqdNcd2yt0_EWq<)lxp(V#VYK>8ELow5XHPPs zd%{4gz`-pCh)$MdzTA)RB~eNZB8*f5(x|YNq!e%PBJXk>9OhaxU8%UJms+O0g+WME zIgp{JBl%QdsRgk#0fCkAqz+uhLDhV=oJKRJPaGN@JVjHNRE`Sz1l7iEM_GR>33=^o zjpLyrVgVAxdssMRw}vD^X$_=!#@J-y=4i4V#4$&=RZdxi9-1OQ12B<`%Q@Hq_2nfs zx!5rNJqPiH?hWB z2ph7Q_&DC0_8k9cM93d?TPX1ax>6-Z_)D!moJcQ1n#OLP$5F956$ z_G+suB>|LGVor3zYN($>MR3MV-OZblHx#5_Ae@0he7*$GtrG#BG2e-^1i4VJo({bHGF0onl~MaP)?UY21}~}g?o*q0 zb1v&yoQ2d~udT1*Vrm{h_>-1i-v)#KP0y~EOUV_0wCB|0%z$^Bi zs95++d3PL}d?;KOXM>PN6Fb$d5gf0)H<&2x>G}R3kZ`Tx+ASgjUtX7YgLz`$L3~pr zx<*h~`7`eYvuE(=2+aF(gdc-#;t0Q?7=94Hi9%8@uA`et>W-jR5ZIbZGk6}OG_i-I z`58Lb=98+jx>9m!^86mKw0qW}9xV0bf3v`c4s2+oB|CqRXOt7<@ zgB^XW_$`^}uT+$9ycYJdhM+vc7E>$pUjeMEVSm&~GB9Iy>RCbj9KDhlti7*C3ALb# zN?3s|Qo?@&OqB36HObc1)1ZWmOBmj*Bw2_VU!EKDl`4J8aQjv@B?-qXDNZ_m$040( zR)M{i0NHYb${!@eBFKP{Fa3@km@IxD!G{Pw9TaXLhywbknlN1cAGl6#1$$@mFs1a& zm@(t^Ro5qTpgQmD!yPo81AoAL?yGAPIt7v0`>03tLgAAm3h84%fKgE2d-ZX*C*Obb<&{AlQyJp% zB=UfB7Y~3No(!W(i|Jm^j0Wwoysuu@yYfTzAa@J(1Mp35KZNwv`LHj;AVg?p#}cGZ zxHMpu1#QQyRj@r#9`?Jdv;63eT?q7dTA?`H8OiNLrH&YI@sAs8c|mf&%N(!`m}A!5 z^T3~XJ#3<`(H(f??dV{d)@qb^B&H``<3QCbBZmRp22^dZRR&cgz;>N~;7WmW6847q z%Fo~>G>GLNJs5weKaP^;1d3;%Qc8Pf1TkOaABCFolUN%HiHl2$=$FL>;>hmhbf9bwi;(oK6n`L&OADGBa0>_eLUiYe+~O28X`n9xD7QJ)pz68> zrTwATa=*{H53m4Mp8#Yt=6U$b4M7H8wuPol4izwlKr6{<)n_!2`KYFl5}m`@Ln%)~ z)1LZ(xUA~RiMdIY1oCF{NDuZmJaN6dj01tV6>iI*| zXTB8l$zEAP;uz7r${VNDfj<|MVmrjdH^StRfCK(+c&l!BU<0b!2vUus4v(Ltw^qM1W*pJk1Mtg<(w z&>+jLV|5*hyQ$%>flk9K4Rjh_1(1sb?veWrZVtLm&IQk~SVKWYQsS_*y<12Sv>(Y& zRj;r%|0$ZO)!mhooA}~C{VL1RQ}gTD0CNt2E@E6{9vWhV%Q)XZoU|YncqhhazQDa& zd!ZKpmR_}Va=s;a|0g9vbFF_RNTD6OcXc{|6em1_N5!~T;yKpXH_;8SA&RD7G@i81> zaRQemHG$)1$PM{51~!hMb+!V04#C$Ms3&37t5ADXvp6jt|7{#KT+AGv<ZSbqK-O7=?EV}ew@fb)tB6Z z{KgAHk6jDU@adM7#SSa-rC{YIC5{l;wZQ~H7FfTBIl6IjFrU4+dipZEbk=%{fiA2r z2UbPh<&6Et%TR+1!1<{0GU))7_7IX9ACT+hrFcpyh|UZmh*cve;~?665{&i++s4We zsWne8-iAK(bmb;ohFST|cA*?Jv0=KqZr$i3(w22**M#ZR2^XysK zc5%FB*{J*Kk#42-Wh)Bm31^2#SK^_;ve8wj<-F8*4QJMX%MS(Q^XSI!1Cpkgt0VaS z2!0@fA2hIWA-i1*FnLm}Y5FkWLXgI5=Ub_#d6@f0SE423;!xWF#M++7<#P>J1t{{4 z6^%>KTSHOrc_3ulh|Ek3$b6~qy9eEtqS$w#mF`UzgBov0QJ54OZ>*yjo?6~iZ%Mf+ zqtsr$(edaJsHXqro0e4;*IUszg+=dm{Y+Tn4Tul!4vDH>RnZKbFNN>L4T{E_>@pjH zvKu=A?t$ppZWI*?=B9`CBG=yli#i{nT=BYgR;}@-Ue>OY^=`ba#+2le$tpeHLna^f zOr?=`VZ?FUuJJ}(?ttN^X!*u=Fc@S_W?fpn&)}ee(KkMV;_bb{v(ofdT3f-mkZ&fM z6Y0HZ?qk+hoAnQIP`rlEX1bR-2q28m_((5vEugu7UJd~X17O~DvF*moG^9AO_Qs_s zW(fy0y#WPOC+Ckt(X7Q=y?*CJr^|eBFyiQ>Z?*btJsLl>H#-0U`t6T5t90t$o9!eT zgDEvH$YLao&!M;(6yk84`UYDD_{dm|n^0Vf;zmZt^#;;q8}RVPCw)eKuU&=rRVRH? zPPU34CMmmQ+XeYd_n;xqYI?xVQpnw7#9N%?Jyg&EFvm4si(wW2fJ!B0Zf^?w$5_id zG}UsT47TF4hS2yn^-bT|gOO|35FFB^ya!g5&`cRh$`B#j2GmQ@RrwoJ`>5nzTel@p zk%IPO|Gs33KA60-KC}0vSxWron(38UK;i$OkeAkQ5HZ@(@AvkWH5GI!c)9%HEe8XP z(RvTAm48W!L2-rEHLk32LVD43_Z~FAw-)9S1TFV6hNQ!7ATr3=X9-*Mr(rqR9W@c6 zLaqVgwN_-dinh#2<2H7a8@(YhE>Lk)>i@S{p;?(VhO0t+5m;&%P%rbIT1vEh0R;FgqyMf4@v6_LD0Md#p{?bzG$FJ7+;Fumm~Nu z5xm{N2EJg2g(BdseAlXYFD{gd=(+S4+=rsNu^pw>_I?y!u$nLm9*D9ppgpSPEC^rd zmaK%~8+sOu)pI$@!Ewt<$?h9y7x>Kx{%ZukWuRN4Qau+gw2C2Q6*v`XFv2qWv6 zZ}XE-4U4M?p`{GE0}WyK>1)8U^ZMLA@MC|}vxa++1$i2GxM>3Lx2+g@DhChHjrcne z{I>{xH-g_YaOhd=c9(%R6(G0@cw7JQQHeLAM%@>xcS2JSqXYjUU2&)3_6`4kD*=J@W#wZ`{f5xg&gKZ@Xw4Qy;>xBCg!4b!sP;yQEy8~Syz4wr`o zXIIO1R5FZr($IG2IG=b{G`17uCbV95rOdc-ceh)d?CTCeB$DL4UT}yX8p(d8KB|C# zP`i?~(ilYLHbw*PHgqag@^e&5lRDzV+F!=n2O{{OfekH+)i z?0TU3x@gF_TB^}d(u`Wst&8HSIFowj&6M;^yx@&LGn)O1`(K69X;j5;A*B@by9mbP zG6nM*5lXc8gp!*IV9oweGS^@|XNTUY;5XI~Mu8`U7FPqtpfCwO=uT=L1*(ft@F+)F z0hE9Zf>>7-UuoG6B7hl`SWgUH>?9iEs%S6A3qZWW>kYCYKW#S{eH)1H^yn*bmGO~L zb`6C;1{Infc@5b$H}dF!j!>!{nAC6w5T=`+of|BMwAS7Z2!Xe^a}9`K;Mt(9-hdjF!JZD@4ZXliy-x-l$uT> z%RUYQ3H$>fT*Sq*d+uu$JQq21DWC9`RAc&x#VtX~#~P;FGlkdfR-S=oOvv5~ z>g26?=o41Zk$XH79ajeTbnZyA)5(}{Xuv*CgiQ2V*U2uO&-zjR9Sw&WwEsmHU?ULe zyb3Md0n6Li0x{@v2?xZ28$fhUrA4A+v6`ZLXR~$I!}!|YTF;>yDe@m0=nOh9f(IEm z^tUx%<6BHa`T$hF&6z8B=Y z0U{4^naz;l!``Cyt)`*x1F0tG5KmO=2X-LW5Eij4bf1`?Y}anlO}!}ifb{*^wR&Qh z$@IH`m?*x(QK>tT63T2sycI7DptHyTdeVAn=sZPQoWdlOzY!G_b?7_ZBb^gGj9Vra zm1FTBSP9vkhtha*iKkm-ak@Ozz@gnJexp1{;RpF9(4BAEPpX{5HcWvNNew{8K#Y@#(wA3{wy@3*CO_X&w zDy#V*RgM7GA#I%Nh5mUEGmG7C0>+}=LFF%IWfGzT%|z;Czi7U7XdZxGs4NbJ7m_0e zkg|-7*_%0f5oKM>1E0jzmk2kHCt}_L+I2BsipuoS#y~MO53qj}lm5ZqloChC34tBU zC?=3f7`ox~p414m4UU@V`NWA!2xb_awd=@$usOp{O?5hZ9cpx@F zx8g6w?p*-Nuk6lgJrRHct#BUMJX*O#lMIF$WK$Z}0|7Pkocc||x>g^(x2K`k75kf_ z&-AqQy2gN}V8foa#8d<7rNWRjC*mjF>$4_&hx;w*;aSZ&2$b?9v@20E#5H$vf0Leo z5N$36=JjEb(Lvm~9aqth?!%m-CtaAawS*pt?MysnLcnmE6ap>HW%ZVU^y!}5U&(e` zFD1hgP#RWAmJ$_fFTPkOsAUob#9D^5C{XhV$PyVeUx>@(lu7y&ZXi{PS^HXF^AzPc z-lJvpZ-Pq)O)$C&Malx#+fXpH;{JNJvp0D+mjP)fBx?RS!QOE&*V)1tO?^zFp~xyR z+#uG?WxcGG12F975#}xK_H0GnrjZG~0kPgZxsGI&1-25J>*_6aUDM^58PBYZw6y+Q zP&eU=P5Sb2y*SPFz}Y!i8+A_f6{RMQAv(;ItokP)R=27f#$XnPUU9OoS+zK`SG7%S zNNMk*xfx9A?oY8EnN@+>)CtNsf_1(8WJ+Qlm*km;S(r7Kfb_{2YWX57TxK~ng4l9s zE+MaRfG43iS*x)Vfi`G0c8XQI)tEb*Vs|cM_7iB+lPm3uXxJhLV>@{g&hoU1uU?F* ztdXPve@Ka&bQwdC&Lds$+8!=$VLvr+Byb)bYALy5QM%;)WdkGOfyUc9%_NSl1oBb+JPMWOZq zy7~YDAKnh*FXYrP^#qdn9{id*IzTytc@95K*%O=e8^MxV{X)_|XH9-?U*Gl6-rHBKmhS*49_(0|(=8lVJ9Dg%q@KPpa%f@{iSXKXQq>GaR`*#U z19AG%3&7ZcY2H<9@tbatSITzp*7PcS@99m-X1T`bB!?DRN4>*e-H~}-YkgKjCk~a3 z!8j9~k6MMyD*+}Z;5hI1D!Ok05I+r^kcZqW9jrsKBatWy%p=EIiO_IVy+zM?=n_vG zH-8azuM_l?KY3WZ$Iz?$Xh@nlacgwdNqrzSe{F?6X_IWmDggX=?oY;pE)OIEKNlhX_pT|_$dI~h1=@UZqs^oy* zL)KD#DLN3YTYqSUGeu+-U%j!$>H?7GteDY|*=G|>bcfKbdA)=+3CPA?Y5W2^C!NRx)IRIjlqvGUBJhzcOoe5&)zzi z$KGE87PRZW6@`hX`YEnE_P_NMqog&$gR=-o)~zGi!^ctJpKVF_gB~3weiN+q6svUX zd|KURRW3N}V~BdAv*)eF%uc~C2S2=vu!2Cto|jtKq=7&Tj#e`luAL>QhA zU4mBuY!Jlas&xwF*PAbwMnf>+VagsS$Li7rhUH!tGDx3!&DH>DKM3Jvk81#SrFr+@sX+%@Wc97HP47TxF$GnxiezId zwC3sqJ+E4{6wTOGZQkkGlY*W`(@`7Gw`N;xp`<6oyxXm&&!}|DZ;^68-Ry4n{ zz{>h$imJ=32oEG>6RZ>E1eY<3K`pqD4b-mJUEBu@cFB=e36s^wtlHhh4P57h8-Rhgaq@yeHewyu zHDlx)uA4u`wQd7GVUU}yK8aebY5oDAcH-x;){54ftY{(xT0AWoj~1#0X|j1gm+vKf zSYvIy5!L_Y9fETxd1MlbpEfFGGDfj<16hTJ>*kMraNKBDJrnz+ouqwq>u;)osUy0x z-*iPf%jdW&TCd5URVZ&lgJ$*580d`7yM(%$-bV(=!>x;~pt4(6b5@SJOpvg?64JE; zk!qp_>J=So417KWziYkK3QoSQ_u}%p9-R;U0Ie8bHYS~K11x;pTV&k5%yt8;?0*Y# zwJw6o&$1nM)WK+@c${#NaheaZlCw}JUWe@zi5jyYRU}q_#o!@1^1s@;x2^>_$}VdJ zNBFeW%Mn}v+b^>FR|L~sdA#A7xe&+m0U<0Kc$(k*2BZ1&s8lrH22iuq7Yu6M3f_FH z%y4xkq;=5()PXs-AzI9``hDgSaja@;HO@zUsR)wjEw??)4aFq8V#%uv=zm7I{Aa82 z&)e3y56Lefvdz(9Y)e_wJ4YXax_wbVo8IyOLuK<$yK?t}x1&XR;7x+`@Kw}mw*Hzy zt#83b+SYM>-MdOL<#UsTpI}o)r-tNrmXW7H&{+Bf7;Qd|O5kZV6}_X6f=>guZRA&s z?U$V=Hc#mT`-xtBJi`T%%_s1;aU^~i*ZwuXk*;QRl7LD{WDV-$-Kh-fUkNMkFe2d; z()cDk03~xIXd0z)MBo_-VKQj`2m!!R@dHH-2dyRa`qubb@7n2~SDw0C<5HKlt)7A$OEHDR$F z9T34HXd98UQ08Kz^+jN7{RoK9CCZ-~}NU1!yjc z5=EG_e_|JY(l(K2Ca2D}ACccMl}a9z<0KERpxsRAL$rNBXq%JH$T84?#hK~qSH{*2 z{ z8gB{R%;48Dd);1&;VfX-db3*hW6lVi68TbdkF~*#>!b>iBH61U)Y5~vLg|0^+M3(F z_iH$aq&3bCOd#z8L4v2`+PphWf&wkkeZ4s4+Bl;Xg4BO_%ywKN^tNnLL|!dV;z$j@~&27p#V@aQeae z+S&Fo2DXTPuNH;{I-c!9~ew^p%q*=woi>6;k#6i z=8*QOL~`Cyb?nODP0g&e-(p!`OE1BR=_BnW3>d)e69`fZ=9AKb%^XrIlZ~6_$&iD5 zqJd5e2N>wIfSrgopY8B9-}VW(ewn+!F`aM(5Y#6|KnzK{rDYNUw&M%`;R2+2mlx_T zFO;^==u9N18*_|+)2mct32%bF2m8MTS4#?4NH4CmH z+$Ml+m@D(3vHFa^+7^>7hd_1u8HbOLdw)f`EGBIXn^uoc*)+FqW;{c{^C*iU<3Zn~ zJ5iF%OyV1V(KfQ=N#6GBjD%cd1duFBh|Yq@cf((dTCNJJBZ#ojO5I>FZe9=4E>*!S zn&r@h`Ag~;ICThRFVu`edwU>3lLw8C!~xN#H~{-{7su^>P@Gd$Y^Ai9k_;Cnk{;LT zDL&R-4%U}O(JEZOHL?^bB3Y51;zNu3DgoJx9GS-JOASZl^OJzjPTxYM7|%zg&>@46 z&`!+uTMTG(&oxfd?d@>W)-Q=f6F!F^3QDg|NlR^Xmr+LClD98GC%8rXl9AGW7sK9Y zLX8NyA4MeM8!2e$(|$9MMxw}IoI$Sk8&Qz%F z>q~X}iS>ok^>#phaa|o|7jEI<51ak3Vh&O#F{kJ{4#asMUp*J?s(l{7K~Js zv*tFWZ0`rmxc|+tSo;RF zQSaLUg=OBcb`hMvYcEbGuD=SH$&8wq9?Pm^x}j7ZV5^|^UtpKc^-n~T7Oy7(l{-->*B_R0fr$(aLYSsq4Ft=3b;?U8wIVzjw2ARZ-}2q@?96(-F|yKZ53U)ROHTCLZRObcr2q02f0%d8YbDt&)9AD6@}-A^tOP z|2eqplx4~t2JYeR7pf;%b?s-F{F0;Rprcjllw-XX-r^Q2nobheSxK(8_+RA#ttQi7 zPuk3;T`hMPw8!ogMpqKQ_!!_Vo6Q;hJ9~SA^YP0X?!`2;pMNgV?1LKfLGUmX?ni(M z12H8y>_DQ^44P&>7D?P9>f@aB1GeN#Q7Mn0Q=ev+&Z$pFlbm{a1Xlp$CO~xtK&?Fg z6d)f%RA&O*LtXF{m4C#<20;YjIeKn-Kl_hzIdv@mfwMhGO%j>&*| zJS*~)$Bgvx1fi$ZcmgR7p);>W{;9ZT)(}yCoV@)2C_&mdZXIFZW~BssvNdN6jEJ7t zEJ{l|H%@sZ(#j?3p%6604@tjyc_c;NRqqo`0Zgtx6NNrhM+Y@5Vmny2bq+yu)S`w3DY+i&JROE( z!c7hLTeQ~(|7q z|Mt%%b}Z3(kLqu8%ZndO5C@FaI)vqY-?Cft~m=tDfbe zIn&`tSX}gz6+wl{+LX<^mAK^7ul;IrCpwo2oMJIkc1C+u(|H9*a)XF*eG1LkikKlxXG>?D(mV%+ZzQ*Q4Q_|K=k*uaF^rY9$Zi@3r9TRsO zk+K(4kkBJDg-}5bj62%2LZpy<=e%BbkaHy;wW6tDw9XnIIVc)HvGk=YNZ&PoP#uCJL2JUbWq zls9Qt{wbLKns1u$dd^8JMcA^TYaL8cKEK(W;JK_x9*1+ATzjO{e7upV&+thep`j8Y z>Iu@x26e0~ndWA!+2z4aK-FZo8K4j-n{MOIL+x6Ail@S;-Eu>GsiS>EC1YO}^NPYY ztJYKa)#Fr8J?E_cAN17uI`}8b8mJOV#hZ&n!zFuCCFes<%@VIftyJcuekc>M#=mI=hVg!+4ZUi`vQ4>`bN3O=>eJ-phE)m%m5wXp(?iS;~oo5 ztr=gnY4Y6goD%0Tj)w^0U`BQ$(*Wmy%bJi``qq0H6k>k{i zFm_XItmJrmM|q*)S+wxE)zpTm(V5NDUP^1}{JQDhxXGJdRQIgS{XWea!!k3tpJfj3 zM!6q&iL9Acb`aV7-^F%ita&(N(tQ%Ez~PF?sfo#{$xY|$o#izc80=GFcF%^}PJrPK zUHlmBWnmoF<_o(=Vi)k}sRsRx-O1^`gEEHK`cJTG`^UxTI) z)k8VjO8v2iV0MfdlS9^?k8-W*H6=q0!%rAOeKuErbVPaI$OKl>Iceo$udmBck6R!+ z;C1f!v^|+CPBjm;S{C*vHk_3ySQPi+G{BEmp3|G&b-}|HMA)>@2o!^p6yPE zuw(%_GSPT}I4abzZFs3Wpw+y}09FB#?0XCl1whWL-7|IyRei}namSJ%_1cJU4ZNw> zC^SY5ZN4?BR`~)nXmfr@KHtv|6926nMNAj&4%?b0}RPYel0UV>@Xw) zH2Q~T8x3{I2~N@O#)yGw=?Mh>!U<1Y51;6Vbc@wH%V9@jwS7)KNl60+l-Z$14G55( zYO0AZf3}vDL4Mo8cJdqKtrsNYcqM-z#rsSrZc^zLf-cp4R@hsL0C7HY_)vmhjo{Y| z)KN*jP^Hb|ZvbJOxZec01}?w@l*14m?>#C#;N>uBeGgD_9U><@{0yt0UX!nK(|Xc7 z{fCM`y3m_m^rvC2rSxI^3dzG$F<=-=F8iSllu*a;CMQXJ6_fW9P7vNyQILT=FQCk8 zKn%+cM#Qi_22an2V8gHG*|Q1>B^88=7dq20R(XB&qlmBeZgjihh4YuIXZpi}*$@+3 zJs9l#P8#jr#2lVxJQ!MU`|JS3y+S*5;-*LX0#;r$pUc!V@AptCulT-!t^Z{0U8r43 zaJPXv2v>m$4#Dc;zk?Bx;Ge`)dOH4@6c))zTm9VcPgr4a z8h~V{*atWTcA7A!+n^1Ir4;aCJ~ARbZL$cD?}!Lw!qkW`CFCc7nooX$)BeNa{ih|JW{_3)~No-v_IH0xaGj z6*)k39sUHM==5@=gs30Fj|@$BD-^$H`i)uNCW56Ph?-^HmGx1HE|TObV%_2gnA{Ys zg~2sIPPS5KtfW=hLTVEI86d}&xFeiSD`=Jz0FrU2DLf%{n)-PJe-Xi70=$K|4@B@m z1G8NIv)OZFAfDFB5{WAK<7A8ewA$aLR1Ed!`}`#bT9@?qR~XY zI5RR|M1l0^lm>8_2^&Ow`oJ+p^h9HEpkcB7Q|smTkQsX$H?Ipj1PVPLMo0myS&+31 ztbT8WCRK~a30&ZfgDwEvuv*p+s|x#8h!zY(ov<_ zVBnb2nWC!88BD)LZ_QG_1ITxlD;Qw-ejqgLzni5RIbiNRHwuG>e?kQC8vbc5203+* z<1j+Iy8M~I!X}-91`M>=k9Hd0`bha_Fe2|GNClQxM{78#}J3$J`sE@z>>9^e(aru!&mC1gk&<6y~iu>2&pKnL050up%2 zocyU9?#vAz3YoIqD3W%+`ih&R;=_EXO`3zOM{KU; zPVHYncRXH}4AW+&WryRldsI2qgN>H@u5D+5)hPv&L7X=nCTJ(;5R(DM`JOtN^K8SM z!=oqw8WieePj6~#9eq;&^Ij4n2v= zkLf0AY0e)*7)vjvMrt$7GD0Igrr){T#>ub-bOTT|cjOprJ=NeG=Tj{@ltR#-BFR&5 W=_jSe9J{a`pchPyojAE}Jo~@(;Cqt* diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index e07f201ae..79b3eee8d 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -583,6 +583,14 @@ expr parser_imp::parse_led_id(expr const & left) { } } +/** \brief Parse expr '==' expr. */ +expr parser_imp::parse_heq(expr const & left) { + auto p = pos(); + next(); + expr right = parse_expr(g_heq_precedence); + return save(mk_heq(left, right), p); +} + /** \brief Parse expr '->' expr. */ expr parser_imp::parse_arrow(expr const & left) { auto p = pos(); @@ -1087,6 +1095,7 @@ expr parser_imp::parse_led(expr const & left) { switch (curr()) { case scanner::token::Id: return parse_led_id(left); case scanner::token::Arrow: return parse_arrow(left); + case scanner::token::HEq: return parse_heq(left); case scanner::token::CartesianProduct: return parse_cartesian_product(left); case scanner::token::LeftParen: return mk_app_left(left, parse_lparen()); case scanner::token::IntVal: return mk_app_left(left, parse_nat_int()); @@ -1118,6 +1127,7 @@ unsigned parser_imp::curr_lbp() { } case scanner::token::Arrow : return g_arrow_precedence; case scanner::token::CartesianProduct: return g_cartesian_product_precedence; + case scanner::token::HEq: return g_heq_precedence; case scanner::token::LeftParen: case scanner::token::IntVal: case scanner::token::DecimalVal: case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder: return g_app_precedence; diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h index 4504f5264..9fe083ab9 100644 --- a/src/frontends/lean/parser_imp.h +++ b/src/frontends/lean/parser_imp.h @@ -311,6 +311,7 @@ private: pos_info const & p); expr parse_expr_macro(name const & id, pos_info const & p); expr parse_led_id(expr const & left); + expr parse_heq(expr const & left); expr parse_arrow(expr const & left); expr parse_cartesian_product(expr const & left); expr parse_lparen(); diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index e3ba8b2db..dc0a06698 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -21,6 +21,7 @@ static name g_type_name("Type"); static name g_pi_name("forall"); static name g_let_name("let"); static name g_in_name("in"); +static name g_heq_name("=="); static name g_arrow_name("->"); static name g_exists_name("exists"); static name g_Exists_name("Exists"); @@ -255,6 +256,8 @@ scanner::token scanner::read_b_symbol(char prev) { return token::Arrow; else if (m_name_val == g_cartesian_product) return token::CartesianProduct; + else if (m_name_val == g_heq_name) + return token::HEq; else return token::Id; } @@ -476,6 +479,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) { case scanner::token::Show: out << "show"; break; case scanner::token::By: out << "by"; break; case scanner::token::Ellipsis: out << "..."; break; + case scanner::token::HEq: out << "=="; break; case scanner::token::Eof: out << "EOF"; break; } return out; diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index f7e9ce2bf..1c5e0af23 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -20,7 +20,7 @@ class scanner { public: enum class token { LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow, - Sig, Tuple, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder, + HEq, Sig, Tuple, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder, Have, Show, By, ScriptBlock, Ellipsis, CartesianProduct, Eof }; protected: diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 41e17e089..59739ca2a 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -8,7 +8,6 @@ Released under Apache 2.0 license as described in the file LICENSE. namespace lean { MK_CONSTANT(TypeU, name("TypeU")); MK_CONSTANT(Bool, name("Bool")); -MK_CONSTANT(heq2_fn, name("heq2")); MK_CONSTANT(hrefl_fn, name("hrefl")); MK_CONSTANT(eq_fn, name("eq")); MK_CONSTANT(refl_fn, name("refl")); @@ -83,6 +82,7 @@ MK_CONSTANT(eqf_intro_fn, name("eqf_intro")); MK_CONSTANT(a_neq_a_fn, name("a_neq_a")); MK_CONSTANT(eq_id_fn, name("eq_id")); MK_CONSTANT(iff_id_fn, name("iff_id")); +MK_CONSTANT(heq_id_fn, name("heq_id")); MK_CONSTANT(neq_elim_fn, name("neq_elim")); MK_CONSTANT(neq_to_not_eq_fn, name("neq_to_not_eq")); MK_CONSTANT(left_comm_fn, name("left_comm")); @@ -188,15 +188,20 @@ MK_CONSTANT(non_surjective_fn, name("non_surjective")); MK_CONSTANT(ind, name("ind")); MK_CONSTANT(infinity, name("infinity")); MK_CONSTANT(pairext_fn, name("pairext")); -MK_CONSTANT(TypeM, name("TypeM")); MK_CONSTANT(cast_fn, name("cast")); MK_CONSTANT(cast_heq_fn, name("cast_heq")); +MK_CONSTANT(hsubst_fn, name("hsubst")); MK_CONSTANT(hsymm_fn, name("hsymm")); MK_CONSTANT(htrans_fn, name("htrans")); MK_CONSTANT(hcongr_fn, name("hcongr")); MK_CONSTANT(hfunext_fn, name("hfunext")); +MK_CONSTANT(hpiext_fn, name("hpiext")); +MK_CONSTANT(hsigext_fn, name("hsigext")); MK_CONSTANT(hallext_fn, name("hallext")); MK_CONSTANT(hsfunext_fn, name("hsfunext")); +MK_CONSTANT(heq_congr_fn, name("heq_congr")); +MK_CONSTANT(hheq_congr_fn, name("hheq_congr")); +MK_CONSTANT(type_eq_fn, name("type_eq")); MK_CONSTANT(cast_eq_fn, name("cast_eq")); MK_CONSTANT(cast_trans_fn, name("cast_trans")); MK_CONSTANT(cast_pull_fn, name("cast_pull")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index eddc52f67..f7a85b83c 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -9,10 +9,6 @@ expr mk_TypeU(); bool is_TypeU(expr const & e); expr mk_Bool(); bool is_Bool(expr const & e); -expr mk_heq2_fn(); -bool is_heq2_fn(expr const & e); -inline bool is_heq2(expr const & e) { return is_app(e) && is_heq2_fn(arg(e, 0)) && num_args(e) == 5; } -inline expr mk_heq2(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq2_fn(), e1, e2, e3, e4}); } expr mk_hrefl_fn(); bool is_hrefl_fn(expr const & e); inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); } @@ -237,6 +233,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_heq_id_fn(); +bool is_heq_id_fn(expr const & e); +inline expr mk_heq_id_th(expr const & e1, expr const & e2) { return mk_app({mk_heq_id_fn(), e1, e2}); } expr mk_neq_elim_fn(); bool is_neq_elim_fn(expr const & e); inline expr mk_neq_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_neq_elim_fn(), e1, e2, e3, e4}); } @@ -551,8 +550,6 @@ bool is_infinity(expr const & e); expr mk_pairext_fn(); bool is_pairext_fn(expr const & e); inline expr mk_pairext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_pairext_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_TypeM(); -bool is_TypeM(expr const & e); expr mk_cast_fn(); bool is_cast_fn(expr const & e); inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; } @@ -560,6 +557,9 @@ inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr cons expr mk_cast_heq_fn(); bool is_cast_heq_fn(expr const & e); inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); } +expr mk_hsubst_fn(); +bool is_hsubst_fn(expr const & e); +inline expr mk_hsubst_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_hsubst_fn(), e1, e2, e3, e4, e5, e6, e7}); } expr mk_hsymm_fn(); bool is_hsymm_fn(expr const & e); inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); } @@ -572,12 +572,27 @@ inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr expr mk_hfunext_fn(); bool is_hfunext_fn(expr const & e); inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_hpiext_fn(); +bool is_hpiext_fn(expr const & e); +inline expr mk_hpiext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hpiext_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_hsigext_fn(); +bool is_hsigext_fn(expr const & e); +inline expr mk_hsigext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsigext_fn(), e1, e2, e3, e4, e5, e6}); } expr mk_hallext_fn(); bool is_hallext_fn(expr const & e); inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); } expr mk_hsfunext_fn(); bool is_hsfunext_fn(expr const & e); inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_heq_congr_fn(); +bool is_heq_congr_fn(expr const & e); +inline expr mk_heq_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_heq_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_hheq_congr_fn(); +bool is_hheq_congr_fn(expr const & e); +inline expr mk_hheq_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_hheq_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); } +expr mk_type_eq_fn(); +bool is_type_eq_fn(expr const & e); +inline expr mk_type_eq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_type_eq_fn(), e1, e2, e3, e4, e5}); } expr mk_cast_eq_fn(); bool is_cast_eq_fn(expr const & e); inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); } diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index bb8924620..98f86b5f8 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -100,6 +100,8 @@ level const & _lift_of(level const & l) { return is_lift(l) ? lift_of(l) : l unsigned _lift_offset(level const & l) { return is_lift(l) ? lift_offset(l) : 0; } void push_back(buffer & ls, level const & l) { + if (l.is_bottom()) + return; for (unsigned i = 0; i < ls.size(); i++) { if (_lift_of(ls[i]) == _lift_of(l)) { if (_lift_offset(ls[i]) < _lift_offset(l)) @@ -114,7 +116,10 @@ level max_core(unsigned sz1, level const * ls1, unsigned sz2, level const * ls2) buffer new_lvls; std::for_each(ls1, ls1 + sz1, [&](level const & l) { push_back(new_lvls, l); }); std::for_each(ls2, ls2 + sz2, [&](level const & l) { push_back(new_lvls, l); }); - if (new_lvls.size() == 1) + unsigned sz = new_lvls.size(); + if (sz == 0) + return level(); + else if (sz == 1) return new_lvls[0]; else return max_core(new_lvls.size(), new_lvls.data()); diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index c080eedb1..aca4e8ca9 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -375,7 +375,7 @@ class elaborator::imp { } /** - \brief Push a new equality constraint new_ctx |- new_a == new_b into the active_cnstrs using + \brief Push a new equality constraint new_ctx |- new_a ≈ new_b into the active_cnstrs using justification \c new_jst. */ void push_new_eq_constraint(cnstr_list & active_cnstrs, @@ -482,7 +482,7 @@ class elaborator::imp { } /** - Process ctx |- a == b and ctx |- a << b when: + Process ctx |- a ≈ b and ctx |- a << b when: 1- \c a is an assigned metavariable 2- \c a is a unassigned metavariable without a metavariable context. 3- \c a is a unassigned metavariable of the form ?m[lift:s:n, ...], and \c b does not have @@ -521,9 +521,9 @@ class elaborator::imp { // Let ctx be of the form // [ce_{m-1}, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0] // Then, we reduce - // [ce_{m-1}, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0] |- ?m[lift:s:n] == b + // [ce_{m-1}, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0] |- ?m[lift:s:n] ≈ b // to - // [ce_{m-1}, ..., ce_{s+n}, lower(ce_{s-1}, n, n), ..., lower(ce_0, s + n - 1, n)] |- ?m == lower(b, s + n, n) + // [ce_{m-1}, ..., ce_{s+n}, lower(ce_{s-1}, n, n), ..., lower(ce_0, s + n - 1, n)] |- ?m ≈ lower(b, s + n, n) // // Remark: we have to check if the lower operations are applicable using the operation has_free_var. // @@ -869,21 +869,21 @@ class elaborator::imp { } /** - \brief Return true iff ctx |- a == b is a "simple" higher-order matching constraint. By simple, we mean + \brief Return true iff ctx |- a ≈ b is a "simple" higher-order matching constraint. By simple, we mean 1) a constraint of the form - ctx |- (?m x1 ... xn) == c where c is closed + ctx |- (?m x1 ... xn) ≈ c where c is closed The constraint is solved by assigning ?m to (fun x1 ... xn, c). The arguments may contain duplicate occurrences of variables. 2) a constraint of the form - ctx |- (?m x1 ... xn) == (f x1 ... xn) where f does not contain x1 ... xn, and x1 ... xn are distinct + ctx |- (?m x1 ... xn) ≈ (f x1 ... xn) where f does not contain x1 ... xn, and x1 ... xn are distinct The constraint is solved by assigning ?m to f OR ?m to (fun x1 ... xn, f x1 ... xn) */ bool process_simple_ho_match(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { // Solve constraint of the form - // ctx |- (?m x) == c + // ctx |- (?m x) ≈ c // using imitation bool eq_closed = is_simple_ho_match_closed(ctx, a, b, is_lhs, c); bool eq_app = is_simple_ho_match_app(ctx, a, b, is_lhs, c); @@ -966,7 +966,7 @@ class elaborator::imp { expr f_b = arg(b, 0); unsigned num_b = num_args(b); // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), f_b (h_1 x_1 ... x_{num_a}) ... (h_{num_b} x_1 ... x_{num_a}) - // New constraints (h_i a_1 ... a_{num_a}) == arg(b, i) + // New constraints (h_i a_1 ... a_{num_a}) ≈ arg(b, i) buffer imitation_args; // arguments for the imitation imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1, new_state.m_menv)); for (unsigned i = 1; i < num_b; i++) { @@ -979,8 +979,8 @@ class elaborator::imp { // Imitation for lambdas, Pis, and Sigmas // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), // fun (x_b : (?h_1 x_1 ... x_{num_a})), (?h_2 x_1 ... x_{num_a} x_b) - // New constraints (h_1 a_1 ... a_{num_a}) == abst_domain(b) - // (h_2 a_1 ... a_{num_a} x_b) == abst_body(b) + // New constraints (h_1 a_1 ... a_{num_a}) ≈ abst_domain(b) + // (h_2 a_1 ... a_{num_a} x_b) ≈ abst_body(b) expr h_1 = new_state.m_menv->mk_metavar(ctx); context new_ctx = extend(ctx, abst_name(b), abst_domain(b)); expr h_2 = new_state.m_menv->mk_metavar(extend(ctx, abst_name(b), abst_domain(b))); @@ -994,6 +994,13 @@ class elaborator::imp { mk_app(update_app(lift_free_vars(a, 1), 0, h_2), mk_var(0)), abst_body(b), new_assumption); imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_h_vars(h_1), mk_app_vars(add_lift(h_2, 1, num_a - 1), num_a))); } + } else if (is_heq(b)) { + // Imitation for heterogeneous equality + expr h_1 = new_state.m_menv->mk_metavar(ctx); + expr h_2 = new_state.m_menv->mk_metavar(ctx); + push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), heq_lhs(b), new_assumption); + push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), heq_rhs(b), new_assumption); + imitation = mk_lambda(arg_types, mk_heq(mk_app_h_vars(h_1), mk_app_h_vars(h_2))); } else if (is_pair(b)) { // Imitation for dependent pairs expr h_f = new_state.m_menv->mk_metavar(ctx); @@ -1072,7 +1079,7 @@ class elaborator::imp { /** \brief Collect possible solutions for ?m given a constraint of the form - ctx |- ?m[lctx] == b + ctx |- ?m[lctx] ≈ b where b is a Constant, Type, Value or Variable. We only need the local context \c lctx and \c b for computing the set of possible solutions. @@ -1080,23 +1087,23 @@ class elaborator::imp { We may have more than one solution. Here is an example: - ?m[inst:3:b, lift:1:1, inst:2:b] == b + ?m[inst:3:b, lift:1:1, inst:2:b] ≈ b The possible solutions is the set of solutions for - 1- ?m[lift:1:1, inst:2:b] == #3 - 2- ?m[lift:1:1, inst:2:b] == b + 1- ?m[lift:1:1, inst:2:b] ≈ #3 + 2- ?m[lift:1:1, inst:2:b] ≈ b The solutions for constraints 1 and 2 are the solutions for - 1.1- ?m[inst:2:b] == #2 - 2.1- ?m[inst:2:b] == b + 1.1- ?m[inst:2:b] ≈ #2 + 2.1- ?m[inst:2:b] ≈ b And 1.1 has two possible solutions - 1.1.1 ?m == #3 - 1.1.2 ?m == b + 1.1.1 ?m ≈ #3 + 1.1.2 ?m ≈ b And 2.1 has also two possible solutions - 2.1.1 ?m == #2 - 2.1.2 ?m == b + 2.1.1 ?m ≈ #2 + 2.1.2 ?m ≈ b Thus, the resulting set of solutions is {#3, b, #2} */ @@ -1143,7 +1150,7 @@ class elaborator::imp { /** \brief Solve a constraint of the form - ctx |- a == b + ctx |- a ≈ b where a is of the form ?m[...] i.e., metavariable with a non-empty local context. b is an abstraction @@ -1217,7 +1224,7 @@ class elaborator::imp { } /** \brief Solve a constraint of the form - ctx |- a == b + ctx |- a ≈ b where a is of the form ?m[...] i.e., metavariable with a non-empty local context. b is a pair projection. @@ -1244,7 +1251,7 @@ class elaborator::imp { /** \brief Solve a constraint of the form - ctx |- a == b + ctx |- a ≈ b where a is of the form ?m[...] i.e., metavariable with a non-empty local context. b is a dependent pair @@ -1272,19 +1279,46 @@ class elaborator::imp { } /** - \brief Process a constraint ctx |- a == b where \c a is of the form ?m[(inst:i t), ...]. + \brief Solve a constraint of the form + ctx |- a ≈ b + where + a is of the form ?m[...] i.e., metavariable with a non-empty local context. + b is a heterogeneous equality + + We solve the constraint by assigning a to an abstraction with fresh metavariables. + */ + void imitate_heq(expr const & a, expr const & b, unification_constraint const & c) { + lean_assert(is_metavar(a)); + lean_assert(is_heq(b)); + lean_assert(!is_assigned(a)); + lean_assert(has_local_context(a)); + // imitate + push_active(c); + // a <- ?h_1 == ?h_2 + // ?h_i are in the same context where 'a' was defined + expr m = mk_metavar(metavar_name(a)); + context ctx_m = m_state.m_menv->get_context(m); + expr h_1 = m_state.m_menv->mk_metavar(ctx_m); + expr h_2 = m_state.m_menv->mk_metavar(ctx_m); + expr imitation = mk_heq(h_1, h_2); + justification new_jst(new imitation_justification(c)); + push_new_constraint(true, ctx_m, m, imitation, new_jst); + } + + /** + \brief Process a constraint ctx |- a ≈ b where \c a is of the form ?m[(inst:i t), ...]. We perform a "case split", - Case 1) ?m[...] == #i and t == b (for constants, variables, values and Type) + Case 1) ?m[...] ≈ #i and t ≈ b (for constants, variables, values and Type) Case 2) imitate b */ bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { // This method is miss some cases. In particular the local context of \c a contains metavariables. // - // (f#2 #1) == ?M2[i:1 ?M1] + // (f#2 #1) ≈ ?M2[i:1 ?M1] // // A possible solution for this constraint is: - // ?M2 == #1 - // ?M1 == f#2 #1 + // ?M2 ≈ #1 + // ?M1 ≈ f#2 #1 // // TODO(Leo): consider the following alternative design: We do NOT use approximations, since it is quite // hard to understand what happened when they do not work. Instead, we rely on user provided plugins @@ -1332,6 +1366,9 @@ class elaborator::imp { } else if (is_proj(b)) { imitate_proj(a, b, c); return true; + } else if (is_heq(b)) { + imitate_heq(a, b, c); + return true; } else if (is_pair(b)) { imitate_pair(a, b, c); return true; @@ -1341,7 +1378,7 @@ class elaborator::imp { } /** - \brief Process a constraint of the form ctx |- ?m[lift, ...] == b where \c b is an abstraction. + \brief Process a constraint of the form ctx |- ?m[lift, ...] ≈ b where \c b is an abstraction. That is, \c b is a Pi or Lambda. In both cases, ?m must have the same kind. We just add a new assignment that forces ?m to have the corresponding kind. @@ -1407,7 +1444,7 @@ class elaborator::imp { } /** - \brief Return true iff the current queue has a max constraint of the form ctx |- max(L1, L2) == a. + \brief Return true iff the current queue has a max constraint of the form ctx |- max(L1, L2) ≈ a. \pre is_metavar(a) */ @@ -1433,7 +1470,7 @@ class elaborator::imp { // We approximate and only consider the most useful ones. // // Remark: we only consider \c a if the queue does not have a constraint - // of the form ctx |- max(L1, L2) == a. + // of the form ctx |- max(L1, L2) ≈ a. // If it does, we don't need to guess. We wait \c a to be assigned // and just check if the upper bound is satisfied. // @@ -1505,7 +1542,7 @@ class elaborator::imp { We replace ctx | ?m << Pi(x : A, B) with - ctx |- ?m == Pi(x : A, ?m1) + ctx |- ?m ≈ Pi(x : A, ?m1) ctx, x : A |- ?m1 << B */ void process_metavar_conv_pi(unification_constraint const & c, expr const & m, expr const & pi, bool is_lhs) { @@ -1520,15 +1557,15 @@ class elaborator::imp { expr m1 = m_state.m_menv->mk_metavar(new_ctx); justification new_jst(new destruct_justification(c)); - // Add ctx, x : A |- ?m1 << B when is_lhs == true, - // and ctx, x : A |- B << ?m1 when is_lhs == false + // Add ctx, x : A |- ?m1 << B when is_lhs ≈ true, + // and ctx, x : A |- B << ?m1 when is_lhs ≈ false expr lhs = m1; expr rhs = abst_body(pi); if (!is_lhs) swap(lhs, rhs); push_new_constraint(false, new_ctx, lhs, rhs, new_jst); - // Add ctx |- ?m == Pi(x : A, ?m1) + // Add ctx |- ?m ≈ Pi(x : A, ?m1) push_new_eq_constraint(ctx, m, update_abstraction(pi, abst_domain(pi), m1), new_jst); } @@ -1577,10 +1614,10 @@ class elaborator::imp { if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0) && !is_metavar(arg(a, 0))) { // If m_assume_injectivity is true, we apply the following rule - // ctx |- (f a1 a2) == (f b1 b2) - // ===> - // ctx |- a1 == b1 - // ctx |- a2 == b2 + // ctx |- (f a1 a2) ≈ (f b1 b2) + // ==> + // ctx |- a1 ≈ b1 + // ctx |- a2 ≈ b2 justification new_jst(new destruct_justification(c)); for (unsigned i = 1; i < num_args(a); i++) push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst); @@ -1800,14 +1837,14 @@ class elaborator::imp { return true; } if (lhs1 == rhs) { - // ctx |- max(lhs1, lhs2) == rhs + // ctx |- max(lhs1, lhs2) ≈ rhs // ==> IF lhs1 = rhs // ctx |- lhs2 << rhs justification new_jst(new normalize_justification(c)); push_active(mk_convertible_constraint(get_context(c), lhs2, rhs, new_jst)); return true; } else if (lhs2 == rhs && is_type(lhs2)) { - // ctx |- max(lhs1, lhs2) == rhs IF lhs2 is a Type + // ctx |- max(lhs1, lhs2) ≈ rhs IF lhs2 is a Type // ==> IF lhs1 = rhs // ctx |- lhs2 << rhs diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 9d8628cf0..6a2ec989d 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -193,14 +193,6 @@ class simplifier_cell::imp { } }; - static bool is_heq(expr const & e) { - return is_heq2(e); - } - - static expr mk_heq(expr const & A, expr const & B, expr const & a, expr const & b) { - return mk_heq2(A, B, a, b); - } - static expr mk_lambda(name const & n, expr const & d, expr const & b) { return ::lean::mk_lambda(n, d, b); } @@ -239,15 +231,10 @@ class simplifier_cell::imp { type A is convertible to B, but not definitionally equal. */ expr translate_eq_proof(expr const & A, expr const & a, expr const & b, expr const & H, expr const & B) { - if (A != B) { - return mk_subst_th(A, a, b, mk_lambda(g_x, A, mk_eq(B, a, mk_var(0))), mk_refl_th(B, a), H); - } else { + if (A != B) + return mk_to_eq_th(B, a, b, mk_to_heq_th(A, a, b, H)); + else return H; - } - } - - expr translate_eq_typem_proof(expr const & a, result const & b) { - return translate_eq_proof(infer_type(a), a, b.m_expr, get_proof(b), mk_TypeM()); } expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) { @@ -309,78 +296,22 @@ class simplifier_cell::imp { // the following two arguments are used only for invoking the simplifier monitor expr const & e, unsigned i) { expr const & A = abst_domain(f_type); - if (is_TypeU(A)) { - if (!is_definitionally_equal(f, new_f)) { - if (m_monitor) - m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::Unsupported); - return none_expr(); // can't handle - } - // The congruence axiom cannot be used in this case. - // Type problem is that we would need provide a proof of (@eq (Type U) a new_a.m_expr), - // and (Type U) has type (Type U+1) the congruence axioms expect arguments from - // (Type U). We address this issue by using the following trick: - // - // We have - // f : Pi x : (Type U), B x - // a : (Type i) s.t. U > i - // a' : (Type i) where a' := new_a.m_expr - // H : a = a' where H := new_a.m_proof - // - // Then a proof term for (@heq (B a) (B a') (f a) (f a')) is - // - // @subst (Type i) a a' (fun x : (Type i), (@heq (B a) (B x) (f a) (f x))) (@hrefl (B a) (f a)) H - expr a_type = infer_type(a); - if (!is_convertible(a_type, A)) { - if (m_monitor) - m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::TypeMismatch); - return none_expr(); // can't handle - } - expr a_prime = new_a.m_expr; - expr H = get_proof(new_a); - if (new_a.is_heq_proof()) - H = mk_to_eq_th(a_type, a, a_prime, H); - expr Ba = instantiate(abst_body(f_type), a); - expr Ba_prime = instantiate(abst_body(f_type), a_prime); - expr Bx = abst_body(f_type); - expr fa = new_f(a); - expr fx = new_f(Var(0)); - expr result = mk_subst_th(a_type, a, a_prime, - mk_lambda(g_x, a_type, mk_heq(Ba, Bx, fa, fx)), - mk_hrefl_th(Ba, fa), - H); - return some_expr(result); - } else { - expr const & new_A = abst_domain(new_f_type); - expr a_type = infer_type(a); - expr new_a_type = infer_type(new_a.m_expr); - if (!is_convertible(new_a_type, new_A)) { - if (m_monitor) - m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::TypeMismatch); - return none_expr(); // failed - } - expr Heq_a = get_proof(new_a); - bool is_heq_proof = new_a.is_heq_proof(); - if (!is_definitionally_equal(A, a_type)|| !is_definitionally_equal(new_A, new_a_type)) { - if (is_heq_proof) { - if (is_definitionally_equal(a_type, new_a_type) && is_definitionally_equal(A, new_A)) { - Heq_a = mk_to_eq_th(a_type, a, new_a.m_expr, Heq_a); - is_heq_proof = false; - } else { - if (m_monitor) - m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::Unsupported); - return none_expr(); // we don't know how to handle this case - } - } - Heq_a = translate_eq_proof(a_type, a, new_a.m_expr, Heq_a, A); - } - if (!is_heq_proof) - Heq_a = mk_to_heq_th(A, a, new_a.m_expr, Heq_a); - return some_expr(::lean::mk_hcongr_th(A, - new_A, - mk_lambda(f_type, abst_body(f_type)), - mk_lambda(new_f_type, abst_body(new_f_type)), - f, new_f, a, new_a.m_expr, Heq_f, Heq_a)); + expr const & new_A = abst_domain(new_f_type); + expr a_type = infer_type(a); + expr new_a_type = infer_type(new_a.m_expr); + if (!is_convertible(new_a_type, new_A)) { + if (m_monitor) + m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::TypeMismatch); + return none_expr(); // failed } + expr Heq_a = get_proof(new_a); + if (!new_a.is_heq_proof()) + Heq_a = mk_to_heq_th(a_type, a, new_a.m_expr, Heq_a); + return some_expr(::lean::mk_hcongr_th(A, + new_A, + mk_lambda(f_type, abst_body(f_type)), + mk_lambda(new_f_type, abst_body(new_f_type)), + f, new_f, a, new_a.m_expr, Heq_f, Heq_a)); } /** @@ -489,7 +420,7 @@ class simplifier_cell::imp { if (!res_a.is_heq_proof()) { Hec = ::lean::mk_htrans_th(B, A, A, e, a, c, update_app(e, 0, mk_cast_heq_fn()), // cast A B H a == a - mk_to_heq_th(B, a, c, Hac)); // a == c + mk_to_heq_th(infer_type(a), a, c, Hac)); // a == c } else { Hec = ::lean::mk_htrans_th(B, A, infer_type(c), e, a, c, update_app(e, 0, mk_cast_heq_fn()), // cast A B H a == a @@ -540,7 +471,10 @@ class simplifier_cell::imp { void ensure_heterogeneous(expr const & lhs, result & rhs) { if (!rhs.is_heq_proof()) { - rhs.m_proof = mk_to_heq_th(infer_type(lhs), lhs, rhs.m_expr, get_proof(rhs)); + if (!rhs.m_proof) + rhs.m_proof = mk_hrefl_th(infer_type(lhs), lhs); + else + rhs.m_proof = mk_to_heq_th(infer_type(lhs), lhs, rhs.m_expr, *rhs.m_proof); rhs.m_heq_proof = true; } } @@ -1141,7 +1075,7 @@ class simplifier_cell::imp { if (res_bi.is_heq_proof()) { lean_assert(m_use_heq); // Using - // theorem hsfunext {A : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : + // theorem hsfunext {A : Type U+1} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : // (∀ x, f x == f' x) → f == f' expr new_proof = mk_hsfunext_th(d, // A mk_lambda(e, infer_type(abst_body(e))), // B @@ -1153,7 +1087,7 @@ class simplifier_cell::imp { } else { expr body_type = infer_type(abst_body(e)); // Using - // axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g + // axiom funext {A : Type U} {B : A → Type U} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g expr new_proof = mk_funext_th(d, mk_lambda(e, body_type), e, new_e, mk_lambda(e, abstract(*res_bi.m_proof, fresh_const))); return rewrite_lambda(e, result(new_e, new_proof)); @@ -1175,7 +1109,7 @@ class simplifier_cell::imp { // d and new_d are only provably equal, so we need to use hfunext expr x_old = mk_fresh_const(d); expr x_new = mk_fresh_const(new_d); - expr x_old_eq_x_new = mk_heq(d, new_d, x_old, x_new); + expr x_old_eq_x_new = mk_heq(x_old, x_new); expr H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new); expr bi = instantiate(abst_body(e), x_old); result res_bi = simplify_remapping_constant(bi, x_old, x_new, H_x_old_eq_x_new); @@ -1189,21 +1123,18 @@ class simplifier_cell::imp { expr new_e = update_lambda(e, new_d, abstract(new_bi, x_new)); if (!m_proofs_enabled) return rewrite(e, result(new_e)); - ensure_homogeneous(d, res_d); + ensure_heterogeneous(d, res_d); ensure_heterogeneous(bi, res_bi); // Using - // axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : - // A = A' → (∀ x x', x == x' → f x == f' x') → f == f' - // Remark: the argument with type A = A' is actually @eq TypeM A A', - // so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof - expr d_eq_new_d_proof = translate_eq_typem_proof(d, res_d); + // axiom hfunext {A A' : Type U+1} {B : A → Type U+1} {B' : A' → Type U+1} {f : ∀ x, B x} {f' : ∀ x, B' x} : + // A == A' → (∀ x x', x == x' → f x == f' x') → f == f' expr new_proof = mk_hfunext_th(d, // A new_d, // A' Fun(x_old, d, infer_type(bi)), // B Fun(x_new, new_d, infer_type(new_bi)), // B' e, // f new_e, // f' - d_eq_new_d_proof, // A = A' + *res_d.m_proof, // A == A' // fun (x_old : d) (x_new : new_d) (H : x_old == x_new), bi == new_bi mk_lambda(abst_name(e), d, mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), @@ -1379,8 +1310,8 @@ class simplifier_cell::imp { lean_assert(is_pi(e) && is_proposition(e)); // We don't support Pi's that are not proposition yet. // The problem is that - // axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} : - // A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) + // axiom hpiext {A A' : Type U+1} {B : A → Type U+1} {B' : A' → Type U+1} : + // A == A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) // produces an equality in TypeM even if A, A', B and B' live in smaller universes. // // This limitation does not seem to be a big problem in practice. @@ -1394,7 +1325,7 @@ class simplifier_cell::imp { // d and new_d are only provably equal, so we need to use hpiext or hallext expr x_old = mk_fresh_const(d); expr x_new = mk_fresh_const(new_d); - expr x_old_eq_x_new = mk_heq(d, new_d, x_old, x_new); + expr x_old_eq_x_new = mk_heq(x_old, x_new); expr H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new); expr bi = instantiate(abst_body(e), x_old); result res_bi = simplify_remapping_constant(bi, x_old, x_new, H_x_old_eq_x_new); @@ -1411,24 +1342,23 @@ class simplifier_cell::imp { m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::TypeMismatch); return rewrite(e, result(new_e)); } - ensure_homogeneous(d, res_d); + ensure_heterogeneous(d, res_d); ensure_homogeneous(bi, res_bi); // Remark: the argument with type A = A' in hallext and hpiext is actually @eq TypeM A A', // so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof - expr d_eq_new_d_proof = translate_eq_typem_proof(d, res_d); expr bi_eq_new_bi_proof = get_proof(res_bi); // Heqb : (∀ x x', x == x' → B x = B' x') expr Heqb = mk_lambda(abst_name(e), d, - mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), - mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), - abstract(bi_eq_new_bi_proof, {x_old, x_new, H_x_old_eq_x_new})))); + mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), + mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), + abstract(bi_eq_new_bi_proof, {x_old, x_new, H_x_old_eq_x_new})))); // Using - // theorem hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : - // A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) + // theorem hallext {A A' : Type U+1} {B : A → Bool} {B' : A' → Bool} : + // A == A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) expr new_proof = mk_hallext_th(d, new_d, Fun(x_old, d, bi), // B Fun(x_new, new_d, new_bi), // B' - d_eq_new_d_proof, // A = A' + *res_d.m_proof, // A == A' Heqb); return rewrite(e, result(new_e, new_proof)); } @@ -1453,6 +1383,58 @@ class simplifier_cell::imp { } } + result rewrite_heq(expr const & old_heq, result const & new_heq) { + expr const & new_lhs = heq_lhs(new_heq.m_expr); + expr const & new_rhs = heq_rhs(new_heq.m_expr); + if (new_lhs == new_rhs) { + // We currently cannot use heq_id as rewrite rule. + // heq_id (A : (Type U+1)) (a : A) : (a == a) ↔ true + // The problem is that A does not occur (even implicitly) in the left-hand-side, + // and it is not a proposition. + // In principle, we could extend the rewrite method to use type inference for computing A. + // IF we find more instances of this problem, we will do it. Before that, it is easier to test + // if the theorem is applicable here. + if (!m_proofs_enabled) { + return result(True); + } else { + return mk_trans_result(old_heq, new_heq, result(True, mk_heq_id_th(infer_type(new_lhs), new_lhs))); + } + } else { + return rewrite(old_heq, new_heq); + } + } + + result simplify_heq(expr const & e) { + lean_assert(is_heq(e)); + expr const & lhs = heq_lhs(e); + expr const & rhs = heq_rhs(e); + result new_lhs = simplify(lhs); + result new_rhs = simplify(rhs); + if (is_eqp(lhs, new_lhs.m_expr) && is_eqp(rhs, new_rhs.m_expr)) { + return rewrite_heq(e, result(e)); + } else { + expr new_heq = mk_heq(new_lhs.m_expr, new_rhs.m_expr); + if (!m_proofs_enabled) { + return rewrite_heq(e, result(new_heq)); + } else { + expr A_prime = infer_type(new_lhs.m_expr); + expr B_prime = infer_type(new_rhs.m_expr); + if (!new_lhs.is_heq_proof() && !new_rhs.is_heq_proof() && !is_TypeU(A_prime) && !is_TypeU(B_prime)) { + return rewrite_heq(e, result(new_heq, mk_heq_congr_th(A_prime, B_prime, + lhs, new_lhs.m_expr, rhs, new_rhs.m_expr, + get_proof(new_lhs), get_proof(new_rhs)))); + } else { + ensure_heterogeneous(lhs, new_lhs); + ensure_heterogeneous(rhs, new_rhs); + return rewrite_heq(e, result(new_heq, mk_hheq_congr_th(infer_type(lhs), A_prime, + infer_type(rhs), B_prime, + lhs, new_lhs.m_expr, rhs, new_rhs.m_expr, + *new_lhs.m_proof, *new_rhs.m_proof))); + } + } + } + } + result save(expr const & e, result const & r) { if (m_memoize) { result new_r = r.update_expr(m_max_sharing(r.m_expr)); @@ -1490,6 +1472,7 @@ class simplifier_cell::imp { case expr_kind::Lambda: return save(e, simplify_lambda(e)); case expr_kind::Pi: return save(e, simplify_pi(e)); case expr_kind::Let: return save(e, simplify(instantiate(let_body(e), let_value(e)))); + case expr_kind::HEq: return save(e, simplify_heq(e)); } lean_unreachable(); } diff --git a/tests/lean/loop3.lean b/tests/lean/loop3.lean index 8a957924c..66fa87357 100644 --- a/tests/lean/loop3.lean +++ b/tests/lean/loop3.lean @@ -2,11 +2,11 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple diff --git a/tests/lean/rs.lean.expected.out b/tests/lean/rs.lean.expected.out index 79db23df8..8d2d7983a 100644 --- a/tests/lean/rs.lean.expected.out +++ b/tests/lean/rs.lean.expected.out @@ -8,15 +8,15 @@ Nat::mul_comm : ∀ a b : ℕ, a * b = b * a Nat::add_assoc : ∀ a b c : ℕ, a + b + c = a + (b + c) Nat::add_comm : ∀ a b : ℕ, a + b = b + a Nat::add_zeror : ∀ a : ℕ, a + 0 = a -forall_rem [check] : ∀ (A : TypeU) (H : inhabited A) (p : Bool), (A → p) ↔ p +forall_rem [check] : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (A → p) ↔ p eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤ -exists_rem : ∀ (A : TypeU) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p -exists_and_distributel : ∀ (A : TypeU) (p : Bool) (φ : A → Bool), +exists_rem : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p +exists_and_distributel : ∀ (A : (Type U)) (p : Bool) (φ : A → Bool), (∃ x : A, φ x ∧ p) ↔ (∃ x : A, φ x) ∧ p -exists_or_distribute : ∀ (A : TypeU) (φ ψ : A → Bool), +exists_or_distribute : ∀ (A : (Type U)) (φ ψ : A → Bool), (∃ x : A, φ x ∨ ψ x) ↔ (∃ x : A, φ x) ∨ (∃ x : A, ψ x) not_and : ∀ a b : Bool, ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b -not_neq : ∀ (A : TypeU) (a b : A), ¬ a ≠ b ↔ a = b +not_neq : ∀ (A : (Type U)) (a b : A), ¬ a ≠ b ↔ a = b not_true : (¬ ⊤) = ⊥ and_comm : ∀ a b : Bool, a ∧ b ↔ b ∧ a and_truer : ∀ a : Bool, a ∧ ⊤ ↔ a diff --git a/tests/lean/simp18.lean b/tests/lean/simp18.lean index 88447c9f8..ba2b925da 100644 --- a/tests/lean/simp18.lean +++ b/tests/lean/simp18.lean @@ -2,11 +2,11 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple diff --git a/tests/lean/simp18.lean.expected.out b/tests/lean/simp18.lean.expected.out index 84691271b..ebc9b48af 100644 --- a/tests/lean/simp18.lean.expected.out +++ b/tests/lean/simp18.lean.expected.out @@ -14,7 +14,7 @@ v ; (w ; v) htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n)))) (to_heq (Nat::add_zeror n))) (htrans (to_heq (concat_empty (v ; w))) - (cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w)))) - (htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v))) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror (n + n))))) (v ; w)))) + (htrans (to_heq (concat_empty v)) (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v))) (to_heq (concat_assoc v w v))) - (cast_heq (congr2 vec (symm (Nat::add_assoc n n n))) (v ; (w ; v))) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_assoc n n n)))) (v ; (w ; v))) diff --git a/tests/lean/simp19.lean b/tests/lean/simp19.lean index a18f641ae..16b4b8348 100644 --- a/tests/lean/simp19.lean +++ b/tests/lean/simp19.lean @@ -2,16 +2,19 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror : simple +universe M >= 1 +definition TypeM := (Type M) + variable n : Nat variable v : vec n variable w : vec n diff --git a/tests/lean/simp19.lean.expected.out b/tests/lean/simp19.lean.expected.out index c1b9a96b7..e0759e850 100644 --- a/tests/lean/simp19.lean.expected.out +++ b/tests/lean/simp19.lean.expected.out @@ -5,6 +5,7 @@ Assumed: concat_assoc Assumed: empty Assumed: concat_empty + Defined: TypeM Assumed: n Assumed: v Assumed: w @@ -13,14 +14,15 @@ f (v ; w ; empty ; (v ; empty)) ===> f (v ; (w ; v)) hcongr (hcongr (hrefl @f) - (to_heq (subst (refl (vec (n + n + 0 + (n + 0)))) - (congr2 vec - (trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n)) - (Nat::add_assoc n n n)))))) + (to_heq (congr2 vec + (trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n)) + (Nat::add_assoc n n n))))) (htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n)))) (to_heq (Nat::add_zeror n))) (htrans (to_heq (concat_empty (v ; w))) - (cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w)))) - (htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v))) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror (n + n))))) + (v ; w)))) + (htrans (to_heq (concat_empty v)) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v))) (to_heq (concat_assoc v w v))) - (cast_heq (congr2 vec (symm (Nat::add_assoc n n n))) (v ; (w ; v)))) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_assoc n n n)))) (v ; (w ; v)))) diff --git a/tests/lean/simp20.lean b/tests/lean/simp20.lean index f6cd3e759..4ece305a8 100644 --- a/tests/lean/simp20.lean +++ b/tests/lean/simp20.lean @@ -2,6 +2,8 @@ rewrite_set simple set_option pp::implicit true +universe M >= 1 +definition TypeM := (Type M) variable g : TypeM → TypeM variable B : Type variable B' : Type diff --git a/tests/lean/simp20.lean.expected.out b/tests/lean/simp20.lean.expected.out index 674a86c71..dce193cb8 100644 --- a/tests/lean/simp20.lean.expected.out +++ b/tests/lean/simp20.lean.expected.out @@ -1,6 +1,7 @@ Set: pp::colors Set: pp::unicode Set: lean::pp::implicit + Defined: TypeM Assumed: g Assumed: B Assumed: B' @@ -8,5 +9,5 @@ g B ===> g B' -@congr2 TypeM TypeM B B' g (@subst Type B B' (λ x : Type, @eq TypeM B x) (@refl TypeM B) H) +@congr2 TypeM TypeM B B' g (@to_eq TypeM B B' (@to_heq Type B B' H)) @eq TypeM (g B) (g B') diff --git a/tests/lean/simp22.lean b/tests/lean/simp22.lean index 43aad69ac..2a491e40d 100644 --- a/tests/lean/simp22.lean +++ b/tests/lean/simp22.lean @@ -2,11 +2,11 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple @@ -15,6 +15,9 @@ rewrite_set simple -- rewrite set, we prevent the simplifier from reducing the following example add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror Nat::add_comm : simple +universe M >= 1 +definition TypeM := (Type M) + variable n : Nat variable v : vec n variable w : vec n diff --git a/tests/lean/simp22.lean.expected.out b/tests/lean/simp22.lean.expected.out index 24f526083..8e22b4dd0 100644 --- a/tests/lean/simp22.lean.expected.out +++ b/tests/lean/simp22.lean.expected.out @@ -5,6 +5,7 @@ Assumed: concat_assoc Assumed: empty Assumed: concat_empty + Defined: TypeM Assumed: n Assumed: v Assumed: w @@ -18,14 +19,15 @@ f (v ; w ; empty ; (v ; empty)) ===> f (v ; (w ; v)) hcongr (hcongr (hrefl @f) - (to_heq (subst (refl (vec (n + n + 0 + (n + 0)))) - (congr2 vec - (trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n)) - (Nat::add_assoc n n n)))))) + (to_heq (congr2 vec + (trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n)) + (Nat::add_assoc n n n))))) (htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n)))) (to_heq (Nat::add_zeror n))) (htrans (to_heq (concat_empty (v ; w))) - (cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w)))) - (htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v))) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror (n + n))))) + (v ; w)))) + (htrans (to_heq (concat_empty v)) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v))) (to_heq (concat_assoc v w v))) - (cast_heq (congr2 vec (symm (Nat::add_assoc n n n))) (v ; (w ; v)))) + (cast_heq (to_heq (congr2 vec (symm (Nat::add_assoc n n n)))) (v ; (w ; v)))) diff --git a/tests/lean/simp23.lean b/tests/lean/simp23.lean index 2df2116a3..05aa0f6ed 100644 --- a/tests/lean/simp23.lean +++ b/tests/lean/simp23.lean @@ -2,16 +2,19 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror and_truer eq_id : simple +universe M >= 1 +definition TypeM := (Type M) + variable n : Nat variable v : vec n variable w : vec n @@ -22,7 +25,7 @@ add_rewrite fax : simple (* local opts = options({"simplifier", "heq"}, true) -local t = parse_lean([[ p (f ((v ; w) ; empty ; (v ; empty))) ∧ v = cast (congr2 vec (Nat::add_zeror n)) (v ; empty) ]]) +local t = parse_lean([[ p (f ((v ; w) ; empty ; (v ; empty))) ∧ v = cast (to_heq (congr2 vec (Nat::add_zeror n))) (v ; empty) ]]) print(t) print("===>") local t2, pr = simplify(t, "simple", opts) diff --git a/tests/lean/simp23.lean.expected.out b/tests/lean/simp23.lean.expected.out index 1431f3c6b..b9bbb0184 100644 --- a/tests/lean/simp23.lean.expected.out +++ b/tests/lean/simp23.lean.expected.out @@ -5,14 +5,16 @@ Assumed: concat_assoc Assumed: empty Assumed: concat_empty + Defined: TypeM Assumed: n Assumed: v Assumed: w Assumed: f Assumed: p Assumed: fax -p (f (v ; w ; empty ; (v ; empty))) ∧ v = cast (congr2 vec (Nat::add_zeror n)) (v ; empty) +p (f (v ; w ; empty ; (v ; empty))) ∧ v = cast (to_heq (congr2 vec (Nat::add_zeror n))) (v ; empty) ===> p (v ; (w ; v)) checking proof -(p (f (v ; w ; empty ; (v ; empty))) ∧ v = cast (congr2 vec (Nat::add_zeror n)) (v ; empty)) == p (v ; (w ; v)) +(p (f (v ; w ; empty ; (v ; empty))) ∧ v = cast (to_heq (congr2 vec (Nat::add_zeror n))) (v ; empty)) == +(p (v ; (w ; v))) diff --git a/tests/lean/simp28.lean b/tests/lean/simp28.lean index e8826fef4..f0696901d 100644 --- a/tests/lean/simp28.lean +++ b/tests/lean/simp28.lean @@ -2,11 +2,11 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple @@ -35,6 +35,9 @@ get_environment():type_check(pr) print "" +universe M >= 1 +definition TypeM := (Type M) + variable lheq {A B : TypeM} : A → B → Bool infixl 50 === : lheq (* diff --git a/tests/lean/simp28.lean.expected.out b/tests/lean/simp28.lean.expected.out index 911fab927..4a9654710 100644 --- a/tests/lean/simp28.lean.expected.out +++ b/tests/lean/simp28.lean.expected.out @@ -9,6 +9,7 @@ Assumed: f λ n : ℕ, f + Defined: TypeM Assumed: lheq λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val === (λ (n : ℕ) (v : vec (n + 0)), v) val =====> diff --git a/tests/lean/simp30.lean b/tests/lean/simp30.lean index 24b406d1f..fa1d93fb6 100644 --- a/tests/lean/simp30.lean +++ b/tests/lean/simp30.lean @@ -2,11 +2,11 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple diff --git a/tests/lean/simp32.lean b/tests/lean/simp32.lean index 7f24d23e5..d146ef5d2 100644 --- a/tests/lean/simp32.lean +++ b/tests/lean/simp32.lean @@ -2,11 +2,11 @@ variable vec : Nat → Type variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) infixl 65 ; : concat axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : - (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; v2) ; v3 = cast (to_heq (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))) (v1 ; (v2 ; v3)) variable empty : vec 0 axiom concat_empty {n : Nat} (v : vec n) : - v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v ; empty = cast (to_heq (congr2 vec (symm (Nat::add_zeror n)))) v rewrite_set simple diff --git a/tests/lean/simp32.lean.expected.out b/tests/lean/simp32.lean.expected.out index 3360c8acb..e537adb02 100644 --- a/tests/lean/simp32.lean.expected.out +++ b/tests/lean/simp32.lean.expected.out @@ -6,9 +6,6 @@ Assumed: empty Assumed: concat_empty Assumed: f -λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val +λ val : ℕ, ((λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val) == ((λ (n : ℕ) (v : vec (n + 0)), v) val) =====> -App simplification failure, argument #2 -Kind: 0 ------------ -λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val +λ val : ℕ, f == (λ v : vec val, v)