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 ce394517b..c7aeb2880 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ 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)