From b20356317c7db351cfda94809ffbaa0be35bb481 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 24 Mar 2020 15:35:41 +0100
Subject: [PATCH] misc

---
 adlib/subtype.lp |  2 +-
 prelude/logic.lp |  4 ++--
 sandbox/nat.lp   | 16 ++++++++++++++--
 sandbox/rat.lp   |  2 --
 4 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/adlib/subtype.lp b/adlib/subtype.lp
index 6e0492e..ae3b195 100644
--- a/adlib/subtype.lp
+++ b/adlib/subtype.lp
@@ -1,5 +1,5 @@
 require open personoj.encodings.cert_f
-personoj.adlib.bootstrap
+        personoj.adlib.bootstrap
 
 // A la rewriting logic
 rule Psub {&A} _ ⊑ &A → true
diff --git a/prelude/logic.lp b/prelude/logic.lp
index ef6be71..2d062b3 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -106,10 +106,10 @@ symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
 // set builtin "refl" ≔ reflexivity_of_equal
 
 symbol transitivity_of_equal T (x y z: Term T) :
-  Term ((eq x y) ∧ (eq y z)) ⇒ Term (eq x z)
+  Term ((x = y) ∧ (y = z)) ⇒ Term (eq x z)
 
 symbol symmetry_of_equal T (x y: Term T):
-  Term (eq x y) ⇒ Term (eq y x)
+  Term (x = y) ⇒ Term (y = x)
 
 //
 // if_props
diff --git a/sandbox/nat.lp b/sandbox/nat.lp
index dfa720e..f714630 100644
--- a/sandbox/nat.lp
+++ b/sandbox/nat.lp
@@ -62,7 +62,10 @@ qed
 symbol surjective_pairing T (p: Term T ⇒ Term bool):
        ∀x: Term (Psub p), Term (pair p (fst x) (snd x) = x)
 
-theorem prf_irrelevance: ∀x y: Term Even, Term (fst x = fst y) ⇒ Term (x = y)
+//symbol app_thm (D R: Term uType) (f: Term (D ~> R))
+//     : ∀x y: Term D, Term (x = y) ⇒ Term (f x = f y)
+
+theorem fst_injective: ∀x y: Term Even, Term (fst x = fst y) ⇒ Term (x = y)
 proof
     assume x y h
     refine transitivity_of_equal Even x (pair even (fst x) (snd x)) y _
@@ -79,5 +82,14 @@ proof
     focus 1
     refine surjective_pairing _ even y
 
-    simpl //FIXME
+abort
+
+rule &x = &x → true
+theorem prf_irrelevance T (p: Term T ⇒ Term bool)
+: ∀(x: Term T) (pr: Term (p x)) (pr': Term (p x)), Term (pair p x pr = pair p x pr')
+proof
+    assume T p x pr0 pr1
+    simpl
+    assume h
+    refine h
 qed
diff --git a/sandbox/rat.lp b/sandbox/rat.lp
index 547492f..cab1f99 100644
--- a/sandbox/rat.lp
+++ b/sandbox/rat.lp
@@ -16,8 +16,6 @@ set infix 8 "/" ≔ rat
 
 symbol times : Term Rat ⇒ Term Rat ⇒ Term Rat
 
-type λx: Term N.Nznat, fst x
-
 rule times (rat &a &b) (rat &c &d) →
   let bv ≔ fst &b in
   let dv ≔ fst &d in
-- 
GitLab