# Library ssrfun

```(c) Copyright Microsoft Corporation and Inria. All rights reserved.
```
Require Import ssreflect.

```This file contains the basic definitions and notations for working with
functions. The definitions concern:

Pair projections
p.1  == first element of a pair
p.2  == second element of a pair

Simplifying functions, beta-reduced by simpl and /= :
[fun : T => E] == constant function from type T that returns E
[fun x => E] == unary function
[fun x : T => E] == unary function with explicit domain type
[fun x y => E] == binary function
[fun x y : T => E] == binary function with explicit domain type
[fun (x : T) y => E] == binary function with explicit domain type
[fun x (y : T) => E] == binary function with explicit domain type
[fun (x : xT) (y : yT) => E]

- partial functions using option type,
oapp f d ox == if ox is Some x returns f x,        d otherwise
odflt d ox == if ox is Some x returns x,          d otherwise
obind f ox == if ox is Some x returns f x,        None otherwise
omap f ox == if ox is Some x returns Some (f x), None otherwise

- extensional equality for functions and relations (i.e. functions of 2
arguments),
f1 =1 f2      ==  f1 x is equal to f2 x forall x
f1 =1 f2 :>A  ==    ... and f2 is explicitly typed
f1 =2 f2      ==  f1 x y is equal to f2 x y forall x y
f1 =2 f2 :> A ==    ... and f2 is explicitly typed

- composition for total and partial functions,
f^~y == function f with y as second argument y
f1 \o f2  == composition of f1 and f2
pcomp f1 f2 == composition of partial functions f1 and f2

- properties of functions
injective f == f is injective
cancel f g == g is the inverse of f
pcancel f g == g is the inverse of f where g is partial
ocancel f g == g is the inverse of f where f is partial
bijective f == f is bijective
involutive f == f is involutive

- properties for operations
left_id e op == e is a left identity for op
right_id e op == e is a right identity for op
left_inverse e i op == i is a left inverse for op with unit e
right_inverse e i op == i is a right inverse for op with unit e
self_inverse x e op == x is its own inverse for op
idempotent x op == x is idempotent
associate op == op is associative
commutative op == op is commutative
left_commutative op == op is left commutative
right_commutative op == op is right commutative
left_zero z op == z is a right zero for op
right_zero z op == z is a right zero for op
left_distributive op1 op2 == op1 is left distributive for op2
right_distributive op1 op2 == op1 is right distributive for op2

- morphisms for functions and relations,
{morph f : x / a >-> r } == f is a morphism with respect to functions
(fun x => a) and (fun x => r)
{morph f : x / a } == f is a morphism with respect to (fun x => a)
{morph f : x y / a >-> r } == f is a morphism with respect to functions
(fun x y => a) and (fun x y => r)
{morph f : x / a } == f is a morphism with respect to (fun x y => a)

The file also contains some basic lemmas for the above concepts.
```

Import Prenex Implicits.

Delimit Scope fun_scope with FUN.
Open Scope fun_scope.

Notation "f ^~ y" := (fun x => f x y)
(at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope.

Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.

```Notations for pair projections
```
Notation "p .1" := (fst p)
(at level 2, left associativity, format "p .1") : pair_scope.
Notation "p .2" := (snd p)
(at level 2, left associativity, format "p .2") : pair_scope.

```Reserved notations for evaluation
```
Reserved Notation "e .[ x ]"
(at level 2, left associativity, format "e .[ x ]").

Reserved Notation "e .[ x1 , x2 , .. , xn ]"
(at level 2, left associativity,
format "e '[ ' .[ x1 , '/' x2 , '/' .. , '/' xn ] ']'").

```Reserved notations for subscripting and superscripting
```
Reserved Notation "x ^-1"
(at level 3, left associativity, format "x ^-1").

Reserved Notation "x *+ n" (at level 40, left associativity).
Reserved Notation "x *- n" (at level 40, left associativity).
Reserved Notation "x ^+ n" (at level 29, left associativity).
Reserved Notation "x ^- n" (at level 29, left associativity).

Reserved Notation "s `_ i"
(at level 3, i at level 2, left associativity, format "s `_ i").

```Complements on the option type constructor, used below to
encode partial functions.
```

Module Option.

Definition apply aT rT (f : aT -> rT) x u := if u is Some y then f y else x.

Definition default T := apply (fun x : T => x).

Definition bind aT rT (f : aT -> option rT) := apply f None.

Definition map aT rT (f : aT -> rT) := bind (fun x => Some (f x)).

End Option.

Notation oapp := Option.apply.
Notation odflt := Option.default.
Notation obind := Option.bind.
Notation omap := Option.map.
Notation some := (@Some _) (only parsing).

```Syntax for defining auxiliary recursive function.
Usage:
Section FooDefinition.
Variables (g1 : T1) (g2 : T2).  (globals)
Fixoint foo_auxiliary (a3 : T3) ... :=
body, using [rec e3, ...] for recursive calls
where "[ 'rec' a3 , a4 , ... ]" := foo_auxiliary.
Definition foo x y .. := [rec e1, ...].
+ proofs about foo
End FooDefinition.
```

Reserved Notation "[ 'rec' a0 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"
(at level 0).

```Definitions and notation for explicit functions with simplification,
i.e., which simpl and /= beta expand (this is complementary to nosimpl).
```

Section SimplFun.

Variables aT rT : Type.

CoInductive simpl_fun : Type := SimplFun of aT -> rT.

Definition fun_of_simpl := fun f x => let: SimplFun lam := f in lam x.

Coercion fun_of_simpl : simpl_fun >-> Funclass.

End SimplFun.

Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E))
(at level 0,
format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope.

Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E))
(at level 0, x ident,
format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope.

Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E))
(at level 0, x ident, only parsing) : fun_scope.

Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E])
(at level 0, x ident, y ident,
format "'[hv' [ 'fun' x y => '/ ' E ] ']'") : fun_scope.

Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.

Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.

Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.

Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" :=
(fun x : xT => [fun y : yT => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.

```For delta functions in eqtype.v.
```
Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z].

```Shorthand for some basic equality lemmas.
```

Definition erefl := refl_equal.
Definition esym := sym_eq.
Definition nesym := sym_not_eq.
Definition etrans := trans_eq.
Definition congr1 := f_equal.
Definition congr2 := f_equal2.
```Force at least one implicit when used as a view.
```

```Extensional equality, for unary and binary functions, including syntactic
sugar.
```

Section ExtensionalEquality.

Variables A B C : Type.

Definition eqfun (f g : B -> A) : Prop := forall x, f x = g x.

Definition eqrel (r s : C -> B -> A) : Prop := forall x y, r x y = s x y.

Lemma frefl : forall f, eqfun f f. Qed.

Lemma fsym : forall f g, eqfun f g -> eqfun g f. Qed.

Lemma ftrans : forall f g h, eqfun f g -> eqfun g h -> eqfun f h.

Lemma rrefl : forall r, eqrel r r. Qed.

End ExtensionalEquality.

Hint Resolve frefl rrefl.

Notation "f1 =1 f2" := (eqfun f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A))
(at level 70, f2 at next level, A at level 90) : fun_scope.
Notation "f1 =2 f2" := (eqrel f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A))
(at level 70, f2 at next level, A, B at level 90) : fun_scope.

Section Composition.

Variables A B C : Type.

Definition comp (f : B -> A) (g : C -> B) := [fun x => f (g x)].

Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x).

Lemma eq_comp : forall f f' g g', f =1 f' -> g =1 g' -> comp f g =1 comp f' g'.

End Composition.

Notation "[ 'eta' f ]" := (fun x => f x)
(at level 0, format "[ 'eta' f ]") : fun_scope.

Notation id := (fun x => x).
Notation "@ 'id' T " := (fun x : T => x)
(at level 10, T at level 8, only parsing) : fun_scope.

Notation "f1 \o f2" := (comp f1 f2) (at level 50) : fun_scope.

Definition idfun T := @id T.

Section OperationProperties.

Variable T : Type.
Variables zero one: T.
Variable inv : T -> T.
Variables mul add : T -> T -> T.

Notation Local "1" := one.
Notation Local "0" := zero.
Notation Local "x ^-1" := (inv x).
Notation Local "x * y" := (mul x y).
Notation Local "x + y" := (add x y).

Definition left_id := forall x, 1 * x = x.
Definition right_id := forall x, x * 1 = x.
Definition left_inverse := forall x, x^-1 * x = 1.
Definition right_inverse := forall x, x * x^-1 = 1.
Definition self_inverse := forall x, x * x = 1.
Definition idempotent := forall x, x * x = x.
Definition associative := forall x y z, x * (y * z) = x * y * z.
Definition commutative := forall x y, x * y = y * x.
Definition left_commutative := forall x y z, x * (y * z) = y * (x * z).
Definition right_commutative := forall x y z, x * y * z = x * z * y.
Definition left_zero := forall x, 0 * x = 0.
Definition right_zero := forall x, x * 0 = 0.
Definition left_distributive := forall x y z, (x + y) * z = x * z + y * z.
Definition right_distributive := forall x y z, x * (y + z) = x * y + x * z.

End OperationProperties.

Section Morphism.

Variables (aT rT sT : Type) (f : aT -> rT).

Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y).

End Morphism.

Notation "{ 'morph' f : x / a >-> r }" :=
(morphism_1 f (fun x => a) (fun x => r))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a >-> r }") : type_scope.

Notation "{ 'morph' f : x / a }" :=
(morphism_1 f (fun x => a) (fun x => a))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a }") : type_scope.

Notation "{ 'morph' f : x y / a >-> r }" :=
(morphism_2 f (fun x y => a) (fun x y => r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a >-> r }") : type_scope.

Notation "{ 'morph' f : x y / a }" :=
(morphism_2 f (fun x y => a) (fun x y => a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a }") : type_scope.

```In an intuitionistic setting, we have two degrees of injectivity. The
weaker one gives only simplification, and the strong one provides a left
inverse (we show in `fintype' that they coincide for finite types).
We also define an intermediate version where the left inverse is only a
partial function.
```

Section Injections.

```rT must come first so we can use @ to mitigate the Coq 1st order
unification bug (e..g., Coq can't infer rT from a "cancel" lemma).
```
Variables (rT aT : Type) (f : aT -> rT).

Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2.

Definition cancel g := forall x, g (f x) = x.

Definition pcancel g := forall x, g (f x) = Some x.

Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.

Lemma can_pcan : forall g, cancel g -> pcancel (fun y => Some (g y)).

Lemma pcan_inj : forall g, pcancel g -> injective.

Lemma can_inj : forall g, cancel g -> injective.

Lemma canLR : forall g x y, cancel g -> x = f y -> g x = y.

Lemma canRL : forall g x y, cancel g -> f x = y -> x = g y.

End Injections.

Section InjectionsTheory.

Variables (A B C : Type) (f g : B -> A) (h : C -> B).

Lemma inj_id : injective (@id A).

Lemma inj_can_sym : forall f', cancel f f' -> injective f' -> cancel f' f.

Lemma inj_comp : injective f -> injective h -> injective (f \o h).

Lemma can_comp : forall f' h',
cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f').

Lemma pcan_pcomp : forall f' h',
pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f').

Lemma eq_inj : injective f -> f =1 g -> injective g.

Lemma eq_can : forall f' g', cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.

Lemma inj_can_eq : forall f',
cancel f f' -> injective f' -> cancel g f' -> f =1 g.

End InjectionsTheory.

Section Bijections.

Variables (A B : Type) (f : B -> A).

Definition bijective : Prop := exists2 g, cancel f g & cancel g f.

Hypothesis bijf : bijective.

Lemma bij_inj : injective f.

Lemma bij_can_sym : forall f', cancel f' f <-> cancel f f'.

Lemma bij_can_eq : forall f' f'', cancel f f' -> cancel f f'' -> f' =1 f''.

End Bijections.

Section BijectionsTheory.

Variables (A B C : Type) (f : B -> A) (h : C -> B).

Lemma eq_bij : bijective f -> forall g, f =1 g -> bijective g.

Lemma bij_comp : bijective f -> bijective h -> bijective (f \o h).

Lemma bij_can_bij : bijective f -> forall f', cancel f f' -> bijective f'.

End BijectionsTheory.

Section Involutions.

Variables (A : Type) (f : A -> A).

Definition involutive := cancel f f.

Hypothesis Hf : involutive.

Lemma inv_inj : injective f. Qed.

Lemma inv_bij : bijective f. Qed.

End Involutions.