Injective follow-up (#2155)

CHANGELOG.md

@@ -48,6 +48,7 @@
   return code of that run.
 * Adds escaped versions of `System.system`, `Systen.File.popen`, and
   `System.run`, which take a list of arguments, and escapes them.
+* Adds the `Injective` interface in module `Control.Function`.
 * Changes `System.pclose` to return the return code of the closed process.
 * Deprecates `base`'s `Data.Nat.Order.decideLTE` in favor of `Data.Nat.isLTE`.
 * Removes `base`'s deprecated `System.Directory.dirEntry`. Use `nextDirEntry` instead.

libs/base/Control/Function.idr

@@ -1,10 +1,29 @@
 module Control.Function
 
+||| An injective function maps distinct elements to distinct elements.
 public export
-interface Injective (f : a -> b) where
+interface Injective (f : a -> b) | f where
   constructor MkInjective
   injective : {x, y : a} -> f x = f y -> x = y
 
 public export
 inj : (0 f : a -> b) -> {auto 0 _ : Injective f} -> {0 x, y : a} -> (0 _ : f x = f y) -> x = y
 inj _ eq = irrelevantEq (injective eq)
+
+----------------------------------------
+
+||| The composition of injective functions is injective.
+public export
+[ComposeInjective] {f : a -> b} -> {g : b -> c} ->
+  (Injective f, Injective g) => Injective (g . f) where
+    injective prf = injective $ injective prf
+
+||| If (g . f) is injective, so is f.
+public export
+[InjFromComp] {f : a -> b} -> {g : b -> c} ->
+  Injective (g . f) => Injective f where
+    injective prf = injective {f = (g . f)} $ cong g prf
+
+public export
+[IdInjective] Injective Prelude.id where
+  injective = id

libs/contrib/Data/Nat/Factor.idr

@@ -122,7 +122,7 @@ multOneSoleNeutral (S k) (S (S j)) prf =
         rewrite plusCommutative k j in
         rewrite sym $ plusAssociative j k (k * S j) in
         rewrite sym $ multRightSuccPlus k (S j) in
-        inj S $ injective prf
+        injective $ injective prf
 
 ||| If a is a factor of b and b is a factor of a, then a = b.
 public export