Some notations updates

encodings/subtype_poly.lp

@@ -8,10 +8,10 @@ require open personoj.encodings.prenex
 set declared "μ"
 set declared "μ₀"
 set declared "π"
-set declared "↑"
+set declared "⇑"
 set declared "↓"
 
-// Maximal supertype
+// Top type
 symbol μ: Set → Set
 rule μ (psub {$T} _) ↪ μ $T
 with μ ($T ~> $U) ↪ $T ~> (μ $U)
@@ -20,52 +20,52 @@ with μ (arrd $b) ↪ arrd (λx, μ ($b x))
 with μ (μ $T) ↪ μ $T // FIXME: can be proved
 
 symbol π (T: Set): η (μ T) → Bool
+rule π ($t ~> $u) ↪ λx: η $t → η (μ $u), ∀ (λy, π $u (x y))
+with π (tuple_t $t $u)
+   ↪ λx: η (tuple_t (μ $t) (μ $u)), π $t (p1 x) ∧ (λ_, π $u (p2 x))
+with π (arrd $b)
+   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π ($b y) (x y))
 
 // Casting from/to maximal supertype
-symbol maxcast {t: Set}: η t → η (μ t)
+symbol topcast {t: Set}: η t → η (μ t)
 symbol downcast {t: Set} (x: η (μ t)): ε (π t x) → η t
-definition ↑ {t} ≔ maxcast {t}
+definition ⇑ {t} ≔ topcast {t}
 definition ↓ {t} ≔ downcast {t}
-symbol _downcast {t: Set}: η (μ t) → η t
-rule downcast {$t} $x _ ↪ _downcast {$t} $x
+symbol downcast_ {t: Set}: η (μ t) → η t // Proof irrelevant downcast
+rule downcast {$t} $x _ ↪ downcast_ {$t} $x
 
-rule π ($t ~> $u) ↪ λx: η $t → η (μ $u), ∀ (λy, π $u (x y))
-with π (tuple_t $t $u)
-   ↪ λx: η (tuple_t (μ $t) (μ $u)), π $t (p1 x) ∧ (λ_, π $u (p2 x))
-with π (psub {$t} $a)
+rule π (psub {$t} $a)
    ↪ λx: η (μ $t), (π $t x) ∧ (λy: ε (π $t x), $a (↓ x y))
-with π (arrd $b)
-   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π ($b y) (x y))
 
 /// A term ‘x’ that has been cast up still validates the properties to be of its
 /// former type.
-symbol cstr_maxcast_idem: ε (∀B (λt, ∀ {t} (λx, π t (maxcast x))))
+symbol cstr_topcast_idem: ε (∀B (λt, ∀ {t} (λx, π t (topcast x))))
 // or as a rewrite-rule:
-// rule ε (π _ (maxcast _)) ↪ ε true
+// rule ε (π _ (topcast _)) ↪ ε true
 
-private constant symbol max_eq: Set → Set → Bool
-set infix 6 "≃" ≔ max_eq
+private constant symbol top_eq: Set → Set → Bool
+set infix 6 "≃" ≔ top_eq
 
 // fr and to must be supertypes
 symbol eqcast {fr: Set} {to: Set}: ε (fr ≃ to) → η (μ fr) → η (μ to)
-protected symbol _eqcast {fr: Set} {to: Set}: η (μ fr) → η (μ to)
-rule eqcast {$fr} {$to} _ $e ↪ _eqcast {$fr} {$to} $e
-rule _eqcast {$t} {$t} $e ↪ $e
+protected symbol eqcast_ {fr: Set} {to: Set}: η (μ fr) → η (μ to)
+rule eqcast {$fr} {$to} _ $e ↪ eqcast_ {$fr} {$to} $e
+rule eqcast_ {$t} {$t} $e ↪ $e
 
 definition compatible (t u: Set) ≔ μ t ≃ μ u
 set infix 6 "~" ≔ compatible
 
 // The one true cast
 symbol cast {fr_t: Set} (to_t: Set) (comp: ε (fr_t ~ to_t)) (m: η fr_t):
-  ε (π to_t (eqcast comp (maxcast m))) → η to_t
+  ε (π to_t (eqcast comp (topcast m))) → η to_t
 
 /// Proof irrelevance
-protected symbol _cast {fr_t: Set} (to_t: Set): η fr_t → η to_t
-rule cast {$f_t} $t_t _ $x _ ↪ _cast {$f_t} $t_t $x
-rule _cast {$t} $t $x ↪ $x // REVIEW: critical pairs?
-rule _cast {$fr_t} $to_t $e
-   ↪ _downcast {$to_t} (_eqcast {$fr_t} {$to_t} (↑ {$fr_t} $e))
-// REVIEW: we can directly rewrite cast to _downcast and maxcast, dropping
+protected symbol cast_ {fr_t: Set} (to_t: Set): η fr_t → η to_t
+rule cast {$f_t} $t_t _ $x _ ↪ cast_ {$f_t} $t_t $x
+rule cast_ {$t} $t $x ↪ $x // REVIEW: critical pairs?
+rule cast_ {$fr_t} $to_t $e
+   ↪ downcast_ {$to_t} (eqcast_ {$fr_t} {$to_t} (⇑ {$fr_t} $e))
+// REVIEW: we can directly rewrite cast to _downcast and topcast, dropping
 // _cast
 
 theorem comp_same_cstr_cast
@@ -75,11 +75,11 @@ theorem comp_same_cstr_cast
                   (π fr)
                   (λx, π to (eqcast comp x))))
         (x: η fr)
-      : ε (π to (eqcast comp (maxcast x)))
+      : ε (π to (eqcast comp (topcast x)))
 proof
   assume fr to comp eq_cstr x
-  refine eq_cstr (λf, f (maxcast x)) _
-  refine cstr_maxcast_idem fr x
+  refine eq_cstr (λf, f (topcast x)) _
+  refine cstr_topcast_idem fr x
 qed
 
 rule ε ($t ≃ $t) ↪ ε true

paper/rat_poly.lp

@@ -9,8 +9,8 @@ set infix right 2 "⇒" ≔ imp
 constant symbol rat: Set
 rule π rat ↪ λ_, true
 rule μ rat ↪ rat
-rule maxcast {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:
@@ -52,8 +52,8 @@ 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_ rat (s $m))
    ↪ cast {nat} rat (λx, x)
           (s (cast {rat} nat (λx, x)
                    ((cast {nat} rat (λx, x) $n (λx, x))
@@ -146,3 +146,15 @@ admit
 //                 (times (cast {nznat} rat (λx, x) $b (λx, x))
 //                        (cast {nznat} rat (λx, x) $d (λx, x)))
 //                 (tcc3 $b $d))
+
+theorem tcc6: ε (and true (λ_, nat_p z))
+proof
+admit
+definition one ≔ s (cast nat (λx, x) z tcc6)
+// FIXME: same as above
+// theorem tcc7: ε (and true
+//                      (λ_, and (nat_p (cast rat (λx, x) one (λx, x)))
+//                               (λ_, nznat_p one)) )
+// proof
+// admit
+// definition one_nz ≔ cast nznat (λx, x) one tcc7