From 2ce9178eacaebe0e0969b4853b76c5373ad53e16 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Thu, 14 May 2020 15:16:52 +0200
Subject: [PATCH] inequality as builtin

---
 encodings/builtins.lp |  4 ++++
 prelude/logic.lp      | 14 ++++++++------
 prelude/numbers.lp    |  2 +-
 3 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index ef313a8..c7b1868 100644
--- a/encodings/builtins.lp
+++ b/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
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 4e6a81d..80c2ec4 100644
--- a/prelude/logic.lp
+++ b/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
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index 1978de6..c3a1598 100644
--- a/prelude/numbers.lp
+++ b/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
-- 
GitLab