misc

adlib/subtype.lp

 require open personoj.encodings.cert_f
-personoj.adlib.bootstrap
+        personoj.adlib.bootstrap
 
 // A la rewriting logic
 rule Psub {&A} _ ⊑ &A → true

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

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

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