new equality

encoding/eq.lp

+// Equality
+require open personoj.lhol personoj.pvs_cert personoj.tuple personoj.logical;
+
+symbol = {a: Set} (_ _: El a): Prop;
+symbol eqind {a: Set} (p: El a → Prop) (x y: El a): Prf (p x) → Prf (@= a x y) → Prf (p y);
+
+symbol refl {a: Set} (x: El a): Prf (@= a x x); 
+
+opaque symbol eq_psub (a: Set) (t u: El a) (p: El a → Prop)
+											(ht: Prf (p t)) (hu: Prf (p u))
+											(e: Prf (@= a t u)):
+	Prf (@= (@psub a p) (@pair a p t ht) (@pair a p u hu)) ≔
+  @eqind a
+	(λ x: El a, (p x) ⇒ (λ h: Prf (p x), @= (@psub a p) (@pair a p t ht) (@pair a p x h))) t u
+	(λ ht': Prf (p t), @refl (@psub a p) (@pair a p t ht')) e hu;
+
+
+// Equality operates on the maximal supertype. It allows to profit
+// from predicate subtyping for free in the propositional equality.
+//rule @eq (@psub $t $p) ($x ^ $y ^ ^nil)
+//   ↪ @eq $t ((@fst $t $p $x) ^ (@fst $t $p $y) ^ ^nil);
+
+symbol != {a: Set} (x y: El a) ≔ ¬ (@= a x y);

specs/src/pp-dk3.lisp

@@ -88,7 +88,7 @@ BODY."
     (set-workdir (uiop:pathname-directory-pathname path))
     (with-open-file (stream file :direction :output :if-exists :supersede)
       (princ "require open personoj.lhol personoj.tuple personoj.sum
-personoj.logical personoj.pvs_cert personoj.eqtup;
+personoj.logical personoj.pvs_cert personoj.eq;
 require open personoj.nat personoj.coercions;
 require personoj.extra.arity-tools as A;" stream)
       (fresh-line stream)
@@ -928,8 +928,8 @@ as ``f (σcons e1 e2) (σcons g1 g2)''."
 
 ;;; REVIEW: factorise disequation and equation
 
-(defmethod pp-dk (stream (ex disequation) &optional colon-p at-sign-p)
-  "/=(A, B)"
+(defmethod pp-dk (stream (ex equation) &optional colon-p at-sign-p)
+  "=(A, B)"
   (with-parens (stream colon-p)
     (let* ((eq-ty (type (operator ex)))
            (dom (types (domain eq-ty)))
@@ -937,11 +937,11 @@ as ``f (σcons e1 e2) (σcons g1 g2)''."
            (tyr (cadr dom)))
       (assert (equal tyl tyr))
       (with-binapp-args (argl argr ex)
-        (format stream "@neq ~:/pvs:pp-dk/ ~:/pvs:pp-dk/"
-                tyl (make!-tuple-expr (list argl argr)))))))
+        (format stream "@= ~:/pvs:pp-dk/ ~:/pvs:pp-dk/ ~:/pvs:pp-dk/"
+                tyl argl argr)))))
 
-(defmethod pp-dk (stream (ex equation) &optional colon-p at-sign-p)
-  "=(A, B)"
+(defmethod pp-dk (stream (ex disequation) &optional colon-p at-sign-p)
+  "/=(A, B)"
   (with-parens (stream colon-p)
     (let* ((eq-ty (type (operator ex)))
            (dom (types (domain eq-ty)))
@@ -949,8 +949,8 @@ as ``f (σcons e1 e2) (σcons g1 g2)''."
            (tyr (cadr dom)))
       (assert (equal tyl tyr))
       (with-binapp-args (argl argr ex)
-        (format stream "@eq ~:/pvs:pp-dk/ ~:/pvs:pp-dk/"
-                tyl (make!-tuple-expr (list argl argr)))))))
+        (format stream "@!= ~:/pvs:pp-dk/ ~:/pvs:pp-dk/ ~:/pvs:pp-dk/"
+                tyl argl argr)))))
 
 (defmethod pp-dk (stream (ex conjunction) &optional colon-p at-sign-p)
   "AND(A, B)"