From 79d335091315753aaa0502afe0c8cd488b337a10 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Mon, 6 Apr 2020 17:39:05 +0200
Subject: [PATCH] ad hoc poly, equality

---
 encodings/ad_hoc.lp   | 7 +++++++
 encodings/equality.lp | 7 +++++++
 encodings/lhol.lp     | 3 +++
 encodings/subtype.lp  | 2 ++
 4 files changed, 19 insertions(+)
 create mode 100644 encodings/ad_hoc.lp
 create mode 100644 encodings/equality.lp

diff --git a/encodings/ad_hoc.lp b/encodings/ad_hoc.lp
new file mode 100644
index 0000000..b1a7c7f
--- /dev/null
+++ b/encodings/ad_hoc.lp
@@ -0,0 +1,7 @@
+require open personoj.encodings.lhol
+             personoj.encodings.pvs_cert
+             personoj.encodings.subtype
+             personoj.encodings.equality
+
+symbol forall_sub: Set ⇒ (Set ⇒ Set) ⇒ Set
+rule η (forall_sub &T &C) → ∀U: Set, ε (U ⊑ &T) ⇒ η (&C U)
diff --git a/encodings/equality.lp b/encodings/equality.lp
new file mode 100644
index 0000000..2450de2
--- /dev/null
+++ b/encodings/equality.lp
@@ -0,0 +1,7 @@
+require open personoj.encodings.lhol
+
+symbol equal {T: Set}: η T ⇒ η T ⇒ Bool
+set infix left 6 "=" ≔ equal
+set builtin "T" ≔ η
+set builtin "P" ≔ ε
+set builtin "eq" ≔ equal
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 25945a0..a4f4793 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -27,3 +27,6 @@ rule ε (forall {&X} &P) → ∀x: η &X, ε (&P x)
 symbol arr: Set ⇒ Set ⇒ Set
 rule η (arr &X &Y) → (η &X) ⇒ (η &Y)
 set infix right 6 "~>" ≔ arr
+
+set builtin "T" ≔ η
+set builtin "P" ≔ ε
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 9a317df..7fa435b 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -13,6 +13,8 @@ symbol Arr (t u1 u2: Set): ε (u1 ⊑ u2) ⇒ ε ((t ~> u1) ⊑ (t ~> u2))
 symbol 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
+
 symbol root: Set ⇒ Set
 rule root (psub {&T} _) → root &T
 
-- 
GitLab