feat(builtin/cast): use heq in the cast library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/CMakeLists.txt

@@ -93,7 +93,8 @@ add_theory("if_then_else.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
 add_theory("Int.lean"          "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean")
 add_theory("Real.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
 add_theory("specialfn.lean"    "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
-## add_theory("cast.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
+add_theory("heq.lean"          "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
+add_theory("cast.lean"         "${CMAKE_CURRENT_BINARY_DIR}/heq.olean")
 
 update_interface("kernel.olean"       "kernel" "-n")
 update_interface("Nat.olean"          "library/arith" "-n")

src/builtin/cast.lean

@@ -1,90 +1,35 @@
--- "Type casting" library.
+import heq
 
--- Heterogeneous substitution
-axiom hsubst {A B : TypeU} {a : A} {b : B} (P : ∀ T : TypeU, T → Bool) : P A a → a == b → P B b
+variable cast {A B : TypeH} : A = B → A → B
 
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
+axiom cast_heq {A B : TypeH} (H : A = B) (a : A) : cast H a == a
 
--- Type equality axiom, if two values are equal, then their types are equal
-theorem type_eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B
-:= hsubst (λ (T : TypeU) (x : T), A == T) (refl A) H
+theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} (f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) :
+      cast Hb f (cast Ha a) == f a
+:= let s1 : cast Hb f == f  := cast_heq Hb f,
+       s2 : cast Ha a == a  := cast_heq Ha a
+   in hcongr s1 s2
 
--- Heterogenous symmetry
-theorem hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a
-:= hsubst (λ (T : TypeU) (x : T), x == a) (refl a) H
+-- The following theorems can be used as rewriting rules
 
--- Heterogenous transitivity
-theorem htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
-:= hsubst (λ (T : TypeU) (x : T), a == x) H1 H2
+theorem cast_eq {A : TypeH} (H : A = A) (a : A) : cast H a = a
+:= to_eq (cast_heq H a)
 
--- The cast operator allows us to cast an element of type A
--- into B if we provide a proof that types A and B are equal.
-variable cast {A B : TypeU} : A == B → A → B
+theorem cast_trans {A B C : TypeH} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
+:= let s1 : cast Hbc (cast Hab a)  == cast Hab a              :=  cast_heq Hbc (cast Hab a),
+       s2 : cast Hab a             == a                       :=  cast_heq Hab a,
+       s3 : cast (trans Hab Hbc) a == a                       :=  cast_heq (trans Hab Hbc) a,
+       s4 : cast Hbc (cast Hab a)  == cast (trans Hab Hbc) a  :=  htrans (htrans s1 s2) (hsymm s3)
+   in to_eq s4
 
--- The CastEq axiom states that for any cast of x is equal to x.
-axiom cast_eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x
+theorem cast_pull {A : TypeH} {B B' : A → TypeH} (f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) :
+      cast Hb f a = cast Hba (f a)
+:= let s1 : cast Hb f a    == f a    :=  hcongr (cast_heq Hb f) (hrefl a),
+       s2 : cast Hba (f a) == f a    :=  cast_heq Hba (f a)
+   in to_eq (htrans s1 (hsymm s2))
 
--- The CastApp axiom "propagates" the cast over application
-axiom cast_app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU}
-                (H1 : (∀ x, B x) == (∀ x, B' x)) (H2 : A == A')
-                (f : ∀ x, B x) (x : A) :
-    cast H1 f (cast H2 x) == f x
 
--- Heterogeneous congruence
-theorem hcongr
-            {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM}
-            {f : ∀ x, B x} {g : ∀ x, B' x} {a : A} {b : A'}
-            (H1 : f == g)
-            (H2 : a == b)
-         : f a == g b
-:= let L1 : A  == A'                    := type_eq H2,
-       L2 : A' == A                     := symm L1,
-       b' : A                           := cast L2 b,
-       L3 : b == b'                     := cast_eq L2 b,
-       L4 : a == b'                     := htrans H2 L3,
-       L5 : f a == f b'                 := congr2 f L4,
-       S1 : (∀ x, B' x) == (∀ x, B x)  := symm (type_eq H1),
-       g' : (∀ x, B x)                  := cast S1 g,
-       L6 : g == g'                     := cast_eq S1 g,
-       L7 : f == g'                     := htrans H1 L6,
-       L8 : f b' == g' b'               := congr1 b' L7,
-       L9 : f a == g' b'                := htrans L5 L8,
-      L10 : g' b' == g b                := cast_app S1 L2 g b
-   in htrans L9 L10
 
-theorem hfunext
-     {A : TypeM} {B B' : A → TypeM} {f : ∀ x : A, B x} {g : ∀ x : A, B' x} (H : ∀ x : A, f x == g x) : f == g
-:= let L1   : (∀ x : A, B x = B' x)             := λ x : A, type_eq (H x),
-       L2   : (∀ x : A, B x) = (∀ x : A, B' x) := allext L1,
-       g'   : (∀ x : A, B x)                    := cast (symm L2) g,
-       Hgg  : g == g'                            := cast_eq (symm L2) g,
-       Hggx : (∀ x : A, g x == g' x)            := λ x : A, hcongr Hgg (refl x) ,
-       L3   : (∀ x : A, f x == g' x)            := λ x : A, htrans (H x) (Hggx x),
-       Hfg  : f == g'                            := funext L3
-   in htrans Hfg (hsymm Hgg)
 
-exit -- Stop here, the following axiom is not sound
 
--- The following axiom is unsound when we treat Pi and
--- forall as the "same thing". The main problem is the
--- rule that says (Pi x : A, B) has type Bool if B has type Bool instead of
--- max(typeof(A), typeof(B))
---
--- Here is the problematic axiom
--- If two (dependent) function spaces are equal, then their domains are equal.
-axiom dominj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
-             (H : (∀ x : A, B x) == (∀ x : A', B' x)) :
-      A == A'
 
--- Here is a derivation of false using the dominj axiom
-theorem unsat : false :=
-let L1 : (∀ x : true, true)                         := (λ x : true,  trivial),
-    L2 : (∀ x : false, true)                        := (λ x : false, trivial),
-    -- When we keep Pi/forall as different things, the following two steps can't be used
-    L3 : (∀ x : true, true) = true                  := eqt_intro L1,
-    L4 : (∀ x : false, true) = true                 := eqt_intro L2,
-    L5 : (∀ x : true, true) = (∀ x : false, true)   := trans L3 (symm L4),
-    L6 : true = false                               := dominj L5
-in L6

src/builtin/heq.lean

@@ -8,13 +8,13 @@ universe H ≥ 1
 universe U ≥ H + 1
 definition TypeH := (Type H)
 
-axiom heq_eq {A : TypeH} (a : A) : a == a ↔ a = a
+axiom heq_eq {A : TypeH} (a b : A) : a == b ↔ a = b
 
-definition to_eq {A : TypeH} {a : A} (H : a == a) : a = a
-:= (heq_eq a) ◂ H
+definition to_eq {A : TypeH} {a b : A} (H : a == b) : a = b
+:= (heq_eq a b) ◂ H
 
-definition to_heq {A : TypeH} {a : A} (H : a = a) : a == a
-:= (symm (heq_eq a)) ◂ H
+definition to_heq {A : TypeH} {a b : A} (H : a = b) : a == b
+:= (symm (heq_eq a b)) ◂ H
 
 theorem hrefl {A : TypeH} (a : A) : a == a
 := to_heq (refl a)
@@ -34,15 +34,3 @@ axiom hpiext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} :
 
 axiom hallext {A A' : TypeH} {B : A → Bool} {B' : A' → Bool} :
       A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)
-
-variable cast {A B : TypeH} : A = B → A → B
-
-axiom cast_eq {A B : TypeH} (H : A = B) (a : A) : a == cast H a
-
-theorem cast_app {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {a : A} (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) :
-      cast Hb f (cast Ha a) == f a
-:= let s1 : cast Hb f == f  := hsymm (cast_eq Hb f),
-       s2 : cast Ha a == a  := hsymm (cast_eq Ha a)
-   in hcongr s1 s2
-
-