From fe6867a0e71a24ef86443a8d0e77a4acd3845f98 Mon Sep 17 00:00:00 2001
From: Frederic Peschanski <frederic.peschanski@lip6.fr>
Date: Fri, 1 Dec 2023 18:15:18 +0100
Subject: [PATCH] misc lemmas

---
 src/latte_prelude/equal.clj | 17 ++++++++++++++++-
 src/latte_prelude/fun.clj   | 20 +++++++++++++++++++-
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/latte_prelude/equal.clj b/src/latte_prelude/equal.clj
index cfce31a..cc91258 100644
--- a/src/latte_prelude/equal.clj
+++ b/src/latte_prelude/equal.clj
@@ -8,7 +8,7 @@
 
    [latte.utils :refer [decomposer set-opacity!]]
    [latte.core :as latte :refer [definition defthm defimplicit defimplicit*
-                                          assume have qed proof]]
+                                          assume have qed proof try-proof]]
 
    [latte-prelude.utils :as pu]
    [latte-prelude.prop :as p :refer [<=> and or not]]
@@ -102,6 +102,21 @@ Proves `(equal y x)` from `eq-proof` by symmetry of equality, cf. [[eq-sym-thm]]
 
 (alter-meta! #'eq-sym update-in [:arglists] (fn [_] (list '[[eq-proof (equal x y)]])))
 
+(defthm not-eq-sym
+  [?T :type, x T, y T]
+  (==> (not (equal x y))
+       (not (equal y x))))
+
+(proof 'not-eq-sym-thm
+  (assume [Heq (not (equal x y))]
+    (assume [Hcontra (equal y x)]
+      (have <a> (equal x y) :by (eq-sym Hcontra))
+      (have <b> p/absurd :by (Heq <a>))))
+
+  (qed <b>))
+
+
+
 (defthm eq-trans-thm
   "The transitivity property of equality."
   [T :type, [x y z T]]
diff --git a/src/latte_prelude/fun.clj b/src/latte_prelude/fun.clj
index 8287cb5..31d3e30 100644
--- a/src/latte_prelude/fun.clj
+++ b/src/latte_prelude/fun.clj
@@ -11,7 +11,7 @@ as objects and functions  as arrows in the so-called *LaTTe category*."
   (:refer-clojure :exclude [and or not identity])
 
   (:require [latte.core :as latte :refer [definition defaxiom defthm defnotation
-                                          proof assume have pose qed
+                                          proof try-proof assume have pose qed
                                           forall lambda]]
             [latte-prelude.prop :as p :refer [and or not]]
             [latte-prelude.equal :as eq :refer [equal]]
@@ -222,6 +222,24 @@ as objects and functions  as arrows in the so-called *LaTTe category*."
     (==> (equal (f x) (f y))
          (equal x y))))
 
+(defthm injective-contra
+  "The contrapositive of [[injective]]."
+  [[?T ?U :type], f (==> T U)]
+  (==> (injective f)
+       (forall [x y T]
+          (==> (not (equal x y))
+               (not (equal (f x) (f y)))))))
+
+(proof 'injective-contra-thm
+  (assume [Hinj _]
+    (assume [x T y T
+             Hneq (not (equal x y))]
+      (assume [Hcontra (equal (f x) (f y))]
+        (have <a> (equal x y) :by (Hinj x y Hcontra))
+        (have <b> p/absurd :by (Hneq <a>)))))
+
+  (qed <b>))
+
 (definition surjective
   "A surjective function."
   [[?T ?U :type], f (==> T U)]