From 5cdf7c1fedf1027ed685a7604599e032d4b05409 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Mon, 13 Apr 2020 17:17:26 +0200
Subject: [PATCH] subtyping

---
 encodings/pvs_cert.lp |  4 ++++
 encodings/subtype.lp  | 27 +++++++++++++++++++++------
 2 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/encodings/pvs_cert.lp b/encodings/pvs_cert.lp
index ba4bf53..3e550d9 100644
--- a/encodings/pvs_cert.lp
+++ b/encodings/pvs_cert.lp
@@ -13,3 +13,7 @@ protected symbol ppair: ∀{t: Set} {p: η t ⇒ Bool}, η t ⇒ η (psub p)
 // Reduction
 rule pair &X _ → ppair &X
 rule fst (ppair &M) → &M
+
+// Sub-typing relation
+symbol subtype : Set ⇒ Set ⇒ Bool
+set infix left 6 "⊑" ≔ subtype
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 160fe0a..b978a29 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -3,6 +3,7 @@ require open personoj.encodings.lhol
   personoj.encodings.booleans
 
 set declared "↑"
+set declared "↓"
 set declared "μ"
 set declared "μ₀"
 set declared "Ï€"
@@ -16,17 +17,31 @@ symbol S_Arr (t u1 u2: Set): ε (u1 ⊑ u2) ⇒ ε ((t ~> u1) ⊑ (t ~> u2))
 symbol S_Darr (d: Set) (r1: η d ⇒ Set) (r2: η d ⇒ Set)
 : ε (forall (λx, (r1 x) ⊑ (r2 x))) ⇒ ε ((arrd r1) ⊑ (arrd r2))
 
-symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
-definition ↑ {A} {B} ≔ upcast {A} {B}
-
 // Maximal supertype
 symbol μ: Set ⇒ Set
 rule μ (psub {&T} _) → μ &T
-rule μ (&T ~> &U) → &T ~> (μ &U)
+ and μ (&T ~> &U) → &T ~> (μ &U)
+ and μ (μ &T) → μ &T // FIXME: can be proved
 // Direct super-type
 symbol μ₀: Set ⇒ Set
 rule μ₀ (psub {&T} _) → μ₀ &T
 
 // Constraints
-symbol π {T: Set}: η T ⇒ Bool
-//rule π {psub {&T} &P} → λx: η (μ &T), (π {&T} x) ∧ (&P x)
+symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
+definition ↑ {A} {B} ≔ upcast {A} {B}
+rule upcast {&t} {&t} _ &x → &x
+
+theorem sub_of_sup A: ε (A ⊑ μ A)
+proof
+admit
+
+symbol π {T: Set}: η (μ T) ⇒ Bool
+symbol downcast {A: Set} {B: Set} (_: ε (B ⊑ A))
+                (a: η A) (p: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a))): η B
+definition ↓ {A} {B} ≔ downcast {A} {B}
+
+set flag "print_implicits" on
+rule π {&T ~> &U} → λx: η &T ⇒ η (μ &U), forall (λy, π {&U} (x y))
+rule π {psub {&T} &a}
+   → λx: η (μ &T), impd {π {&T} x} (λy, &a (↓ {μ &T} {&T} _ x y))
+// FIXME: does not type check because μ (μ &T) is not reduced to μ &T
-- 
GitLab