From 7a9e970d1015ecb2238522c0fb3b01abe05acdc3 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Wed, 17 Mar 2021 11:14:23 +0100
Subject: [PATCH] Submodule for prenex polymorphism

---
 encodings/bool_plus.lp     |  1 -
 encodings/builtins.lp      |  3 +--
 encodings/deptype.lp       |  3 +++
 encodings/lhol.lp          |  2 --
 encodings/prenex.lp        | 31 -------------------------------
 encodings/prenex/README.md | 11 +++++++++++
 encodings/prenex/kind.lp   |  9 +++++++++
 encodings/prenex/prop.lp   |  6 ++++++
 encodings/prenex/set.lp    | 10 ++++++++++
 9 files changed, 40 insertions(+), 36 deletions(-)
 delete mode 100644 encodings/prenex.lp
 create mode 100644 encodings/prenex/README.md
 create mode 100644 encodings/prenex/kind.lp
 create mode 100644 encodings/prenex/prop.lp
 create mode 100644 encodings/prenex/set.lp

diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index f5fd584..a6cde4e 100644
--- a/encodings/bool_plus.lp
+++ b/encodings/bool_plus.lp
@@ -1,5 +1,4 @@
 require open personoj.encodings.lhol
-             personoj.encodings.prenex
              personoj.encodings.logical;
 
 // It may be generalisable to dependent propositions
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index 28afce3..07edfb4 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -1,8 +1,7 @@
 require open personoj.encodings.lhol
              personoj.encodings.pvs_cert
              personoj.encodings.logical
-             personoj.encodings.equality
-             personoj.encodings.prenex;
+             personoj.encodings.equality;
 
 constant symbol {|!Number!|}: Set;
 
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index 75a9c8d..d6c5776 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -8,6 +8,9 @@
 require open personoj.encodings.lhol
              personoj.encodings.pvs_cert;
 
+constant symbol Kind: TYPE;
+constant symbol set: Kind;
+
 injective symbol Ty : Kind → TYPE;
 rule Ty set ↪ Set;
 
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 08e1175..fb6484f 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -1,12 +1,10 @@
 /// Encoding of λHOL
-symbol Kind: TYPE;
 symbol Set: TYPE;
 symbol Prop: TYPE;
 
 injective symbol El: Set → TYPE;
 injective symbol Prf: Prop → TYPE;
 
-constant symbol {|set|}: Kind;
 constant symbol prop: Set;
 
 rule El prop ↪ Prop;
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
deleted file mode 100644
index 725dab8..0000000
--- a/encodings/prenex.lp
+++ /dev/null
@@ -1,31 +0,0 @@
-/// Prenex polymorphism
-
-/// Prenex polymorphism allows to quantify over variables of type ‘Set’.
-/// PVS allows it in theory formals, such as
-/// groups[t: TYPE]: THEORY BEGIN ... END groups
-/// For more informations on the encoding of prenex polymorphism, see
-/// https://arxiv.org/abs/1807.01873 and theory U
-require open personoj.encodings.lhol
-             personoj.encodings.deptype;
-
-// Quantification for objects of type ‘Kind’
-constant symbol SchemeK: TYPE;
-injective symbol El_k: SchemeK → TYPE;
-constant symbol scheme_k: Kind → SchemeK;
-rule El_k (scheme_k $X) ↪ Ty $X;
-
-constant symbol ∀K: (Set → SchemeK) → SchemeK;
-rule El_k (∀K $e) ↪ Π t: Set, El_k ($e t);
-
-// Quantification for objects of type ‘Set’
-constant symbol SchemeS: TYPE;
-injective symbol El_s: SchemeS → TYPE;
-constant symbol scheme_s: Set → SchemeS;
-rule El_s (scheme_s $X) ↪ El $X;
-
-constant symbol ∀S: (Set → SchemeS) → SchemeS;
-rule El_s (∀S $e) ↪ Π t: Set, El_s ($e t);
-
-// Quantification for objects of type ‘Prop’
-constant symbol ∀B: (Set → Prop) → Prop;
-rule Prf (∀B $p) ↪ Π x: Set, Prf ($p x);
diff --git a/encodings/prenex/README.md b/encodings/prenex/README.md
new file mode 100644
index 0000000..9da0107
--- /dev/null
+++ b/encodings/prenex/README.md
@@ -0,0 +1,11 @@
+Prenex polymorphism
+===================
+
+Submodules in this directory provide the encoding of prenex polymorphism.
+Prenex polymorphism is allowed in PVS using the construction
+
+    groups[G: TYPE]: THEORY BEGIN ... END groups
+
+The encoding of prenex polymorphism is described in
+<https://arxiv.org/abs/1807.01873> and in the
+[Theory U](http://www.lsv.fr/~dowek/Publi/axiomslong.pdf).
diff --git a/encodings/prenex/kind.lp b/encodings/prenex/kind.lp
new file mode 100644
index 0000000..c36b9e0
--- /dev/null
+++ b/encodings/prenex/kind.lp
@@ -0,0 +1,9 @@
+require open personoj.encodings.lhol
+             personoj.encodings.deptype;
+
+constant symbol Scheme: TYPE;
+injective symbol Els: Scheme → TYPE;
+constant symbol lift: Kind → Scheme;
+rule Els (lift $X) ↪ Ty $X;
+constant symbol ∀: (Set → Scheme) → Scheme;
+rule Els (∀ $e) ↪ Π t: Set, Els ($e t);
diff --git a/encodings/prenex/prop.lp b/encodings/prenex/prop.lp
new file mode 100644
index 0000000..71f3d98
--- /dev/null
+++ b/encodings/prenex/prop.lp
@@ -0,0 +1,6 @@
+/// Prenex polymorphism in objects of type ‘Prop’
+
+require open personoj.encodings.lhol;
+
+constant symbol ∀: (Set → Prop) → Prop;
+rule Prf (∀ $P) ↪ Π x: Set, Prf ($P x);
diff --git a/encodings/prenex/set.lp b/encodings/prenex/set.lp
new file mode 100644
index 0000000..77e4750
--- /dev/null
+++ b/encodings/prenex/set.lp
@@ -0,0 +1,10 @@
+/// Prenex polymorphism in sorts of type ‘Set’
+require personoj.encodings.lhol as lhol;
+
+constant symbol Scheme: TYPE;
+injective symbol El: Scheme → TYPE;
+constant symbol lift: lhol.Set → Scheme;
+rule El (lift $X) ↪ lhol.El $X;
+
+constant symbol ∀: (lhol.Set → Scheme) → Scheme;
+rule El (∀ $e) ↪ Π a: lhol.Set, El ($e a);
-- 
GitLab