From 49d439a7413ad72ae52c47680de0119e18edb8ae Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Fri, 4 Dec 2020 08:54:35 +0100
Subject: [PATCH] Renaming

---
 encodings/dtuple.lp        |  9 +++++++++
 encodings/equality_tup.lp  |  7 +++++++
 encodings/logical.lp       |  3 +--
 encodings/pair_equality.lp |  7 -------
 encodings/pairs.lp         | 23 ----------------------
 encodings/tuple.lp         | 39 +++++++-------------------------------
 6 files changed, 24 insertions(+), 64 deletions(-)
 create mode 100644 encodings/dtuple.lp
 create mode 100644 encodings/equality_tup.lp
 delete mode 100644 encodings/pair_equality.lp
 delete mode 100644 encodings/pairs.lp

diff --git a/encodings/dtuple.lp b/encodings/dtuple.lp
new file mode 100644
index 0000000..1e4e9c1
--- /dev/null
+++ b/encodings/dtuple.lp
@@ -0,0 +1,9 @@
+// Dependent tuples
+require open personoj.encodings.lhol
+
+constant symbol t (a: Set): (El a → Set) → Set
+symbol cons {a: Set} {b: El a → Set} (m: El a): El (b m) → El (t a b)
+symbol car {a: Set} {b: El a → Set}: El (t a b) → El a
+symbol cdr {a: Set} {b: El a → Set} (m: El (t a b)): El (b (car m))
+rule car (cons $m _) ↪ $m
+rule cdr (cons _ $n) ↪ $n
diff --git a/encodings/equality_tup.lp b/encodings/equality_tup.lp
new file mode 100644
index 0000000..dbfae48
--- /dev/null
+++ b/encodings/equality_tup.lp
@@ -0,0 +1,7 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require personoj.encodings.tuple as T
+require open personoj.encodings.logical
+
+symbol peq {t: Set} (_: El (T.t (μ t) (μ t))): Bool
+definition pneq {t} m ≔ ¬ (@peq t m)
diff --git a/encodings/logical.lp b/encodings/logical.lp
index 161a017..3bfae83 100644
--- a/encodings/logical.lp
+++ b/encodings/logical.lp
@@ -1,6 +1,5 @@
 // Definition based on implication
 require open personoj.encodings.lhol
-require open personoj.encodings.pairs
 
 definition false ≔ ∀ {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
@@ -23,7 +22,7 @@ set builtin "imp" ≔ imp
 set builtin "and" ≔ and
 set builtin "or"  ≔ or
 
-symbol if {s: Set} p: (Prf p → El s) → (Prf (¬ p) → El s) → El s
+symbol if {s: Set} (p: Bool): (Prf p → El s) → (Prf (¬ p) → El s) → El s
 rule if {bool} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
 
 definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
diff --git a/encodings/pair_equality.lp b/encodings/pair_equality.lp
deleted file mode 100644
index 3da34c1..0000000
--- a/encodings/pair_equality.lp
+++ /dev/null
@@ -1,7 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.pairs
-require open personoj.encodings.logical
-
-symbol peq {t: Set} (_: El (σ (μ t) (μ t))): Bool
-definition pneq  {t} m ≔ ¬ (@peq t m)
diff --git a/encodings/pairs.lp b/encodings/pairs.lp
deleted file mode 100644
index 4b852f2..0000000
--- a/encodings/pairs.lp
+++ /dev/null
@@ -1,23 +0,0 @@
-require open personoj.encodings.lhol
-
-set declared "Σ" // Dependent pairs
-set declared "σ" // Non dependent pairs
-set declared "σcons"
-set declared "σfst"
-set declared "σsnd"
-
-constant symbol σ: Set → Set → Set
-symbol σcons {t} {u}: El t → El u → El (σ t u)
-symbol σfst {t} {u}: El (σ t u) → El t
-rule σfst (σcons $x _) ↪ $x
-symbol σsnd {t} {u}: El (σ t u) → El u
-rule σsnd (σcons _ $y) ↪ $y
-
-constant symbol Σ (t: Set): (El t → Set) → Set
-symbol pair_ss {t: Set} {u: El t → Set} (m: El t): El (u m) → El (Σ t u)
-
-symbol fst_ss {t: Set} {u: El t → Set}: El (Σ t u) → El t
-symbol snd_ss {t: Set} {u: El t → Set} (m: El (Σ t u)): El (u (fst_ss m))
-
-rule fst_ss (pair_ss $m _) ↪ $m
-rule snd_ss (pair_ss _ $n) ↪ $n
diff --git a/encodings/tuple.lp b/encodings/tuple.lp
index e24bd8d..7089800 100644
--- a/encodings/tuple.lp
+++ b/encodings/tuple.lp
@@ -1,34 +1,9 @@
-/// WIP
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-
 // Non dependent tuples
-constant symbol tuple_t: Set → Set → Set
-constant symbol tuple {t} {u}: El t → El u → El (tuple_t t u)
-symbol p1 {t} {u}: El (tuple_t t u) → El t
-symbol p2 {t} {u}: El (tuple_t t u) → El u
-rule p1 (tuple $m _) ↪ $m
-rule p2 (tuple _ $n) ↪ $n
-
-constant symbol set_t: Set
-constant symbol set_nil: El set_t
-constant symbol set_cons: Set → El set_t → El set_t
-// TODO rewrite rules that transform (t, u, v) ~> w in t ~> u ~> v ~> w
-
-constant symbol TypeList: TYPE
-constant symbol type_nil: TypeList
-constant symbol type_cons: Set → TypeList → TypeList
-symbol type_cdr: TypeList → TypeList
-rule type_cdr (type_cons _ $tl) ↪ $tl
-symbol type_car: TypeList → Set
-rule type_car (type_cons $hd _) ↪ $hd
-
-constant symbol Tuple: TypeList → TYPE
-constant symbol tuple_nil: Tuple type_nil
-constant symbol tuple_cons (t: Set) (_: El t) (tl: TypeList) (_: Tuple tl):
-  Tuple (type_cons t tl)
+require open personoj.encodings.lhol
 
-symbol tuple_car (tl: TypeList): Tuple tl → El (type_car tl)
-rule tuple_car (type_cons $t _) (tuple_cons $t $x _) ↪ $x
-symbol tuple_cdr (tl: TypeList): Tuple tl → Tuple (type_cdr tl)
-rule tuple_cdr _ (tuple_cons _ _ _ $tup) ↪ $tup
+constant symbol t: Set → Set → Set
+symbol cons {a: Set} {b: Set}: El a → El b → El (t a b)
+symbol car {a: Set} {b: Set}: El (t a b) → El a
+symbol cdr {a: Set} {b: Set}: El (t a b) → El b
+rule car (cons $x _) ↪ $x
+rule cdr (cons _ $y) ↪ $y
-- 
GitLab