Renaming

encodings/dtuple.lp

+// 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

encodings/pair_equality.lp → encodings/equality_tup.lp

 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.pairs
+require personoj.encodings.tuple as T
 require open personoj.encodings.logical
 
-symbol peq {t: Set} (_: El (σ (μ t) (μ t))): Bool
-definition pneq  {t} m ≔ ¬ (@peq t m)
+symbol peq {t: Set} (_: El (T.t (μ t) (μ t))): Bool
+definition pneq {t} m ≔ ¬ (@peq t m)

encodings/logical.lp

 // 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)))

encodings/pairs.lp

-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

encodings/tuple.lp

-/// 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