New encoding for subtyping

encodings/subtyping.lp

+/// Sub-type polymorphism
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
+require open personoj.encodings.tuple
+require open personoj.encodings.pairs
+require open personoj.encodings.prenex
+
+// Returns the top type of any type
+symbol Pull: Set → Set
+rule Pull (psub {$T} _) ↪ Pull $T
+with Pull bool ↪ bool
+
+// [pull {t} m] pulls term [t] from its type [t] to the top-type [Pull t]
+symbol pull {t: Set} (_: El t): El (Pull t)
+rule pull {psub _} $m ↪ pull (fst $m)
+with pull bool $x ↪ $x
+
+// [Comp t u] can be inhabited only if [t] and [u] are convertible top types.
+constant symbol Comp : Set → Set → TYPE
+constant symbol CompRefl : Π(t: Set), Comp t t
+definition Equivalent A B ≔ Comp (Pull A) (Pull B)
+
+// [Dive t m] generates the proposition gathering all the predicate
+// on the path to type [t].
+symbol Dive (t: Set) (_: El (Pull t)): Bool
+// [dive t m h] types term [m: El (Pull t)] as [El t], with [h] the proof that
+// [m] validates all predicates generated by [Dive t m]. Proof irrelevant in
+// [h].
+protected symbol dive_ (t: Set) (_: El (Pull t)): El t
+definition dive (t: Set) (m: El (Pull t)) (_: Prf (Dive t m)) ≔ dive_ t m
+
+// Actual computation of [Dive]
+rule Dive (psub {$t} $a) $x
+   ↪ (Dive $t $x) ∧ (λy: Prf (Dive $t $x), $a (dive $t $x y))
+
+protected symbol transfer_ (t: Set) (u: Set) (_: El t): El u
+definition transfer (t: Set) (u: Set) (_: Comp t u) (m: El t) ≔ transfer_ t u m
+
+// symbol cast {fr_t: Set} (to_t: Set)
+//             (comp: Equivalent fr_t to_t) (m: El fr_t)
+//             (_: Prf (Dive to_t (transfer (Pull fr_t) (Pull to_t) comp (pull m))))
+//      : El to_t
+
+definition cast {fr_t: Set} (to_t: Set)
+                (comp: Equivalent fr_t to_t) (m: El fr_t)
+                (tcc: Prf (Dive to_t (transfer (Pull fr_t) (Pull to_t)
+                                               comp (pull m))))
+         ≔ dive to_t (transfer (Pull fr_t) (Pull to_t) comp (pull m)) tcc
+
+// [below t a m h] provides a proof that [m] validates all predicates up to type
+// [t] given that [h] is a proof that [m] validates all predicates up  to type
+// [{x: t | a}].
+symbol below (t: Set) (a: El t → Bool) (m: El (Pull t))
+             (_: Prf (Dive (psub {t} a) m))
+     : Prf (Dive t m)
+// TODO: use a theorem
+
+symbol top (t: Set) (a: El t → Bool) (m: El (Pull t))
+           (h: Prf (Dive (psub {t} a) m))
+     : Prf (a (dive t m (below t a m h)))
+// TODO: use a theorem
+
+// Rewrite casts to projections
+// rule cast {$fr} (psub {$t} $p) $comp $m $h
+//    ↪ let mtop: El (Pull $t) ≔ transfer (Pull $fr) (Pull $t) $comp (pull $m) in
+//      @pair $t $p (@cast $fr $t $comp $m (below $t $p mtop $h))
+//                  (top $t $p mtop $h)
+
+// Using definition line 40 (cast as a new symbol), we obtain the constraint
+// [$p (dive $t mtop (below $t $p mtop $h)) ≡
+//    $p (cast $t $comp $m (below $t $p mtop $h))]
+// which should be solved by defining the cast in function of [dive], [pull] &c.
+// and writing the rule directly on [dive]