fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall

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

src/builtin/cast.lean

@@ -1,24 +1,80 @@
 -- "Type casting" library.
 
+-- Heterogeneous substitution
+axiom hsubst {A B : TypeU} {a : A} {b : B} (P : ∀ (T : TypeU), T -> Bool) : P A a → a == b → P B b
+
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
+
+-- 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
+
+-- 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
+
+-- 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
+
 -- 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 : (Type U)} : A == B → A → B.
+variable cast {A B : TypeU} : A == B → A → B
 
 -- The CastEq axiom states that for any cast of x is equal to x.
-axiom cast::eq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x.
+axiom cast::eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x
 
 -- The CastApp axiom "propagates" the cast over application
-axiom cast::app {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
+axiom cast::app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU}
-              (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : A == A')
+                (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : A == A')
-              (f : ∀ x : A, B x) (x : A) :
+                (f : ∀ x : A, B x) (x : A) :
-    cast H1 f (cast H2 x) == f x.
+    cast H1 f (cast H2 x) == f x
 
+-- Heterogeneous congruence
+theorem hcongr
+            {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM}
+            {f : ∀ x : A, B x} {g : ∀ x : A', 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 : A', B' x) == (∀ x : A, B x) := symm (type::eq H1),
+       g' : (∀ x : A, 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
+
+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'.
+      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
 
--- If two (dependent) function spaces are equal, then their ranges are equal.
-axiom raninj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
-             (H : (∀ x : A, B x) == (∀ x : A', B' x)) (a : A) :
-    B a == B' (cast (dominj H) a).

src/builtin/kernel.lean

@@ -45,26 +45,23 @@ definition neq {A : TypeU} (a b : A) : Bool
 
 infix 50 ≠ : neq
 
-axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
-
 axiom refl {A : TypeU} (a : A) : a == a
 
 axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b
 
-definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
-:= subst H1 H2
-
-axiom eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
-
 axiom iff::intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a == b
 
 axiom abst {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x == g x) : f == g
 
 axiom abstpi {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x)
 
-axiom hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a
+axiom eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
 
-axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
+axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
+
+-- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
+definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
+:= subst H1 H2
 
 theorem trivial : true
 := refl true
@@ -189,7 +186,7 @@ theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H :
 -- because the types are not definitionally equal
 
 theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
-:= htrans (congr2 f H2) (congr1 b H1)
+:= subst (congr2 f H2) (congr1 b H1)
 
 -- Remark: the existential is defined as (¬ (forall x : A, ¬ P x))
 

tests/lean/cast2.lean

@@ -5,8 +5,3 @@ variable A' : Type
 variable B' : Type
 axiom H : (A -> B) = (A' -> B')
 variable a : A
-check dominj H
-theorem BeqB' : B = B' := raninj H a
-set::option pp::implicit true
-print dominj H
-print raninj H a

tests/lean/cast2.lean.expected.out

@@ -7,8 +7,3 @@
   Assumed: B'
   Assumed: H
   Assumed: a
-dominj H : A == A'
-  Proved: BeqB'
-  Set: lean::pp::implicit
-@dominj A A' (λ x : A, B) (λ x : A', B') H
-@raninj A A' (λ x : A, B) (λ x : A', B') H a

tests/lean/cast4.lean

@@ -1,8 +1,5 @@
 import cast
 set::option pp::colors false
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (B   : A -> TypeM)
@@ -11,20 +8,6 @@ check fun (A A': TypeM)
           (g   : forall x : A', B' x)
           (a   : A)
           (b   : A')
-          (H1  : (forall x : A, B x) == (forall x : A', B' x))
           (H2  : f == g)
           (H3  : a == b),
-    let
+     hcongr H2 H3
-        S1 : (forall x : A', B' x) == (forall x : A, B x) := symm H1,
-        L2 : A' == A                              := dominj S1,
-        b' : A                                    := cast L2 b,
-        L3 : b  == b'                             := cast::eq L2 b,
-        L4 : a == b'                              := htrans H3 L3,
-        L5 : f a == f b'                          := congr2 f L4,
-        g' : (forall x : A, B x)                      := cast S1 g,
-        L6 : g == g'                              := cast::eq S1 g,
-        L7 : f == g'                              := htrans H2 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

tests/lean/cast4.lean.expected.out

@@ -2,7 +2,6 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
-  Defined: TypeM
 λ (A A' : TypeM)
   (B : A → TypeM)
   (B' : A' → TypeM)
@@ -10,22 +9,9 @@
   (g : ∀ x : A', B' x)
   (a : A)
   (b : A')
-  (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
   (H2 : f == g)
   (H3 : a == b),
-  let S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm H1,
+  hcongr H2 H3 :
-      L2 : A' == A := dominj S1,
-      b' : A := cast L2 b,
-      L3 : b == b' := cast::eq L2 b,
-      L4 : a == b' := htrans H3 L3,
-      L5 : f a == f b' := congr2 f L4,
-      g' : ∀ x : A, B x := cast S1 g,
-      L6 : g == g' := cast::eq S1 g,
-      L7 : f == g' := htrans H2 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 :
     ∀ (A A' : TypeM)
       (B : A → TypeM)
       (B' : A' → TypeM)
@@ -33,4 +19,4 @@
       (g : ∀ x : A', B' x)
       (a : A)
       (b : A'),
-      (∀ x : A, B x) == (∀ x : A', B' x) → f == g → a == b → f a == g b
+      f == g → a == b → f a == g b

tests/lean/eq3.lean

@@ -1,3 +1,4 @@
+import cast
 variable Vector : Nat -> Type
 variable n  : Nat
 variable v1 : Vector n

tests/lean/eq3.lean.expected.out

@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'cast'
   Assumed: Vector
   Assumed: n
   Assumed: v1

tests/lean/mod1.lean.expected.out

@@ -2,5 +2,5 @@
   Set: pp::unicode
   Imported 'cast'
   Imported 'cast'
-@cast : ∀ (A B : (Type U)), A == B → A → B
+@cast : ∀ (A B : TypeU), A == B → A → B
-@cast : ∀ (A B : (Type U)), A == B → A → B
+@cast : ∀ (A B : TypeU), A == B → A → B

tests/lean/norm_bug1.lean

@@ -1,8 +1,5 @@
 import cast
 set::option pp::colors false
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)
@@ -19,10 +16,9 @@ check fun (A A': TypeM)
           (g   : forall x : A', B' x)
           (a   : A)
           (b   : A')
-          (H1  : (forall x : A, B x) == (forall x : A', B' x))
           (H2  : f == g)
           (H3  : a == b),
-    let L1 : A  == A'               := dominj H1,
+    let L1 : A  == A'               := type::eq H3,
         L2 : A' == A                := symm L1,
         b' : A                      := cast L2 b,
         L3 : b  == b'               := cast::eq L2 b,

tests/lean/norm_bug1.lean.expected.out

@@ -2,7 +2,6 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
-  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
@@ -12,10 +11,9 @@
   (g : ∀ x : A', B' x)
   (a : A)
   (b : A')
-  (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
   (H2 : f == g)
   (H3 : a == b),
-  let L1 : A == A' := dominj H1,
+  let L1 : A == A' := type::eq H3,
       L2 : A' == A := symm L1,
       b' : A := cast L2 b,
       L3 : b == b' := cast::eq L2 b,
@@ -29,5 +27,6 @@
       (g : ∀ x : A', B' x)
       (a : A)
       (b : A')
-      (H1 : (∀ x : A, B x) == (∀ x : A', B' x)),
+      (H2 : f == g)
-      f == g → a == b → f a == f (cast (symm (dominj H1)) b)
+      (H3 : a == b),
+      f a == f (cast (symm (type::eq H3)) b)

tests/lean/type_inf_bug1.lean

@@ -1,8 +1,5 @@
 import cast
 set::option pp::colors false
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)
@@ -22,7 +19,7 @@ check fun (A A': TypeM)
           (H1  : (forall x : A, B x) == (forall x : A', B' x))
           (H2  : f == g)
           (H3  : a == b),
-    let L1 : A  == A'                             := dominj H1,
+    let L1 : A  == A'                             := type::eq H3,
         L2 : A' == A                              := symm L1,
         b' : A                                    := cast L2 b,
         L3 : b  == b'                             := cast::eq L2 b,

tests/lean/type_inf_bug1.lean.expected.out

@@ -2,7 +2,6 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
-  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
@@ -15,7 +14,7 @@
   (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
   (H2 : f == g)
   (H3 : a == b),
-  let L1 : A == A' := dominj H1,
+  let L1 : A == A' := type::eq H3,
       L2 : A' == A := symm L1,
       b' : A := cast L2 b,
       L3 : b == b' := cast::eq L2 b,
@@ -35,5 +34,7 @@
       (g : ∀ x : A', B' x)
       (a : A)
       (b : A')
-      (H1 : (∀ x : A, B x) == (∀ x : A', B' x)),
+      (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
-      f == g → a == b → f a == cast (symm H1) g (cast (symm (dominj H1)) b)
+      (H2 : f == g)
+      (H3 : a == b),
+      f a == cast (symm H1) g (cast (symm (type::eq H3)) b)