From fa74efc277363bb3e2b827263e5fd2fa92b504c1 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Fri, 27 Nov 2020 21:16:29 +0100
Subject: [PATCH] updated encoding
---
encodings/bool_plus.lp | 2 +-
encodings/builtins.lp | 7 ++++---
encodings/deptype.lp | 3 ++-
encodings/{bool_pvs.lp => if.lp} | 0
encodings/lhol.lp | 3 ---
encodings/{bool_hol.lp => logical.lp} | 0
encodings/pairs.lp | 4 ----
encodings/prenex.lp | 18 ++++++++++--------
prelude/functions.lp | 2 +-
prelude/logic.lp | 8 ++++----
10 files changed, 22 insertions(+), 25 deletions(-)
rename encodings/{bool_pvs.lp => if.lp} (100%)
rename encodings/{bool_hol.lp => logical.lp} (100%)
diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index 7aac76c..0aa7d98 100644
--- a/encodings/bool_plus.lp
+++ b/encodings/bool_plus.lp
@@ -1,6 +1,6 @@
require open personoj.encodings.lhol
require open personoj.encodings.prenex
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
// It may be generalisable to dependent propositions
theorem and_intro:
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index 115d771..5d46955 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -1,8 +1,9 @@
require open personoj.encodings.lhol
require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
+require open personoj.encodings.prenex
-constant symbol {|!Number!|}: θ {|set|}
+constant symbol {|!Number!|}: Set
constant symbol zero: El {|!Number!|}
constant symbol succ: El ({|!Number!|} ~> {|!Number!|})
@@ -17,7 +18,7 @@ with Prf (zero = succ _) ↪ Prf false
with Prf (zero = zero) ↪ Prf true
// Define strings as list of numbers
-constant symbol {|!String!|}: θ {|set|}
+constant symbol {|!String!|}: Set
constant symbol str_empty: El {|!String!|}
constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|}
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index 9b1fc41..ffc1bff 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -7,7 +7,8 @@
require open personoj.encodings.lhol
require open personoj.encodings.pvs_cert
+require open personoj.encodings.prenex
constant symbol darr: Set → Kind → Kind
set infix right 6 "*>" ≔ darr
-rule θ ($t *> $k) ↪ El $t → θ $k
+rule Ty ($t *> $k) ↪ El $t → Ty $k
diff --git a/encodings/bool_pvs.lp b/encodings/if.lp
similarity index 100%
rename from encodings/bool_pvs.lp
rename to encodings/if.lp
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 8e94c6f..75843f2 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -3,16 +3,13 @@ symbol Kind: TYPE
symbol Set: TYPE
symbol Bool: TYPE
-set declared "θ"
set declared "∀"
-injective symbol θ: Kind → TYPE
injective symbol El: Set → TYPE
injective symbol Prf: Bool → TYPE
constant symbol {|set|}: Kind
constant symbol bool: Set
-rule θ {|set|} ↪ Set
rule El bool ↪ Bool
constant symbol ∀ {x: Set}: (El x → Bool) → Bool
diff --git a/encodings/bool_hol.lp b/encodings/logical.lp
similarity index 100%
rename from encodings/bool_hol.lp
rename to encodings/logical.lp
diff --git a/encodings/pairs.lp b/encodings/pairs.lp
index eb53f18..4b852f2 100644
--- a/encodings/pairs.lp
+++ b/encodings/pairs.lp
@@ -1,8 +1,4 @@
require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
-require open personoj.encodings.tuple
-require open personoj.encodings.prenex
set declared "Σ" // Dependent pairs
set declared "σ" // Non dependent pairs
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index 77709b2..3ac6e86 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -8,29 +8,31 @@
require open personoj.encodings.lhol
// Quantification for objects of type ‘Kind’
-set declared "Ï•"
set declared "∀K"
// Quantification for objects of type ‘Set’
-set declared "χ"
set declared "∀S"
// Quantification for objects of type ‘Bool’
set declared "∀B"
+// To interpret PVS sorts
+injective symbol Ty : Kind → TYPE
+rule Ty {|set|} ↪ Set
+
constant symbol SchemeK: TYPE
-symbol ϕ: SchemeK → TYPE
+injective symbol El_k: SchemeK → TYPE
constant symbol scheme_k: Kind → SchemeK
-rule ϕ (scheme_k $X) ↪ θ $X
+rule El_k (scheme_k $X) ↪ Ty $X
constant symbol ∀K: (Set → SchemeK) → SchemeK
-rule ϕ (∀K $e) ↪ Πt: Set, ϕ ($e t)
+rule El_k (∀K $e) ↪ Πt: Set, El_k ($e t)
constant symbol SchemeS: TYPE
-symbol χ: SchemeS → TYPE
+injective symbol El_s: SchemeS → TYPE
constant symbol scheme_s: Set → SchemeS
-rule χ (scheme_s $X) ↪ El $X
+rule El_s (scheme_s $X) ↪ El $X
constant symbol ∀S: (Set → SchemeS) → SchemeS
-rule χ (∀S $e) ↪ Πt: Set, χ ($e t)
+rule El_s (∀S $e) ↪ Πt: Set, El_s ($e t)
constant symbol ∀B: (Set → Bool) → Bool
rule Prf (∀B $p) ↪ Πx: Set, Prf ($p x)
diff --git a/prelude/functions.lp b/prelude/functions.lp
index fe6835e..c0d6db2 100644
--- a/prelude/functions.lp
+++ b/prelude/functions.lp
@@ -1,6 +1,6 @@
require open personoj.encodings.lhol
require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
require open personoj.encodings.prenex
require open personoj.prelude.logic
//
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 6694784..cd351e4 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -1,6 +1,6 @@
require open personoj.encodings.lhol
require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
require open personoj.encodings.prenex
require open personoj.encodings.builtins
//
@@ -60,7 +60,7 @@ admit
//
// Defined types
//
-definition pred: ϕ (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> bool
+definition pred: El_k (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> bool
definition PRED ≔ pred
definition predicate ≔ pred
definition PREDICATE ≔ pred
@@ -112,8 +112,8 @@ set builtin "eqind" ≔ eqind
//
theorem lift_if1:
- Prf (∀B (λs: θ {|set|},
- ∀B (λt: θ {|set|},
+ Prf (∀B (λs: Ty {|set|},
+ ∀B (λt: Ty {|set|},
∀ {bool}
(λa,
∀ (λx: El s,
--
GitLab