From c3b4c18b7e7b8856f5a70e701679c79db43cf670 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 7 Jul 2020 11:41:20 +0200
Subject: [PATCH] Introducing pairs

---
 encodings/pairs.lp | 16 ++++++++++++++++
 tests/pairs.lp     | 15 +++++++++++++++
 2 files changed, 31 insertions(+)
 create mode 100644 encodings/pairs.lp
 create mode 100644 tests/pairs.lp

diff --git a/encodings/pairs.lp b/encodings/pairs.lp
new file mode 100644
index 0000000..caba304
--- /dev/null
+++ b/encodings/pairs.lp
@@ -0,0 +1,16 @@
+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 "Σ"
+
+constant symbol Σ (t: Set): (η t → Set) → Set
+symbol pair_ss {t: Set} {u: η t → Set} (m: η t): η (u m) → η (Σ t u)
+
+symbol fst_ss {t: Set} {u: η t → Set}: η (Σ t u) → η t
+symbol snd_ss {t: Set} {u: η t → Set} (m: η (Σ t u)): η (u (fst_ss m))
+
+rule fst_ss (pair_ss $m _) ↪ $m
+rule snd_ss (pair_ss _ $n) ↪ $n
diff --git a/tests/pairs.lp b/tests/pairs.lp
new file mode 100644
index 0000000..869f3d4
--- /dev/null
+++ b/tests/pairs.lp
@@ -0,0 +1,15 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.deptype
+require open personoj.encodings.prenex
+require open personoj.encodings.pairs
+
+symbol nat: Set
+symbol plus: η ((Σ nat (λ_, nat)) ~> nat)
+
+symbol z: η nat
+symbol s: η (nat ~> nat)
+set builtin "0" ≔ z
+set builtin "+1" ≔ s
+
+assert plus (pair_ss 3 4): η nat
-- 
GitLab