keeping the eqcast

encodings/subtype_poly.lp

@@ -31,9 +31,8 @@ with π (arrd $b)
 symbol topcast {t: Set}: η t → η (μ t)
 definition ⇑ {t} ≔ topcast {t}
 
-private symbol top_comp: Set → Set → Bool
+symbol top_comp: Set → Set → Bool
 set infix 6 "≃" ≔ top_comp
-rule $t ≃ $t ↪ true
 
 definition compatible (t u: Set) ≔ μ t ≃ μ u
 set infix 6 "~" ≔ compatible
@@ -43,6 +42,7 @@ set infix 6 "~" ≔ compatible
 symbol eqcast {t: Set} (u: Set): ε (t ~ u) → η (μ t) → η (μ u)
 symbol eqcast_ {t: Set} (u: Set): η (μ t) → η (μ u) // Proof irrelevant
 rule eqcast {$t} $u _ $m ↪ eqcast_ {$t} $u $m
+rule eqcast_ {$t} $t $x ↪ $x
 
 // Casting from/to maximal supertype
 symbol downcast (t: Set) (x: η (μ t)): ε (π t x) → η t
@@ -50,6 +50,8 @@ definition ↓ t ≔ downcast t
 symbol downcast_ (t: Set): η (μ t) → η t
 rule downcast $t $x _ ↪ downcast_ $t $x
 
+rule downcast_ $t (eqcast_ _ (topcast {$t} $x)) ↪ $x
+
 rule π (psub {$t} $a)
    ↪ λx: η (μ $t), (π $t x) ∧ (λy: ε (π $t x), $a (↓ $t x y))
 
@@ -84,14 +86,14 @@ rule ($t1 ~> $u1) ≃ ($t2 ~> $u2)
         (eq {μ $t1 ~> bool} (π $t1)
             (λx: η (μ $t1), π $t2 (@eqcast $t1 $t2 h x)))
         ∧ (λ_, $u1 ≃ $u2))
-rule ε (tuple_t $t1 $u1 ≃ tuple_t $t2 $u2)
-   ↪ ε ($t1 ≃ $t2 ∧ (λ_, $u1 ≃ $u2))
-with ε ((arrd {$t1} $u1) ≃ (arrd {$t2} $u2))
-   ↪ ε ((μ $t1 ≃ μ $t2)
-        ∧ (λh,
-           (eq {μ $t1 ~> bool} (π $t1) (λx, π $t2 (@eqcast $t1 $t2 h x)))
-           ∧ (λh', ∀
-               (λx: η $t1,
-                ($u1 x) ≃ ($u2 (cast {$t1} $t2 h x
-                                               (comp_same_cstr_cast
-                                                $t1 $t2 h h' x)))))))
+rule tuple_t $t1 $u1 ≃ tuple_t $t2 $u2
+   ↪ $t1 ≃ $t2 ∧ (λ_, $u1 ≃ $u2)
+with (arrd {$t1} $u1) ≃ (arrd {$t2} $u2)
+   ↪ (μ $t1 ≃ μ $t2)
+     ∧ (λh,
+        (eq {μ $t1 ~> bool} (π $t1) (λx, π $t2 (@eqcast $t1 $t2 h x)))
+        ∧ (λh', ∀
+            (λx: η $t1,
+             ($u1 x) ≃ ($u2 (cast {$t1} $t2 h x
+                                            (comp_same_cstr_cast
+                                             $t1 $t2 h h' x))))))

paper/rat_poly.lp

@@ -9,8 +9,8 @@ set infix right 2 "⇒" ≔ imp
 constant symbol rat: Set
 rule π rat ↪ λ_, true
 rule μ rat ↪ rat
-rule topcast {rat} $x ↪ $x
-rule downcast_ {rat} $e ↪ $e
+// rule topcast {rat} $x ↪ $x
+// rule downcast_ rat $e ↪ $e
 
 constant symbol z: η rat
 
@@ -33,7 +33,7 @@ constant symbol s_not_z:
   ε (∀ {nat} (λx, ¬ (z = (cast rat (λx, x) (s x) (λx, x)))))
 
 rule ε (z = z) ↪ ε true
-rule ε ((cast_ rat (s $n)) = (cast_ rat (s $m)))
+rule ε ((cast rat _ (s $n) _) = (cast rat _ (s $m) _))
    ↪ ε ((cast rat (λx, x) $n (λx, x)) = (cast rat (λx, x) $m (λx, x)))
 
 theorem plus_closed_nat:
@@ -46,20 +46,20 @@ admit
 theorem tcc1:
   ε (∀ {nat} (λn, (∀ {nat}
                      (λm, true
-                          ∧ (λ_, nat_p ((cast rat (λx, x) n (λx, x))
-                                        + (cast rat (λx, x) m (λx, x))))))))
+                          ∧ (λ_, nat_p (plus (cast rat (λx, x) n (λx, x))
+                                             (cast rat (λx, x) m (λx, x))))))))
 proof
 admit
 
 set flag "print_implicits" on
-rule (cast_ {nat} rat $n) + z ↪ cast rat (λx, x) $n (λx, x)
-with (cast_ {nat} rat $n) + (cast_ rat (s $m))
+rule (cast {nat} rat _ $n _) + z ↪ cast rat (λx, x) $n (λx, x)
+with (cast {nat} rat _ $n _) + (cast {nat} rat _ (s $m) _)
    ↪ cast {nat} rat (λx, x)
           (s (cast {rat} nat (λx, x)
-                   ((cast {nat} rat (λx, x) $n (λx, x))
-                    + (cast {nat} rat (λx, x) $m (λx, x)))
+                   (plus (cast {nat} rat (λx, x) $n (λx, x))
+                         (cast {nat} rat (λx, x) $m (λx, x)))
               (tcc1 $n $m)))
-     (λx, x)
+          (λx, x)
 
 theorem tcc2: ε (true ∧ (λ_, nat_p z))
 proof