michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-07 15:03:16 -08:00
parent 6d7ec9d7b6
commit ad7b13104f
29 changed files with 417 additions and 303 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
examples/lean/dep_if.lean
View file

@ -10,16 +10,16 @@ import tactic
-- We define the "dependent" if-then-else using Hilbert's choice operator ε. -- We define the "dependent" if-then-else using Hilbert's choice operator ε.
-- Note that ε is only applicable to non-empty types. Thus, we first -- Note that ε is only applicable to non-empty types. Thus, we first
-- prove the following auxiliary theorem. -- 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) := or_elim (em c)
(λ Hc, inhabited_range (inhabited_intro t) Hc) (λ Hc, inhabited_range (inhabited_intro t) Hc)
(λ Hnc, inhabited_range (inhabited_intro e) Hnc) (λ Hnc, inhabited_range (inhabited_intro e) Hnc)
-- The actual definition -- 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)) := ε (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 : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = t H
:= let s1 : (∀ Hc : c, r = t Hc) ↔ r = t H := let s1 : (∀ Hc : c, r = t Hc) ↔ r = t H
:= iff_intro := iff_intro
@ -32,17 +32,17 @@ theorem then_simp (A : TypeU) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A)
in by simp in by simp
-- Given H : c, (dep_if c t e) = t H -- 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) := 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) := 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) 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 } ... = ε (inhabited_resolve t e) (λ r, r = t H) : { s1 }
... = t H : eps_singleton (inhabited_resolve t e) (t H) ... = 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 := 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 : (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H
:= let s1 : (∀ Hc : c, r = t Hc) ↔ true := let s1 : (∀ Hc : c, r = t Hc) ↔ true
:= eqt_intro (λ Hc : c, absurd_elim (r = t Hc) Hc H), := 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 in by simp
-- Given H : ¬ c, (dep_if c t e) = e H -- 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) := 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) := 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) 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 } ... = ε (inhabited_resolve t e) (λ r, r = e H) : { s1 }
... = e H : eps_singleton (inhabited_resolve t e) (e H) ... = 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 := dep_if_elim_else false t e not_false_trivial
set_option simplifier::heq true -- enable heterogeneous equality support 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) (t1 : c1 → A) (t2 : c2 → A)
(e1 : ¬ c1 → A) (e2 : ¬ c2 → A) (e1 : ¬ c1 → A) (e2 : ¬ c2 → A)
(Hc : c1 = c2) (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 -- 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 -- 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) := or_elim (em c)
(assume Hc : c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hc, t) Hc : dep_if_elim_then _ _ _ Hc (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) ... = if c then t else e : by simp)

201
src/builtin/kernel.lean
View file

@ -11,12 +11,11 @@ definition TypeU := (Type U)
(* mk_rewrite_rule_set() *) (* mk_rewrite_rule_set() *)
variable Bool : Type variable Bool : Type
-- Heterogeneous equality
variable heq2 {A B : (Type U)} (a : A) (b : B) : Bool
infixl 50 == : heq2
-- Reflexivity for heterogeneous equality -- 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 -- Homogeneous equality
definition eq {A : (Type U)} (a b : A) := a == b 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 theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
:= assume Ha, H2 (H1 ◂ Ha) := 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 := (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 := (symm (heq_eq a b)) ◂ H
theorem iff_eliml {a b : Bool} (H : a ↔ b) : a → b 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 theorem iff_elimr {a b : Bool} (H : a ↔ b) : b → a
:= (λ Hb : b, eqmpr H Hb) := (λ 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) := 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) := 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 := subst H1 H2
theorem eqt_elim {a : Bool} (H : a = true) : a 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 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) := not_not_eq (a = b)
add_rewrite not_neq 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 := (not_neq a b) ◂ H
theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a 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 theorem iff_id (a : Bool) : (a ↔ a) ↔ true
:= eqt_intro (refl a) := 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 theorem neq_elim {A : (Type U)} {a b : A} (H : a ≠ b) : a = b ↔ false
:= eqf_intro H := eqf_intro H
@ -429,12 +431,12 @@ theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
:= congr2 not H := congr2 not H
-- Recall that exists is defined as ¬ ∀ x : A, ¬ P x -- 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, := refute (λ R : ¬ B,
absurd (take a : A, mt (assume H : P a, H2 a H) R) absurd (take a : A, mt (assume H : P a, H2 a H) R)
H1) 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), := assume H1 : (∀ x : A, ¬ P x),
absurd H (H1 a) 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 theorem not_exists_elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x
:= (not_exists A P) ◂ H := (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 := exists_elim H
(λ (w : A) (H1 : P w), (λ (w : A) (H1 : P w),
or_elim (em (w = a)) or_elim (em (w = a))
(λ Heq : w = a, or_introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) (λ 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)))) (λ 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 := or_elim H
(λ H1 : P a, exists_intro a H1) (λ H1 : P a, exists_intro a H1)
(λ H2 : (∃ x : A, x ≠ a ∧ P x), (λ 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), (λ (w : A) (Hw : w ≠ a ∧ P w),
exists_intro w (and_elimr Hw))) 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) := 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) (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 := ∃ x : A, true
-- If we have an element of type A, then A is inhabited -- 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) := 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, := obtain (w : A) (Hw : true), from H1,
H2 w 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, := obtain (w : A) (Hw : P w), from H,
exists_intro w trivial 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 -- 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), := refute (λ N : ¬ inhabited (B a),
let s1 : ¬ ∃ x : B a, true := N, let s1 : ¬ ∃ x : B a, true := N,
s2 : ∀ x : B a, false := take x : B a, absurd_not_true (not_exists_elim s1 x), 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 let s4 : B a := w a
in s2 s4) 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 := iff_intro
(assume Hl : (∃ x : A, p), (assume Hl : (∃ x : A, p),
obtain (w : A) (Hw : p), from Hl, 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, (assume Hr : p,
inhabited_elim H (λ w, exists_intro w Hr)) 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 := iff_intro
(assume Hl : (∀ x : A, p), (assume Hl : (∀ x : A, p),
inhabited_elim H (λ w, Hl w)) 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 theorem not_iff_elim {a b : Bool} (H : ¬ (a ↔ b)) : (¬ a) ↔ b
:= (not_iff a b) ◂ H := (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 := boolext
(assume H : (∀ x, p ∨ φ x), (assume H : (∀ x, p ∨ φ x),
or_elim (em p) 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) (λ H1 : (∀ x, φ x), or_introl (H1 x) p)
(λ H2 : p, or_intror (φ x) H2)) (λ 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 := boolext
(assume H : (∀ x, φ x ∧ ψ x), (assume H : (∀ x, φ x ∧ ψ x),
and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x))) and_intro (take x, and_eliml (H x)) (take x, and_elimr (H x)))
(assume H : (∀ x, φ x) ∧ (∀ x, ψ x), (assume H : (∀ x, φ x) ∧ (∀ x, ψ x),
take x, and_intro (and_eliml H x) (and_elimr H 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 := boolext
(assume H : (∃ x, p ∧ φ x), (assume H : (∃ x, p ∧ φ x),
obtain (w : A) (Hw : p ∧ φ w), from H, 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)) 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 := boolext
(assume H : (∃ x, φ x ∨ ψ x), (assume H : (∃ x, φ x ∨ ψ x),
obtain (w : A) (Hw : φ w ∨ ψ w), from H, 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 theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
:= (not_forall A P) ◂ H := (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) := calc (∃ x, φ x ∧ p) = (∃ x, p ∧ φ x) : eq_exists_intro (λ x, and_comm (φ x) p)
... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ ... = (p ∧ (∃ x, φ x)) : exists_and_distributer p φ
... = ((∃ x, φ x) ∧ p) : and_comm p (∃ x, φ x) ... = ((∃ 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)) := 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) : exists_or_distribute _ _
... = ¬ (∀ x, φ x) ∨ (∃ x, ψ x) : { symm (not_forall A φ) } ... = ¬ (∀ 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 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 -- 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)) := funext (λ x : A, refl (f x))
-- Epsilon (Hilbert's operator) -- 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 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 := 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, := let P := λ x, x = a,
Ha : P a := refl a Ha : P a := refl a
in eps_ax H a Ha in eps_ax H a Ha
-- A function space (∀ x : A, B x) is inhabited if forall a : A, we have inhabited (B a) -- 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)) := 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, := obtain (w : A) (Hw : P w), from H,
eps_ax (inhabited_ex_intro H) w Hw 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 := exists_intro
(λ x, ε (inhabited_ex_intro (H x)) (λ y, R x y)) -- witness for f (λ 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) (λ 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)) (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x))
:= iff_intro := iff_intro
(λ H : (∀ x, ∃ y, P x y), axiom_of_choice H) (λ 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)) exists_intro (fw x) (Hw x))
-- if-then-else expression, we define it using Hilbert's operator -- 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)) := ε (inhabited_intro a) (λ r, (c → r = a) ∧ (¬ c → r = b))
notation 45 if _ then _ else _ : ite 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) := 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 ... = ε (inhabited_intro a) (λ r, r = a) : by simp
... = a : eps_singleton (inhabited_intro a) a ... = 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) := 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 ... = ε (inhabited_intro a) (λ r, r = b) : by simp
... = b : eps_singleton (inhabited_intro a) b ... = 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) := or_elim (em c)
(λ H : c, calc (if c then a else a) = (if true then a else a) : { eqt_intro H } (λ H : c, calc (if c then a else a) = (if true then a else a) : { eqt_intro H }
... = a : if_true a a) ... = 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 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) : (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 (if b then x else y) = if c then u else v
:= or_elim (em c) := 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) } ... = if a then b else c : { symm (eqf_intro Hna) }
... = true : eqt_intro H) ... = 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) := or_elim (em c)
(λ Hc : c , calc (λ Hc : c , calc
f (if c then a else b) = f (if true then a else b) : { eqt_intro Hc } 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 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) }) ... = 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 := 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 := app_if_distribute c (λ x, x = v) a b
set_opaque exists true 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 -- Heterogeneous equality axioms and theorems
-- In the following definitions the type of A and B cannot be (Type U) -- We can "type-cast" an A expression into a B expression, if we can prove that A == B
-- because A = B would be @eq (Type U+1) A B, and -- Remark: we use A == B instead of A = B, because A = B would be type incorrect.
-- the type of eq is (∀T : (Type U), T → T → bool). -- A = B is actually (@eq (Type U) A B), which is type incorrect because
-- So, we define M a universe smaller than U. -- the first argument of eq must have type (Type U) and the type of (Type U) is (Type U+1)
universe M ≥ 1 variable cast {A B : (Type U+1)} : A == B → A → B
definition TypeM := (Type M)
-- We can "type-cast" an A expression into a B expression, if we can prove that A = B axiom cast_heq {A B : (Type U+1)} (H : A == B) (a : A) : cast H a == a
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
-- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence and function extensionality -- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence, 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 -- Heterogeneous version of subst
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'} : 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' 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 -- Heterogeneous version of the allext theorem
theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool} 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) (Ha : A == A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x)
:= boolext := to_eq (hpiext Ha (λ x x' Heq, to_heq (Hb x x' Heq)))
(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)))
-- Simpler version of hfunext axiom, we use it to build proofs -- 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' (∀ x, f x == f' x) → f == f'
:= λ Hb, := λ 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, 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) 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. -- 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) := 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 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
:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a), := have Heq1 : cast Hbc (cast Hab a) == cast Hab a,
s2 : cast Hab a == a := cast_heq Hab a, from cast_heq Hbc (cast Hab a),
s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a, have Heq2 : cast Hab a == a,
s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3) from cast_heq Hab a,
in to_eq s4 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)} 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)) : (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) cast Hb f a = cast Hba (f a)
:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a), := have s1 : cast Hb f a == f a,
s2 : cast Hba (f a) == f a := cast_heq Hba (f a) from hcongr (cast_heq Hb f) (hrefl a),
in to_eq (htrans s1 (hsymm s2)) 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. -- Proof irrelevance is true in the set theoretic model we have for Lean.
axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2 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 -- 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 theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
:= let H1b : b := cast (by simp) H1, := let Hab : a == b := to_heq (iff_intro (assume Ha, H2) (assume Hb, H1)),
H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) 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) H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2)
in htrans H1_eq_H1b H1b_eq_H2 in htrans H1_eq_H1b H1b_eq_H2

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

10
src/frontends/lean/parser_expr.cpp
View file

@ -583,6 +583,14 @@ expr parser_imp::parse_led_id(expr const & left) {
} }
} }
/** \brief Parse <tt>expr '==' expr</tt>. */
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 <tt>expr '->' expr</tt>. */ /** \brief Parse <tt>expr '->' expr</tt>. */
expr parser_imp::parse_arrow(expr const & left) { expr parser_imp::parse_arrow(expr const & left) {
auto p = pos(); auto p = pos();
@ -1087,6 +1095,7 @@ expr parser_imp::parse_led(expr const & left) {
switch (curr()) { switch (curr()) {
case scanner::token::Id: return parse_led_id(left); case scanner::token::Id: return parse_led_id(left);
case scanner::token::Arrow: return parse_arrow(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::CartesianProduct: return parse_cartesian_product(left);
case scanner::token::LeftParen: return mk_app_left(left, parse_lparen()); case scanner::token::LeftParen: return mk_app_left(left, parse_lparen());
case scanner::token::IntVal: return mk_app_left(left, parse_nat_int()); 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::Arrow : return g_arrow_precedence;
case scanner::token::CartesianProduct: return g_cartesian_product_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::LeftParen: case scanner::token::IntVal: case scanner::token::DecimalVal:
case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder: case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder:
return g_app_precedence; return g_app_precedence;

1
src/frontends/lean/parser_imp.h
View file

@ -311,6 +311,7 @@ private:
pos_info const & p); pos_info const & p);
expr parse_expr_macro(name const & id, pos_info const & p); expr parse_expr_macro(name const & id, pos_info const & p);
expr parse_led_id(expr const & left); expr parse_led_id(expr const & left);
expr parse_heq(expr const & left);
expr parse_arrow(expr const & left); expr parse_arrow(expr const & left);
expr parse_cartesian_product(expr const & left); expr parse_cartesian_product(expr const & left);
expr parse_lparen(); expr parse_lparen();

4
src/frontends/lean/scanner.cpp
View file

@ -21,6 +21,7 @@ static name g_type_name("Type");
static name g_pi_name("forall"); static name g_pi_name("forall");
static name g_let_name("let"); static name g_let_name("let");
static name g_in_name("in"); static name g_in_name("in");
static name g_heq_name("==");
static name g_arrow_name("->"); static name g_arrow_name("->");
static name g_exists_name("exists"); static name g_exists_name("exists");
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; return token::Arrow;
else if (m_name_val == g_cartesian_product) else if (m_name_val == g_cartesian_product)
return token::CartesianProduct; return token::CartesianProduct;
else if (m_name_val == g_heq_name)
return token::HEq;
else else
return token::Id; 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::Show: out << "show"; break;
case scanner::token::By: out << "by"; break; case scanner::token::By: out << "by"; break;
case scanner::token::Ellipsis: out << "..."; break; case scanner::token::Ellipsis: out << "..."; break;
case scanner::token::HEq: out << "=="; break;
case scanner::token::Eof: out << "EOF"; break; case scanner::token::Eof: out << "EOF"; break;
} }
return out; return out;

2
src/frontends/lean/scanner.h
View file

@ -20,7 +20,7 @@ class scanner {
public: public:
enum class token { enum class token {
LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow, 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 Have, Show, By, ScriptBlock, Ellipsis, CartesianProduct, Eof
}; };
protected: protected:

9
src/kernel/kernel_decls.cpp
View file

@ -8,7 +8,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
namespace lean { namespace lean {
MK_CONSTANT(TypeU, name("TypeU")); MK_CONSTANT(TypeU, name("TypeU"));
MK_CONSTANT(Bool, name("Bool")); MK_CONSTANT(Bool, name("Bool"));
MK_CONSTANT(heq2_fn, name("heq2"));
MK_CONSTANT(hrefl_fn, name("hrefl")); MK_CONSTANT(hrefl_fn, name("hrefl"));
MK_CONSTANT(eq_fn, name("eq")); MK_CONSTANT(eq_fn, name("eq"));
MK_CONSTANT(refl_fn, name("refl")); 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(a_neq_a_fn, name("a_neq_a"));
MK_CONSTANT(eq_id_fn, name("eq_id")); MK_CONSTANT(eq_id_fn, name("eq_id"));
MK_CONSTANT(iff_id_fn, name("iff_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_elim_fn, name("neq_elim"));
MK_CONSTANT(neq_to_not_eq_fn, name("neq_to_not_eq")); MK_CONSTANT(neq_to_not_eq_fn, name("neq_to_not_eq"));
MK_CONSTANT(left_comm_fn, name("left_comm")); 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(ind, name("ind"));
MK_CONSTANT(infinity, name("infinity")); MK_CONSTANT(infinity, name("infinity"));
MK_CONSTANT(pairext_fn, name("pairext")); MK_CONSTANT(pairext_fn, name("pairext"));
MK_CONSTANT(TypeM, name("TypeM"));
MK_CONSTANT(cast_fn, name("cast")); MK_CONSTANT(cast_fn, name("cast"));
MK_CONSTANT(cast_heq_fn, name("cast_heq")); MK_CONSTANT(cast_heq_fn, name("cast_heq"));
MK_CONSTANT(hsubst_fn, name("hsubst"));
MK_CONSTANT(hsymm_fn, name("hsymm")); MK_CONSTANT(hsymm_fn, name("hsymm"));
MK_CONSTANT(htrans_fn, name("htrans")); MK_CONSTANT(htrans_fn, name("htrans"));
MK_CONSTANT(hcongr_fn, name("hcongr")); MK_CONSTANT(hcongr_fn, name("hcongr"));
MK_CONSTANT(hfunext_fn, name("hfunext")); 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(hallext_fn, name("hallext"));
MK_CONSTANT(hsfunext_fn, name("hsfunext")); 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_eq_fn, name("cast_eq"));
MK_CONSTANT(cast_trans_fn, name("cast_trans")); MK_CONSTANT(cast_trans_fn, name("cast_trans"));
MK_CONSTANT(cast_pull_fn, name("cast_pull")); MK_CONSTANT(cast_pull_fn, name("cast_pull"));

27
src/kernel/kernel_decls.h
View file

@ -9,10 +9,6 @@ expr mk_TypeU();
bool is_TypeU(expr const & e); bool is_TypeU(expr const & e);
expr mk_Bool(); expr mk_Bool();
bool is_Bool(expr const & e); 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(); expr mk_hrefl_fn();
bool is_hrefl_fn(expr const & e); 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}); } 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(); expr mk_iff_id_fn();
bool is_iff_id_fn(expr const & e); 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}); } 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(); expr mk_neq_elim_fn();
bool is_neq_elim_fn(expr const & e); 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}); } 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(); expr mk_pairext_fn();
bool is_pairext_fn(expr const & e); 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}); } 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(); expr mk_cast_fn();
bool is_cast_fn(expr const & e); bool is_cast_fn(expr const & e);
inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; } inline 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(); expr mk_cast_heq_fn();
bool is_cast_heq_fn(expr const & e); 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}); } 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(); expr mk_hsymm_fn();
bool is_hsymm_fn(expr const & e); 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}); } 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(); expr mk_hfunext_fn();
bool is_hfunext_fn(expr const & e); 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}); } 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(); expr mk_hallext_fn();
bool is_hallext_fn(expr const & e); 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}); } 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(); expr mk_hsfunext_fn();
bool is_hsfunext_fn(expr const & e); 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}); } 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(); expr mk_cast_eq_fn();
bool is_cast_eq_fn(expr const & e); 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}); } 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}); }

7
src/kernel/level.cpp
View file

@ -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; } unsigned _lift_offset(level const & l) { return is_lift(l) ? lift_offset(l) : 0; }
void push_back(buffer<level> & ls, level const & l) { void push_back(buffer<level> & ls, level const & l) {
if (l.is_bottom())
return;
for (unsigned i = 0; i < ls.size(); i++) { for (unsigned i = 0; i < ls.size(); i++) {
if (_lift_of(ls[i]) == _lift_of(l)) { if (_lift_of(ls[i]) == _lift_of(l)) {
if (_lift_offset(ls[i]) < _lift_offset(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<level> new_lvls; buffer<level> new_lvls;
std::for_each(ls1, ls1 + sz1, [&](level const & l) { push_back(new_lvls, l); }); 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); }); 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]; return new_lvls[0];
else else
return max_core(new_lvls.size(), new_lvls.data()); return max_core(new_lvls.size(), new_lvls.data());

121
src/library/elaborator/elaborator.cpp
View file

@ -375,7 +375,7 @@ class elaborator::imp {
} }
/** /**
\brief Push a new equality constraint <tt>new_ctx |- new_a == new_b</tt> into the active_cnstrs using \brief Push a new equality constraint <tt>new_ctx |- new_a ≈ new_b</tt> into the active_cnstrs using
justification \c new_jst. justification \c new_jst.
*/ */
void push_new_eq_constraint(cnstr_list & active_cnstrs, void push_new_eq_constraint(cnstr_list & active_cnstrs,
@ -482,7 +482,7 @@ class elaborator::imp {
} }
/** /**
Process <tt>ctx |- a == b</tt> and <tt>ctx |- a << b</tt> when: Process <tt>ctx |- a ≈ b</tt> and <tt>ctx |- a << b</tt> when:
1- \c a is an assigned metavariable 1- \c a is an assigned metavariable
2- \c a is a unassigned metavariable without a metavariable context. 2- \c a is a unassigned metavariable without a metavariable context.
3- \c a is a unassigned metavariable of the form <tt>?m[lift:s:n, ...]</tt>, and \c b does not have 3- \c a is a unassigned metavariable of the form <tt>?m[lift:s:n, ...]</tt>, and \c b does not have
@ -521,9 +521,9 @@ class elaborator::imp {
// Let ctx be of the form // Let ctx be of the form
// [ce_{m-1}, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0] // [ce_{m-1}, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0]
// Then, we reduce // 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 // 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. // 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 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 constraint is solved by assigning ?m to (fun x1 ... xn, c).
The arguments may contain duplicate occurrences of variables. The arguments may contain duplicate occurrences of variables.
2) a constraint of the form 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) 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) { 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 // Solve constraint of the form
// ctx |- (?m x) == c // ctx |- (?m x) ≈ c
// using imitation // using imitation
bool eq_closed = is_simple_ho_match_closed(ctx, a, b, is_lhs, c); 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); 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); expr f_b = arg(b, 0);
unsigned num_b = num_args(b); 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}) // 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<expr> imitation_args; // arguments for the imitation buffer<expr> imitation_args; // arguments for the imitation
imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1, new_state.m_menv)); 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++) { for (unsigned i = 1; i < num_b; i++) {
@ -979,8 +979,8 @@ class elaborator::imp {
// Imitation for lambdas, Pis, and Sigmas // Imitation for lambdas, Pis, and Sigmas
// Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), // 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) // 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) // New constraints (h_1 a_1 ... a_{num_a}) ≈ abst_domain(b)
// (h_2 a_1 ... a_{num_a} x_b) == abst_body(b) // (h_2 a_1 ... a_{num_a} x_b) ≈ abst_body(b)
expr h_1 = new_state.m_menv->mk_metavar(ctx); expr h_1 = new_state.m_menv->mk_metavar(ctx);
context new_ctx = extend(ctx, abst_name(b), abst_domain(b)); 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))); 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); 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))); 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)) { } else if (is_pair(b)) {
// Imitation for dependent pairs // Imitation for dependent pairs
expr h_f = new_state.m_menv->mk_metavar(ctx); 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 \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. 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. 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: 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 The possible solutions is the set of solutions for
1- ?m[lift:1:1, inst:2:b] == #3 1- ?m[lift:1:1, inst:2:b] ≈ #3
2- ?m[lift:1:1, inst:2:b] == b 2- ?m[lift:1:1, inst:2:b] ≈ b
The solutions for constraints 1 and 2 are the solutions for The solutions for constraints 1 and 2 are the solutions for
1.1- ?m[inst:2:b] == #2 1.1- ?m[inst:2:b] ≈ #2
2.1- ?m[inst:2:b] == b 2.1- ?m[inst:2:b] ≈ b
And 1.1 has two possible solutions And 1.1 has two possible solutions
1.1.1 ?m == #3 1.1.1 ?m ≈ #3
1.1.2 ?m == b 1.1.2 ?m ≈ b
And 2.1 has also two possible solutions And 2.1 has also two possible solutions
2.1.1 ?m == #2 2.1.1 ?m ≈ #2
2.1.2 ?m == b 2.1.2 ?m ≈ b
Thus, the resulting set of solutions is {#3, b, #2} Thus, the resulting set of solutions is {#3, b, #2}
*/ */
@ -1143,7 +1150,7 @@ class elaborator::imp {
/** /**
\brief Solve a constraint of the form \brief Solve a constraint of the form
ctx |- a == b ctx |- a ≈ b
where where
a is of the form ?m[...] i.e., metavariable with a non-empty local context. a is of the form ?m[...] i.e., metavariable with a non-empty local context.
b is an abstraction b is an abstraction
@ -1217,7 +1224,7 @@ class elaborator::imp {
} }
/** /**
\brief Solve a constraint of the form \brief Solve a constraint of the form
ctx |- a == b ctx |- a ≈ b
where where
a is of the form ?m[...] i.e., metavariable with a non-empty local context. a is of the form ?m[...] i.e., metavariable with a non-empty local context.
b is a pair projection. b is a pair projection.
@ -1244,7 +1251,7 @@ class elaborator::imp {
/** /**
\brief Solve a constraint of the form \brief Solve a constraint of the form
ctx |- a == b ctx |- a ≈ b
where where
a is of the form ?m[...] i.e., metavariable with a non-empty local context. a is of the form ?m[...] i.e., metavariable with a non-empty local context.
b is a dependent pair b is a dependent pair
@ -1272,19 +1279,46 @@ class elaborator::imp {
} }
/** /**
\brief Process a constraint <tt>ctx |- a == b</tt> where \c a is of the form <tt>?m[(inst:i t), ...]</tt>. \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 <tt>ctx |- a ≈ b</tt> where \c a is of the form <tt>?m[(inst:i t), ...]</tt>.
We perform a "case split", 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 Case 2) imitate b
*/ */
bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { 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. // 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: // A possible solution for this constraint is:
// ?M2 == #1 // ?M2 ≈ #1
// ?M1 == f#2 #1 // ?M1 ≈ f#2 #1
// //
// TODO(Leo): consider the following alternative design: We do NOT use approximations, since it is quite // 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 // 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)) { } else if (is_proj(b)) {
imitate_proj(a, b, c); imitate_proj(a, b, c);
return true; return true;
} else if (is_heq(b)) {
imitate_heq(a, b, c);
return true;
} else if (is_pair(b)) { } else if (is_pair(b)) {
imitate_pair(a, b, c); imitate_pair(a, b, c);
return true; return true;
@ -1341,7 +1378,7 @@ class elaborator::imp {
} }
/** /**
\brief Process a constraint of the form <tt>ctx |- ?m[lift, ...] == b</tt> where \c b is an abstraction. \brief Process a constraint of the form <tt>ctx |- ?m[lift, ...] ≈ b</tt> where \c b is an abstraction.
That is, \c b is a Pi or Lambda. In both cases, ?m must have the same kind. 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. 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 <tt>ctx |- max(L1, L2) == a</tt>. \brief Return true iff the current queue has a max constraint of the form <tt>ctx |- max(L1, L2) ≈ a</tt>.
\pre is_metavar(a) \pre is_metavar(a)
*/ */
@ -1433,7 +1470,7 @@ class elaborator::imp {
// We approximate and only consider the most useful ones. // We approximate and only consider the most useful ones.
// //
// Remark: we only consider \c a if the queue does not have a constraint // 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 // 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. // and just check if the upper bound is satisfied.
// //
@ -1505,7 +1542,7 @@ class elaborator::imp {
We replace We replace
ctx | ?m << Pi(x : A, B) ctx | ?m << Pi(x : A, B)
with with
ctx |- ?m == Pi(x : A, ?m1) ctx |- ?m ≈ Pi(x : A, ?m1)
ctx, x : A |- ?m1 << B ctx, x : A |- ?m1 << B
*/ */
void process_metavar_conv_pi(unification_constraint const & c, expr const & m, expr const & pi, bool is_lhs) { 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); expr m1 = m_state.m_menv->mk_metavar(new_ctx);
justification new_jst(new destruct_justification(c)); justification new_jst(new destruct_justification(c));
// Add ctx, x : A |- ?m1 << B when is_lhs == true, // Add ctx, x : A |- ?m1 << B when is_lhs ≈ true,
// and ctx, x : A |- B << ?m1 when is_lhs == false // and ctx, x : A |- B << ?m1 when is_lhs ≈ false
expr lhs = m1; expr lhs = m1;
expr rhs = abst_body(pi); expr rhs = abst_body(pi);
if (!is_lhs) if (!is_lhs)
swap(lhs, rhs); swap(lhs, rhs);
push_new_constraint(false, new_ctx, lhs, rhs, new_jst); 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); 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_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 // If m_assume_injectivity is true, we apply the following rule
// ctx |- (f a1 a2) == (f b1 b2) // ctx |- (f a1 a2) ≈ (f b1 b2)
// ===> // ==>
// ctx |- a1 == b1 // ctx |- a1 ≈ b1
// ctx |- a2 == b2 // ctx |- a2 ≈ b2
justification new_jst(new destruct_justification(c)); justification new_jst(new destruct_justification(c));
for (unsigned i = 1; i < num_args(a); i++) for (unsigned i = 1; i < num_args(a); i++)
push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst); push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst);
@ -1800,14 +1837,14 @@ class elaborator::imp {
return true; return true;
} }
if (lhs1 == rhs) { if (lhs1 == rhs) {
// ctx |- max(lhs1, lhs2) == rhs // ctx |- max(lhs1, lhs2) ≈ rhs
// ==> IF lhs1 = rhs // ==> IF lhs1 = rhs
// ctx |- lhs2 << rhs // ctx |- lhs2 << rhs
justification new_jst(new normalize_justification(c)); justification new_jst(new normalize_justification(c));
push_active(mk_convertible_constraint(get_context(c), lhs2, rhs, new_jst)); push_active(mk_convertible_constraint(get_context(c), lhs2, rhs, new_jst));
return true; return true;
} else if (lhs2 == rhs && is_type(lhs2)) { } 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 // ==> IF lhs1 = rhs
// ctx |- lhs2 << rhs // ctx |- lhs2 << rhs

203
src/library/simplifier/simplifier.cpp
View file

@ -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) { static expr mk_lambda(name const & n, expr const & d, expr const & b) {
return ::lean::mk_lambda(n, d, 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. 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) { expr translate_eq_proof(expr const & A, expr const & a, expr const & b, expr const & H, expr const & B) {
if (A != 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); return mk_to_eq_th(B, a, b, mk_to_heq_th(A, a, b, H));
} else { else
return H; 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) { 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 // the following two arguments are used only for invoking the simplifier monitor
expr const & e, unsigned i) { expr const & e, unsigned i) {
expr const & A = abst_domain(f_type); expr const & A = abst_domain(f_type);
if (is_TypeU(A)) { expr const & new_A = abst_domain(new_f_type);
if (!is_definitionally_equal(f, new_f)) { expr a_type = infer_type(a);
if (m_monitor) expr new_a_type = infer_type(new_a.m_expr);
m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::Unsupported); if (!is_convertible(new_a_type, new_A)) {
return none_expr(); // can't handle if (m_monitor)
} m_monitor->failed_app_eh(ro_simplifier(m_this), e, i, simplifier_monitor::failure_kind::TypeMismatch);
// The congruence axiom cannot be used in this case. return none_expr(); // failed
// 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 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()) { if (!res_a.is_heq_proof()) {
Hec = ::lean::mk_htrans_th(B, A, A, e, a, c, 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 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 { } else {
Hec = ::lean::mk_htrans_th(B, A, infer_type(c), e, a, c, 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 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) { void ensure_heterogeneous(expr const & lhs, result & rhs) {
if (!rhs.is_heq_proof()) { 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; rhs.m_heq_proof = true;
} }
} }
@ -1141,7 +1075,7 @@ class simplifier_cell::imp {
if (res_bi.is_heq_proof()) { if (res_bi.is_heq_proof()) {
lean_assert(m_use_heq); lean_assert(m_use_heq);
// Using // 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' // (∀ x, f x == f' x) → f == f'
expr new_proof = mk_hsfunext_th(d, // A expr new_proof = mk_hsfunext_th(d, // A
mk_lambda(e, infer_type(abst_body(e))), // B mk_lambda(e, infer_type(abst_body(e))), // B
@ -1153,7 +1087,7 @@ class simplifier_cell::imp {
} else { } else {
expr body_type = infer_type(abst_body(e)); expr body_type = infer_type(abst_body(e));
// Using // 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, 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))); mk_lambda(e, abstract(*res_bi.m_proof, fresh_const)));
return rewrite_lambda(e, result(new_e, new_proof)); 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 // d and new_d are only provably equal, so we need to use hfunext
expr x_old = mk_fresh_const(d); expr x_old = mk_fresh_const(d);
expr x_new = mk_fresh_const(new_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 H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new);
expr bi = instantiate(abst_body(e), x_old); 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); 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)); expr new_e = update_lambda(e, new_d, abstract(new_bi, x_new));
if (!m_proofs_enabled) if (!m_proofs_enabled)
return rewrite(e, result(new_e)); return rewrite(e, result(new_e));
ensure_homogeneous(d, res_d); ensure_heterogeneous(d, res_d);
ensure_heterogeneous(bi, res_bi); ensure_heterogeneous(bi, res_bi);
// Using // Using
// axiom hfunext {A A' : TypeM} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B x} {f' : ∀ x, B' x} : // 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' // 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);
expr new_proof = mk_hfunext_th(d, // A expr new_proof = mk_hfunext_th(d, // A
new_d, // A' new_d, // A'
Fun(x_old, d, infer_type(bi)), // B Fun(x_old, d, infer_type(bi)), // B
Fun(x_new, new_d, infer_type(new_bi)), // B' Fun(x_new, new_d, infer_type(new_bi)), // B'
e, // f e, // f
new_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 // fun (x_old : d) (x_new : new_d) (H : x_old == x_new), bi == new_bi
mk_lambda(abst_name(e), d, mk_lambda(abst_name(e), d,
mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), 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)); lean_assert(is_pi(e) && is_proposition(e));
// We don't support Pi's that are not proposition yet. // We don't support Pi's that are not proposition yet.
// The problem is that // The problem is that
// axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} : // 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) // 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. // 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. // 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 // 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_old = mk_fresh_const(d);
expr x_new = mk_fresh_const(new_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 H_x_old_eq_x_new = mk_fresh_const(x_old_eq_x_new);
expr bi = instantiate(abst_body(e), x_old); 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); 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); m_monitor->failed_abstraction_eh(ro_simplifier(m_this), e, simplifier_monitor::failure_kind::TypeMismatch);
return rewrite(e, result(new_e)); return rewrite(e, result(new_e));
} }
ensure_homogeneous(d, res_d); ensure_heterogeneous(d, res_d);
ensure_homogeneous(bi, res_bi); ensure_homogeneous(bi, res_bi);
// Remark: the argument with type A = A' in hallext and hpiext is actually @eq TypeM A A', // 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 // 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); expr bi_eq_new_bi_proof = get_proof(res_bi);
// Heqb : (∀ x x', x == x' → B x = B' x') // Heqb : (∀ x x', x == x' → B x = B' x')
expr Heqb = mk_lambda(abst_name(e), d, 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(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}), 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})))); abstract(bi_eq_new_bi_proof, {x_old, x_new, H_x_old_eq_x_new}))));
// Using // Using
// theorem hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : // 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) // 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, expr new_proof = mk_hallext_th(d, new_d,
Fun(x_old, d, bi), // B Fun(x_old, d, bi), // B
Fun(x_new, new_d, new_bi), // B' Fun(x_new, new_d, new_bi), // B'
d_eq_new_d_proof, // A = A' *res_d.m_proof, // A == A'
Heqb); Heqb);
return rewrite(e, result(new_e, new_proof)); 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) { result save(expr const & e, result const & r) {
if (m_memoize) { if (m_memoize) {
result new_r = r.update_expr(m_max_sharing(r.m_expr)); 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::Lambda: return save(e, simplify_lambda(e));
case expr_kind::Pi: return save(e, simplify_pi(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::Let: return save(e, simplify(instantiate(let_body(e), let_value(e))));
case expr_kind::HEq: return save(e, simplify_heq(e));
} }
lean_unreachable(); lean_unreachable();
} }

4
tests/lean/loop3.lean
View file

@ -2,11 +2,11 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple

10
tests/lean/rs.lean.expected.out
View file

@ -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_assoc : ∀ a b c : ℕ, a + b + c = a + (b + c)
Nat::add_comm : ∀ a b : ℕ, a + b = b + a Nat::add_comm : ∀ a b : ℕ, a + b = b + a
Nat::add_zeror : ∀ a : ℕ, a + 0 = 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 ↔ ⊤ eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤
exists_rem : ∀ (A : TypeU) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p exists_rem : ∀ (A : (Type U)) (H : inhabited A) (p : Bool), (∃ x : A, p) ↔ p
exists_and_distributel : ∀ (A : TypeU) (p : Bool) (φ : A → Bool), exists_and_distributel : ∀ (A : (Type U)) (p : Bool) (φ : A → Bool),
(∃ x : A, φ x ∧ p) ↔ (∃ x : A, φ x) ∧ p (∃ 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) (∃ x : A, φ x ∨ ψ x) ↔ (∃ x : A, φ x) ∨ (∃ x : A, ψ x)
not_and : ∀ a b : Bool, ¬ (a ∧ b) ↔ ¬ a ∨ ¬ b 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 : (¬ ⊤) = ⊥ not_true : (¬ ⊤) = ⊥
and_comm : ∀ a b : Bool, a ∧ b ↔ b ∧ a and_comm : ∀ a b : Bool, a ∧ b ↔ b ∧ a
and_truer : ∀ a : Bool, a ∧ ⊤ ↔ a and_truer : ∀ a : Bool, a ∧ ⊤ ↔ a

4
tests/lean/simp18.lean
View file

@ -2,11 +2,11 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple

6
tests/lean/simp18.lean.expected.out
View file

@ -14,7 +14,7 @@ v ; (w ; v)
htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n)))) htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n))))
(to_heq (Nat::add_zeror n))) (to_heq (Nat::add_zeror n)))
(htrans (to_heq (concat_empty (v ; w))) (htrans (to_heq (concat_empty (v ; w)))
(cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w)))) (cast_heq (to_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))) (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))) (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)))

7
tests/lean/simp19.lean
View file

@ -2,16 +2,19 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple
add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror : 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 n : Nat
variable v : vec n variable v : vec n
variable w : vec n variable w : vec n

16
tests/lean/simp19.lean.expected.out
View file

@ -5,6 +5,7 @@
Assumed: concat_assoc Assumed: concat_assoc
Assumed: empty Assumed: empty
Assumed: concat_empty Assumed: concat_empty
Defined: TypeM
Assumed: n Assumed: n
Assumed: v Assumed: v
Assumed: w Assumed: w
@ -13,14 +14,15 @@ f (v ; w ; empty ; (v ; empty))
===> ===>
f (v ; (w ; v)) f (v ; (w ; v))
hcongr (hcongr (hrefl @f) hcongr (hcongr (hrefl @f)
(to_heq (subst (refl (vec (n + n + 0 + (n + 0)))) (to_heq (congr2 vec
(congr2 vec (trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n))
(trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n)) (Nat::add_assoc n n n)))))
(Nat::add_assoc n n n))))))
(htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n)))) (htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n))))
(to_heq (Nat::add_zeror n))) (to_heq (Nat::add_zeror n)))
(htrans (to_heq (concat_empty (v ; w))) (htrans (to_heq (concat_empty (v ; w)))
(cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w)))) (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror (n + n)))))
(htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v))) (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))) (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))))

2
tests/lean/simp20.lean
View file

@ -2,6 +2,8 @@ rewrite_set simple
set_option pp::implicit true set_option pp::implicit true
universe M >= 1
definition TypeM := (Type M)
variable g : TypeM → TypeM variable g : TypeM → TypeM
variable B : Type variable B : Type
variable B' : Type variable B' : Type

3
tests/lean/simp20.lean.expected.out
View file

@ -1,6 +1,7 @@
Set: pp::colors Set: pp::colors
Set: pp::unicode Set: pp::unicode
Set: lean::pp::implicit Set: lean::pp::implicit
Defined: TypeM
Assumed: g Assumed: g
Assumed: B Assumed: B
Assumed: B' Assumed: B'
@ -8,5 +9,5 @@
g B g B
===> ===>
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') @eq TypeM (g B) (g B')

7
tests/lean/simp22.lean
View file

@ -2,11 +2,11 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple
@ -15,6 +15,9 @@ rewrite_set simple
-- rewrite set, we prevent the simplifier from reducing the following example -- 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 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 n : Nat
variable v : vec n variable v : vec n
variable w : vec n variable w : vec n

16
tests/lean/simp22.lean.expected.out
View file

@ -5,6 +5,7 @@
Assumed: concat_assoc Assumed: concat_assoc
Assumed: empty Assumed: empty
Assumed: concat_empty Assumed: concat_empty
Defined: TypeM
Assumed: n Assumed: n
Assumed: v Assumed: v
Assumed: w Assumed: w
@ -18,14 +19,15 @@ f (v ; w ; empty ; (v ; empty))
===> ===>
f (v ; (w ; v)) f (v ; (w ; v))
hcongr (hcongr (hrefl @f) hcongr (hcongr (hrefl @f)
(to_heq (subst (refl (vec (n + n + 0 + (n + 0)))) (to_heq (congr2 vec
(congr2 vec (trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n))
(trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n)) (Nat::add_assoc n n n)))))
(Nat::add_assoc n n n))))))
(htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n)))) (htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n))))
(to_heq (Nat::add_zeror n))) (to_heq (Nat::add_zeror n)))
(htrans (to_heq (concat_empty (v ; w))) (htrans (to_heq (concat_empty (v ; w)))
(cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w)))) (cast_heq (to_heq (congr2 vec (symm (Nat::add_zeror (n + n)))))
(htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v))) (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))) (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))))

9
tests/lean/simp23.lean
View file

@ -2,16 +2,19 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple
add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror and_truer eq_id : 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 n : Nat
variable v : vec n variable v : vec n
variable w : vec n variable w : vec n
@ -22,7 +25,7 @@ add_rewrite fax : simple
(* (*
local opts = options({"simplifier", "heq"}, true) 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(t)
print("===>") print("===>")
local t2, pr = simplify(t, "simple", opts) local t2, pr = simplify(t, "simple", opts)

6
tests/lean/simp23.lean.expected.out
View file

@ -5,14 +5,16 @@
Assumed: concat_assoc Assumed: concat_assoc
Assumed: empty Assumed: empty
Assumed: concat_empty Assumed: concat_empty
Defined: TypeM
Assumed: n Assumed: n
Assumed: v Assumed: v
Assumed: w Assumed: w
Assumed: f Assumed: f
Assumed: p Assumed: p
Assumed: fax 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)) p (v ; (w ; v))
checking proof 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)))

7
tests/lean/simp28.lean
View file

@ -2,11 +2,11 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple
@ -35,6 +35,9 @@ get_environment():type_check(pr)
print "" print ""
universe M >= 1
definition TypeM := (Type M)
variable lheq {A B : TypeM} : A → B → Bool variable lheq {A B : TypeM} : A → B → Bool
infixl 50 === : lheq infixl 50 === : lheq
(* (*

1
tests/lean/simp28.lean.expected.out
View file

@ -9,6 +9,7 @@
Assumed: f Assumed: f
λ n : ℕ, f λ n : ℕ, f
Defined: TypeM
Assumed: lheq Assumed: lheq
λ 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
=====> =====>

4
tests/lean/simp30.lean
View file

@ -2,11 +2,11 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple

4
tests/lean/simp32.lean
View file

@ -2,11 +2,11 @@ variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : 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)) (v1 ; (v2 ; v3))
variable empty : vec 0 variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) : 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 v
rewrite_set simple rewrite_set simple

7
tests/lean/simp32.lean.expected.out
View file

@ -6,9 +6,6 @@
Assumed: empty Assumed: empty
Assumed: concat_empty Assumed: concat_empty
Assumed: f 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 λ val : ℕ, f == (λ v : vec val, v)
Kind: 0
-----------
λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val