[ new ] Introduce a Biinjective interface

libs/base/Control/Function.idr

@@ -1,5 +1,7 @@
 module Control.Function
 
+%default total
+
 ||| An injective function maps distinct elements to distinct elements.
 public export
 interface Injective (f : a -> b) | f where
@@ -16,7 +18,7 @@ inj _ eq = irrelevantEq (injective eq)
 public export
 [ComposeInjective] {f : a -> b} -> {g : b -> c} ->
   (Injective f, Injective g) => Injective (g . f) where
-    injective prf = injective $ injective prf
+    injective = injective . injective
 
 ||| If (g . f) is injective, so is f.
 public export
@@ -27,3 +29,47 @@ public export
 public export
 [IdInjective] Injective Prelude.id where
   injective = id
+
+----------------------------------------
+
+||| An bi-injective function maps distinct elements to distinct elements in both arguments.
+||| This is more strict than injectivity on each of arguments.
+||| For instance, list appending is injective on both arguments but is not biinjective.
+public export
+interface Biinjective (f : a -> b -> c) | f where
+  constructor MkBiinjective
+  biinjective : {x, y : a} -> {v, w : b} -> f x v = f y w -> (x = y, v = w)
+
+public export
+biinj : (0 f : _) -> (0 _ : Biinjective f) => (0 _ : f x v = f y w) -> (x = y, v = w)
+biinj _ eq = let 0 bii = biinjective eq in (irrelevantEq $ fst bii, irrelevantEq $ snd bii)
+
+public export
+[ComposeBiinjective] {f : a -> b -> c} -> {g : c -> d} ->
+  Biinjective f => Injective g => Biinjective (g .: f) where
+    biinjective = biinjective . injective
+
+||| If (g .: f) is biinjective, so is f.
+public export
+[BiinjFromComp] {f : a -> b -> c} -> {g : c -> d} ->
+  Biinjective (g .: f) => Biinjective f where
+    biinjective = biinjective {f = (g .: f)} . cong g
+
+public export
+[FlipBiinjective] {f : a -> b -> c} ->
+  Biinjective f => Biinjective (flip f) where
+    biinjective = swap . biinjective
+
+public export
+[FromBiinjectiveL] {f : a -> b -> c} -> {x : a} ->
+  Biinjective f => Injective (f x) where
+    injective = snd . biinjective
+
+public export
+[FromBiinjectiveR] {f : a -> b -> c} -> {y : b} ->
+  Biinjective f => Injective (`f` y) where
+    injective = fst . biinjective
+
+export
+Biinjective MkPair where
+  biinjective Refl = (Refl, Refl)

libs/base/Data/List.idr

@@ -1,5 +1,7 @@
 module Data.List
 
+import public Control.Function
+
 import Data.Nat
 import Data.List1
 import Data.Fin
@@ -914,6 +916,11 @@ export
 
 ||| (::) is injective
 export
+Biinjective Prelude.(::) where
+  biinjective Refl = (Refl, Refl)
+
+||| Heterogeneous injectivity for (::)
+export
 consInjective : forall x, xs, y, ys .
                 the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys)
 consInjective Refl = (Refl, Refl)

libs/base/Data/List1.idr

@@ -1,7 +1,7 @@
 module Data.List1
 
 import public Data.Zippable
-import Control.Function
+import public Control.Function
 
 %default total
 

libs/base/Data/List1/Properties.idr

@@ -12,9 +12,14 @@ import Data.List1
 %default total
 
 export
+-- %deprecate -- deprecated in favor of Biinjective interface
 consInjective : (x ::: xs) === (y ::: ys) -> (x === y, xs === ys)
 consInjective Refl = (Refl, Refl)
 
+export
+Biinjective (:::) where
+  biinjective Refl = (Refl, Refl)
+
 export
 {x : a} -> Injective (x :::) where
   injective Refl = Refl
@@ -64,6 +69,5 @@ fromListAppend [] ys with (fromList ys)
   _ | (Just _) = Refl
 fromListAppend (x::xs) ys with (fromList ys) proof prf
   fromListAppend (x::xs) []      | Nothing         = rewrite appendNilRightNeutral xs in Refl
-  fromListAppend (x::xs) (y::ys) | (Just $ l:::ls) = do
+  fromListAppend (x::xs) (y::ys) | (Just $ l:::ls) =
-    let (prfL, prfLs) = consInjective $ injective prf
+    let (Refl, Refl) = biinjective $ injective prf in Refl
-    rewrite prfL; rewrite prfLs; Refl

libs/base/Data/These.idr

@@ -51,6 +51,10 @@ export
 {y : _} -> Injective (`Both` y) where
   injective Refl = Refl
 
+export
+Biinjective Both where
+  biinjective Refl = (Refl, Refl)
+
 public export
 (Show a, Show b) => Show (These a b) where
   showPrec d (This x)   = showCon d "This" $ showArg x

libs/base/Data/Vect.idr

@@ -33,10 +33,6 @@ lengthCorrect : (xs : Vect len elem) -> length xs = len
 lengthCorrect []        = Refl
 lengthCorrect (_ :: xs) = rewrite lengthCorrect xs in Refl
 
-||| If two vectors are equal, their heads and tails are equal
-vectInjective : {0 xs : Vect n a} -> {0 ys : Vect m b} -> x::xs = y::ys -> (x = y, xs = ys)
-vectInjective Refl = (Refl, Refl)
-
 export
 {x : a} -> Injective (Vect.(::) x) where
   injective Refl = Refl
@@ -45,6 +41,10 @@ export
 {xs : Vect n a} -> Injective (\x => Vect.(::) x xs) where
   injective Refl = Refl
 
+export
+Biinjective Vect.(::) where
+  biinjective Refl = (Refl, Refl)
+
 --------------------------------------------------------------------------------
 -- Indexing into vectors
 --------------------------------------------------------------------------------
@@ -333,8 +333,8 @@ DecEq a => DecEq (Vect n a) where
   decEq []      []      = Yes Refl
   decEq (x::xs) (y::ys) with (decEq x y, decEq xs ys)
     decEq (x::xs) (x::xs) | (Yes Refl, Yes Refl) = Yes Refl
-    decEq (x::xs) (y::ys) | (No nhd, _) = No $ nhd . fst . vectInjective
+    decEq (x::xs) (y::ys) | (No nhd, _) = No $ nhd . fst . biinjective
-    decEq (x::xs) (y::ys) | (_, No ntl) = No $ ntl . snd . vectInjective
+    decEq (x::xs) (y::ys) | (_, No ntl) = No $ ntl . snd . biinjective
 
 --------------------------------------------------------------------------------
 -- Order

libs/contrib/Data/List/Equalities.idr

@@ -1,5 +1,7 @@
 module Data.List.Equalities
 
+import Control.Function
+
 import Data.List
 
 %default total
@@ -34,7 +36,7 @@ snocInjective {xs = z :: xs} {ys = []} prf =
   let snocIsNil = snd $ consInjective {x = z} {xs = xs ++ [x]} {ys = []} prf
    in void $ snocNonEmpty snocIsNil
 snocInjective {xs = w :: xs} {ys = z :: ys} prf =
-  let (wEqualsZ, xsSnocXEqualsYsSnocY) = consInjective prf
+  let (wEqualsZ, xsSnocXEqualsYsSnocY) = biinjective prf
       (xsEqualsYS, xEqualsY) = snocInjective xsSnocXEqualsYsSnocY
    in (consCong2 wEqualsZ xsEqualsYS, xEqualsY)
 
@@ -80,7 +82,7 @@ lengthSnoc x (_ :: xs) = cong S (lengthSnoc x xs)
 export
 appendSameLeftInjective : (xs, ys, zs : List a) -> zs ++ xs = zs ++ ys -> xs = ys
 appendSameLeftInjective xs ys []      = id
-appendSameLeftInjective xs ys (_::zs) = appendSameLeftInjective xs ys zs . snd . consInjective
+appendSameLeftInjective xs ys (_::zs) = appendSameLeftInjective xs ys zs . snd . biinjective
 
 ||| Appending the same list at right is injective.
 export
@@ -92,16 +94,24 @@ appendSameRightInjective xs ys (z::zs) = rewrite appendAssociative xs [z] zs in
                                          rewrite appendAssociative ys [z] zs in
                                          fst . snocInjective . appendSameRightInjective (xs ++ [z]) (ys ++ [z]) zs
 
+export
+{zs : List a} -> Injective (zs ++) where
+  injective = appendSameLeftInjective _ _ zs
+
+export
+{zs : List a} -> Injective (++ zs) where
+  injective = appendSameRightInjective _ _ zs
+
 ||| List cannot be equal to itself prepended with some non-empty list.
 export
 appendNonEmptyLeftNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = xs ++ zs)
 appendNonEmptyLeftNotEq []      (_::_)  Refl impossible
 appendNonEmptyLeftNotEq (z::zs) (_::xs) prf
   = appendNonEmptyLeftNotEq zs (xs ++ [z]) @{SnocNonEmpty xs z}
-  $ rewrite sym $ appendAssociative xs [z] zs in snd $ consInjective prf
+  $ rewrite sym $ appendAssociative xs [z] zs in snd $ biinjective prf
 
 ||| List cannot be equal to itself appended with some non-empty list.
 export
 appendNonEmptyRightNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = zs ++ xs)
 appendNonEmptyRightNotEq []      (_::_)  Refl impossible
-appendNonEmptyRightNotEq (_::zs) (x::xs) prf = appendNonEmptyRightNotEq zs (x::xs) $ snd $ consInjective prf
+appendNonEmptyRightNotEq (_::zs) (x::xs) prf = appendNonEmptyRightNotEq zs (x::xs) $ snd $ biinjective prf

libs/contrib/Data/List/Palindrome.idr

@@ -39,7 +39,7 @@ reversePalindromeEqualsLemma x x' xs prf = equateInnerAndOuter flipHeadX
     flipLastX' : reverse (xs ++ [x']) = x :: xs -> (x' :: reverse xs) = (x :: xs)
     flipLastX' prf = rewrite (revAppend xs [x']) in prf
     cancelOuter : (reverse (xs ++ [x'])) = x :: xs -> reverse xs = xs
-    cancelOuter prf = snd (consInjective (flipLastX' prf))
+    cancelOuter prf = snd (biinjective (flipLastX' prf))
     equateInnerAndOuter
       : reverse (xs ++ [x']) ++ [x] = (x :: xs) ++ [x']
       -> (reverse xs = xs, x = x')