From 15e6cccaf91af399e57dbec795372f397145a620 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Mon, 20 Apr 2020 12:04:49 +0200
Subject: [PATCH] new take on sub-typing

---
 encodings/subtype2.lp | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 encodings/subtype2.lp

diff --git a/encodings/subtype2.lp b/encodings/subtype2.lp
new file mode 100644
index 0000000..e2c5c8e
--- /dev/null
+++ b/encodings/subtype2.lp
@@ -0,0 +1,25 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
+
+set declared "μ"
+set declared "μ₀"
+set declared "Ï€"
+set declared "↑"
+set declared "↓"
+
+// Maximal supertype
+constant symbol μ: Set → Set
+rule η (μ (psub {$T} _)) ↪ η (μ $T)
+with η (μ ($T ~> $U)) ↪ η ($T ~> (μ $U))
+with η (μ (μ $T)) ↪ η (μ $T) // FIXME: can be proved
+
+symbol π {T: Set}: η (μ T) → Bool
+
+constant symbol maxcast {t: Set}: η t → η (μ t)
+constant symbol downcast {t: Set} (x: η (μ t)): ε (π x) → η t
+definition ↑ {t} ≔ maxcast {t}
+definition ↓ {t} ≔ downcast {t}
+
+rule ε (π {$t ~> $u}) ↪ ε (λx: η $t → η (μ $u), forall (λy, π (x y)))
+with ε (π {psub {$t} $a}) ↪ ε (λx: η (μ $t), (π x) ∧ (λy: ε (π x), $a (↓ x y)))
-- 
GitLab