Computing on dive

encodings/subtyping.lp

@@ -9,12 +9,10 @@ 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
@@ -25,22 +23,53 @@ definition Equivalent A B ≔ Comp (Pull A) (Pull B)
 // 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
+// [m] validates all predicates generated by [Dive t m]. It rewrites to a
+// succession of pairs, given a reduction rule below. Proof irrelevant in
+// [h] thanks to the reduction into pairs.
+symbol dive (t: Set) (m: El (Pull t)) (_: Prf (Dive t m)): El t
 
 // 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
+/// The two theorems below are needed to split the tccs generated by [dive]
+/// into 2: the tcc of the top, and all tccs below it. Let [P] be the TCC
+/// generated by [dive], then, morally, [P = below P ∧ top P].
 
-// 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
+// [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}].
+theorem below:
+  Prf
+  (∀B (λt,
+   ∀ {t ~> bool} (λa,
+   ∀ {Pull t} (λm,
+     Dive (psub {t} a) m ⊃ (λ_, Dive t m)))))
+proof
+  // Is mainly the application of the elimination of "and" since
+  // [Dive (psub a) m] rewrites to [Dive t m ∧ a (dive t m h)]
+admit
+
+// [top t a m h] provides a proof that [m] validates the tcc [a] so that
+// [m] given a proof [h] that [m] can be typed as [psub a].
+theorem top:
+  Prf
+  (∀B (λt,
+   ∀ {t ~> bool} (λa,
+   ∀ {Pull t} (λm,
+   Dive (psub {t} a) m ⊃ (λh, a (dive t m (below t a m h)))))))
+proof
+admit
+
+// Rewrite [dive {x: T | a} m h] to succession of pairs.
+rule dive (psub {$t} $a) $m $h
+   ↪ pair {$t} {$a} (dive $t $m (below $t $a $m $h)) (top $t $a $m $h)
+
+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
+
+// Erase [transfer] if casting to the same type.
+rule transfer' $t $t $m ↪ $m
 
 definition cast {fr_t: Set} (to_t: Set)
                 (comp: Equivalent fr_t to_t) (m: El fr_t)
@@ -48,27 +77,7 @@ definition cast {fr_t: Set} (to_t: Set)
                                                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]
+// Some rules on top types are needed, we give them for [bool]
+rule Pull bool ↪ bool // Can't go above [bool]
+with pull bool $x ↪ $x // A term can't be pulled higher than [bool]
+with Dive bool _ ↪ true // A term compatible with [bool] can always be [bool]