From f53ae83a7c66225136349cd5f6d0353eeffc0219 Mon Sep 17 00:00:00 2001
From: hondet <hondet@nancy.private.lsv.fr>
Date: Tue, 29 Sep 2020 11:44:56 +0200
Subject: [PATCH] Testing generalised subtyping

---
 encodings/subtyping.lp   |  5 +++-
 paper/rat_generalised.lp | 62 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 66 insertions(+), 1 deletion(-)
 create mode 100644 paper/rat_generalised.lp

diff --git a/encodings/subtyping.lp b/encodings/subtyping.lp
index fc5e4ba..3ec5b63 100644
--- a/encodings/subtyping.lp
+++ b/encodings/subtyping.lp
@@ -17,7 +17,9 @@ rule pull {psub _} $m ↪ pull (fst $m)
 // [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
+// We can potentiall make [Comp] and [CompRefl] private
 definition Equivalent A B ≔ Comp (Pull A) (Pull B)
+definition EqvRefl (t: Set) ≔ CompRefl (Pull t)
 
 // [Dive t m] generates the proposition gathering all the predicate
 // on the path to type [t].
@@ -80,4 +82,5 @@ definition cast {fr_t: Set} (to_t: Set)
 // 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]
+rule Dive bool _ ↪ true // A term compatible with [bool] can always be [bool]
+with dive bool $x _ ↪ $x // Diving to [bool] is immediate
diff --git a/paper/rat_generalised.lp b/paper/rat_generalised.lp
new file mode 100644
index 0000000..46f12e6
--- /dev/null
+++ b/paper/rat_generalised.lp
@@ -0,0 +1,62 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.subtyping
+require open personoj.encodings.bool_hol
+
+set infix right 2 "⇒" ≔ imp
+constant symbol rat: Set
+rule Pull rat ↪ rat
+rule pull rat $x ↪ $x
+rule Dive rat _ ↪ true
+rule dive rat $x _ ↪ $x
+
+constant symbol z: El rat
+symbol eq: El (rat ~> rat ~> bool)
+set infix 3 "=" ≔ eq
+
+symbol nat_p : El (rat ~> bool)
+definition nat ≔ psub nat_p
+
+constant symbol z_nat : Prf (nat_p z)
+constant symbol s: El (nat ~> nat)
+symbol plus: El (rat ~> rat ~> rat)
+set infix left 4 "+" ≔ plus
+
+constant symbol s_not_z:
+  Prf (∀ {nat} (λx, ¬ (z = (cast rat (EqvRefl nat) (s x) (λx, x)))))
+
+rule z = z ↪ true
+with cast rat _ (s $n) _ = cast rat _ (s $m) _
+   ↪ @cast nat rat (EqvRefl nat) $n (λx, x) = @cast nat rat (EqvRefl nat) $m (λx, x)
+
+theorem plus_closed_nat:
+  Prf
+  (∀ {nat} (λn,
+   ∀ {nat} (λm,
+   nat_p (cast rat (EqvRefl nat) n (λx, x) + cast rat (EqvRefl nat) m (λx, x)))))
+proof
+admit
+
+// It’s just true ∧ plus_closed_nat n m
+theorem tcc1:
+  Prf
+  (∀ {nat} (λn,
+   ∀ {nat} (λm,
+   true ∧ (λ_, nat_p (plus (cast rat (EqvRefl nat) n (λx, x))
+                           (cast rat (EqvRefl nat) m (λx, x)))))))
+proof
+admit
+
+set flag "print_implicits" on
+compute λn: El nat, cast rat (EqvRefl rat) n (λx, x)
+
+rule cast {nat} rat _ $n _ + z ↪ cast rat (EqvRefl rat) $n (λx, x)
+with cast {nat} rat _ $n _ + cast rat _ (s $m) _
+   ↪ cast {nat} rat (EqvRefl rat)
+          (s (cast {rat} nat (EqvRefl rat)
+                   (plus (cast {nat} rat (EqvRefl rat) $n (λx, x))
+                         (cast {nat} rat (EqvRefl rat) $m (λx, x)))
+                   _))
+          (λx, x)
+
+// compute λn: nat, cast rat (EqvRefl rat) n (λx, x)
-- 
GitLab