From 345d051b2f5e87dc9280f1fed04f8d9ace14bdf7 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 22 Apr 2020 15:34:09 +0200
Subject: [PATCH] dependent types, phi to theta

---
 encodings/lhol.lp     | 18 +++++++++---------
 encodings/pvs_more.lp | 10 ++++++++++
 paper/equal.lp        |  2 +-
 prelude/logic.lp      |  5 ++---
 prelude/numbers.lp    |  2 +-
 5 files changed, 23 insertions(+), 14 deletions(-)
 create mode 100644 encodings/pvs_more.lp

diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 7dabafd..0fc57f8 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -3,29 +3,29 @@ symbol Kind: TYPE
 symbol Set: TYPE
 symbol Bool: TYPE
 
-set declared "Ï•"
+set declared "θ"
 set declared "η"
 set declared "ε"
 set declared "∀"
-injective symbol ϕ: Kind → TYPE
+injective symbol θ: Kind → TYPE
 injective symbol η: Set → TYPE
 injective symbol ε: Bool → TYPE
 
-symbol {|set|}: Kind
-symbol bool: Set
+constant symbol {|set|}: Kind
+constant symbol bool: Set
 
-rule ϕ {|set|} ↪ Set
+rule θ {|set|} ↪ Set
 rule η bool ↪ Bool
 
-symbol ∀ {x: Set}: (η x → Bool) → Bool
-symbol impd {x: Bool}: (ε x → Bool) → Bool
-symbol arrd {x: Set}: (η x → Set) → Set
+constant symbol ∀ {x: Set}: (η x → Bool) → Bool
+constant symbol impd {x: Bool}: (ε x → Bool) → Bool
+constant symbol arrd {x: Set}: (η x → Set) → Set
 
 rule ε (∀ {$X} $P) ↪ Πx: η $X, ε ($P x)
 with ε (impd {$H} $P) ↪ Πh: ε $H, ε ($P h)
 with η (arrd {$X} $T) ↪ Πx: η $X, η ($T x)
 
-symbol arr: Set → Set → Set
+constant symbol arr: Set → Set → Set
 rule η (arr $X $Y) ↪ (η $X) → (η $Y)
 set infix right 6 "~>" ≔ arr
 
diff --git a/encodings/pvs_more.lp b/encodings/pvs_more.lp
new file mode 100644
index 0000000..ab7a0cb
--- /dev/null
+++ b/encodings/pvs_more.lp
@@ -0,0 +1,10 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+// Dependent type
+// FIXME: quantification on types must be restricted to a prenex form
+set declared "ι"
+symbol ι: Kind → TYPE
+symbol dt_arr: Kind → Kind → Kind
+set infix right 7 "*>" ≔ dt_arr
+rule ι ({|set|} *> {|set|}) ↪ θ {|set|} → θ {|set|}
diff --git a/paper/equal.lp b/paper/equal.lp
index 7bd1476..150cc40 100644
--- a/paper/equal.lp
+++ b/paper/equal.lp
@@ -2,4 +2,4 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.prenex
 
-symbol eq: χ (∀S (λT: ϕ {|set|}, scheme (T ~> T ~> bool)))
+symbol eq: χ (∀S (λT: θ {|set|}, scheme (T ~> T ~> bool)))
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 0daaf1a..d109dc0 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -64,9 +64,8 @@ definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
 // Defined types
 //
 // FIXME: needs another prenex polymorphism to be encoded,
-// ∀K (λt, ? (t ~> {|set|})) ≔ λt: ϕ {|set|}, t ~> bool
-// definition pred : χ (∀S (λt, scheme (t ~> {|set|}))) ≔ λt: ϕ {|set|}, t ~> bool
-definition pred t ≔ t ~> bool
+require open personoj.encodings.pvs_more
+definition pred : ι ({|set|} *> {|set|}) ≔ λt: θ {|set|}, t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index c6e0660..9f47ebe 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -7,7 +7,7 @@ require open personoj.prelude.logic
 //
 // Theory numbers
 //
-constant symbol number: Ï• {|set|}
+constant symbol number: θ {|set|}
 
 //
 // Theory number_fields
-- 
GitLab