From 18c66708bf2e6c11b117e5ccaad047cf60e32c23 Mon Sep 17 00:00:00 2001
From: hondet <hondet@nancy.private.lsv.fr>
Date: Sun, 11 Oct 2020 10:31:53 +0200
Subject: [PATCH] cert star, reduced dependencies

---
 encodings/bool_plus.lp | 19 +++++++++++++++++++
 encodings/cert_star.lp |  2 +-
 encodings/prenex.lp    |  1 -
 3 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 encodings/bool_plus.lp

diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
new file mode 100644
index 0000000..cf1b187
--- /dev/null
+++ b/encodings/bool_plus.lp
@@ -0,0 +1,19 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.prenex
+require open personoj.encodings.bool_hol
+
+// It may be generalisable to dependent propositions
+theorem and_intro:
+  Prf
+  (∀ {bool} (λa,
+   ∀ {bool} (λb,
+   a ⊃ (λ_, b ⊃ (λ_, a ∧ (λ_, b))))))
+proof
+  assume A B h0 h1 f
+  refine f h0 h1
+qed
+
+theorem and_elim_1 a b (_: Prf (a ∧ (λ_, b))): Prf a
+proof
+  assume a b h
+qed
diff --git a/encodings/cert_star.lp b/encodings/cert_star.lp
index 04a81db..1ceddc8 100644
--- a/encodings/cert_star.lp
+++ b/encodings/cert_star.lp
@@ -33,10 +33,10 @@ set infix left 2 "~" ≔ compatible
 definition comp_refl t ≔ eqv_refl (pull t)
 
 protected symbol same' {t: Set} (u: Set) (_: El t): El u
+rule same' $t $t $m ↪ $m
 definition same {t: Set} (u: Set) (_: Prf (equivalent t u)) (m: El t)
          ≔ same' u m
 
-rule same' $t $t $m ↪ $m
 
 definition cast {fr_t: Set} (to_t: Set) (comp: Prf (fr_t ~ to_t))
                 (m: El fr_t)
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index b33c08c..77709b2 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -6,7 +6,6 @@
 /// For more informations on the encoding of prenex polymorphism, see
 /// https://arxiv.org/abs/1807.01873 and theory U
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
 
 // Quantification for objects of type ‘Kind’
 set declared "Ï•"
-- 
GitLab