inequality as builtin

encodings/builtins.lp

@@ -26,3 +26,7 @@ definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
 
 symbol propositional_extensionality:
   ε (∀ {bool} (λp, (∀ {bool} (λq, (iff p q) ⊃ (λ_, eq {bool} p q)))))
+
+definition neq {t} x y ≔ ¬ (eq {t} x y)
+set infix left 2 "/=" ≔ neq
+set infix left 2 "≠" ≔ neq

prelude/logic.lp

@@ -2,6 +2,7 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.bool_hol
 require open personoj.encodings.prenex
+require open personoj.encodings.builtins
 //
 // Booleans
 // In [adlib.cert_f.bootstrap]
@@ -14,10 +15,11 @@ require open personoj.encodings.prenex
 // Notequal
 //
 // definition neq {T: Set} (x y: η T) ≔ ¬ (x = y)
-symbol neq: χ (∀S (λt, scheme (t ~> t ~> bool)))
-rule neq _ $x $y ↪ ¬ ($x = $y)
-set infix left 2 "/=" ≔ neq
-set infix left 2 "≠" ≔ neq
+// symbol neq: χ (∀S (λt, scheme (t ~> t ~> bool)))
+// rule neq _ $x $y ↪ ¬ ($x = $y)
+// set infix left 2 "/=" ≔ neq
+// set infix left 2 "≠" ≔ neq
+/// Defined in builtins
 
 //
 // if_def
@@ -26,7 +28,7 @@ set infix left 2 "≠" ≔ neq
 //
 // boolean_props
 // Slightly modified from the prelude
-constant symbol bool_exclusive: ε (neq bool false true)
+constant symbol bool_exclusive: ε (neq {bool} false true)
 constant
 symbol bool_inclusive
      : ε (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
@@ -40,7 +42,7 @@ qed
 //
 // xor_def
 //
-definition xor (a b: η bool) ≔ neq bool a b
+definition xor (a b: η bool) ≔ neq {bool} a b
 
 // PVS solves that kind of things thanks to the (bddsimp) tactic which uses an
 // external C program

prelude/numbers.lp

@@ -58,7 +58,7 @@ symbol Num_real: ε (∀ (λx: η {|!Number!|}, real_pred (insertnum x)))
 definition nonzero_real ≔
   psub {real}
        (λx: η real,
-        neq _ x (cast {_} {real} (λx, x) (insertnum 0) _))
+        neq {_} x (cast {_} {real} (λx, x) (insertnum 0) _))
 
 // symbol closed_plus_real: Π(x y: Term real),
 //   let pr ≔ S.restr numfield real_pred in