Library Coq.ssr.ssrfun

Require Import ssreflect.


Set Implicit Arguments.

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.
Notation "@^~ x" := (fun f => f x)
  (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope.

Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.

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.

Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ).

Definition all_pair I T U (w : forall i : I, T i * U i) :=
  (fun i => (w i).1, fun i => (w i).2).


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).


Notation erefl := refl_equal.
Notation ecast i T e x := (let: erefl in _ = i := e return T in x).
Definition esym := sym_eq.
Definition nesym := sym_not_eq.
Definition etrans := trans_eq.
Definition congr1 := f_equal.
Definition congr2 := f_equal2.

Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0.

Lemma unitE : all_equal_to tt.


Structure wrapped T := Wrap {unwrap : T}.
Canonical wrap T x := @Wrap T x.



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


Section SimplFun.

Variables aT rT : Type.

CoInductive simpl_fun := SimplFun of aT -> rT.

Definition fun_of_simpl f := fun 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.

Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z].


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 f : eqfun f f.
Lemma fsym f g : eqfun f g -> eqfun g f.

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

Lemma rrefl r : eqrel r r.

End ExtensionalEquality.

Typeclasses Opaque eqfun.
Typeclasses Opaque eqrel.

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 at level 90) : fun_scope.

Section Composition.

Variables A B C : Type.

Definition funcomp u (f : B -> A) (g : C -> B) x := let: tt := u in f (g x).
Definition catcomp u g f := funcomp u f g.

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

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

End Composition.

Notation comp := (funcomp tt).
Notation "@ 'comp'" := (fun A B C => @funcomp A B C tt).
Notation "f1 \o f2" := (comp f1 f2)
  (at level 50, format "f1 \o '/ ' f2") : fun_scope.
Notation "f1 \; f2" := (catcomp tt f1 f2)
  (at level 60, right associativity, format "f1 \; '/ ' f2") : fun_scope.

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

Notation "'fun' => E" := (fun _ => E) (at level 200, only parsing) : 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.

Definition id_head T u x : T := let: tt := u in x.
Definition explicit_id_key := tt.
Notation idfun := (id_head tt).
Notation "@ 'idfun' T " := (@id_head T explicit_id_key)
  (at level 10, T at level 8, format "@ 'idfun' T") : fun_scope.

Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2.


Section Tag.

Variables (I : Type) (i : I) (T_ U_ : I -> Type).

Definition tag := projT1.
Definition tagged : forall w, T_(tag w) := @projT2 I [eta T_].
Definition Tagged x := @existT I [eta T_] i x.

Definition tag2 (w : @sigT2 I T_ U_) := let: existT2 _ _ i _ _ := w in i.
Definition tagged2 w : T_(tag2 w) := let: existT2 _ _ _ x _ := w in x.
Definition tagged2' w : U_(tag2 w) := let: existT2 _ _ _ _ y := w in y.
Definition Tagged2 x y := @existT2 I [eta T_] [eta U_] i x y.

End Tag.


Coercion tag_of_tag2 I T_ U_ (w : @sigT2 I T_ U_) :=
  Tagged (fun i => T_ i * U_ i)%type (tagged2 w, tagged2' w).

Lemma all_tag I T U :
   (forall x : I, {y : T x & U x y}) ->
  {f : forall x, T x & forall x, U x (f x)}.

Lemma all_tag2 I T U V :
    (forall i : I, {y : T i & U i y & V i y}) ->
  {f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}.


Notation sval := (@proj1_sig _ _).
Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").

Section Sig.

Variables (T : Type) (P Q : T -> Prop).

Lemma svalP (u : sig P) : P (sval u).

Definition s2val (u : sig2 P Q) := let: exist2 _ _ x _ _ := u in x.

Lemma s2valP u : P (s2val u).

Lemma s2valP' u : Q (s2val u).

End Sig.


Coercion tag_of_sig I P (u : @sig I P) := Tagged P (svalP u).

Coercion sig_of_sig2 I P Q (u : @sig2 I P Q) :=
  exist (fun i => P i /\ Q i) (s2val u) (conj (s2valP u) (s2valP' u)).

Lemma all_sig I T P :
    (forall x : I, {y : T x | P x y}) ->
  {f : forall x, T x | forall x, P x (f x)}.

Lemma all_sig2 I T P Q :
    (forall x : I, {y : T x | P x y & Q x y}) ->
  {f : forall x, T x | forall x, P x (f x) & forall x, Q x (f x)}.

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).

Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x).
Definition homomorphism_2 (aR rR : _ -> _ -> Prop) :=
  forall x y, aR x y -> rR (f x) (f y).

Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x.
Definition monomorphism_2 (aR rR : _ -> _ -> sT) :=
  forall x y, rR (f x) (f y) = aR x 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.

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

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

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

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

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

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

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

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

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

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


Section Injections.

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 g : cancel g -> pcancel (fun y => Some (g y)).

Lemma pcan_inj g : pcancel g -> injective.

Lemma can_inj g : cancel g -> injective.

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

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

End Injections.

Lemma Some_inj {T} : injective (@Some T).


Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).

Lemma etrans_id T x y (eqxy : x = y :> T) : etrans (erefl x) eqxy = eqxy.

Section InjectionsTheory.

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

Lemma inj_id : injective (@id A).

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

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

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

Lemma pcan_pcomp 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 f' g' : cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.

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

End InjectionsTheory.

Section Bijections.

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

CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f.

Hypothesis bijf : bijective.

Lemma bij_inj : injective f.

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

Lemma bij_can_eq 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.
Lemma inv_bij : bijective f.

End Involutions.

Section OperationProperties.

Variables S T R : Type.

Section SopTisR.
Implicit Type op : S -> T -> R.
Definition left_inverse e inv op := forall x, op (inv x) x = e.
Definition right_inverse e inv op := forall x, op x (inv x) = e.
Definition left_injective op := forall x, injective (op^~ x).
Definition right_injective op := forall y, injective (op y).
End SopTisR.

Section SopTisS.
Implicit Type op : S -> T -> S.
Definition right_id e op := forall x, op x e = x.
Definition left_zero z op := forall x, op z x = z.
Definition right_commutative op := forall x y z, op (op x y) z = op (op x z) y.
Definition left_distributive op add :=
  forall x y z, op (add x y) z = add (op x z) (op y z).
Definition right_loop inv op := forall y, cancel (op^~ y) (op^~ (inv y)).
Definition rev_right_loop inv op := forall y, cancel (op^~ (inv y)) (op^~ y).
End SopTisS.

Section SopTisT.
Implicit Type op : S -> T -> T.
Definition left_id e op := forall x, op e x = x.
Definition right_zero z op := forall x, op x z = z.
Definition left_commutative op := forall x y z, op x (op y z) = op y (op x z).
Definition right_distributive op add :=
  forall x y z, op x (add y z) = add (op x y) (op x z).
Definition left_loop inv op := forall x, cancel (op x) (op (inv x)).
Definition rev_left_loop inv op := forall x, cancel (op (inv x)) (op x).
End SopTisT.

Section SopSisT.
Implicit Type op : S -> S -> T.
Definition self_inverse e op := forall x, op x x = e.
Definition commutative op := forall x y, op x y = op y x.
End SopSisT.

Section SopSisS.
Implicit Type op : S -> S -> S.
Definition idempotent op := forall x, op x x = x.
Definition associative op := forall x y z, op x (op y z) = op (op x y) z.
Definition interchange op1 op2 :=
  forall x y z t, op1 (op2 x y) (op2 z t) = op2 (op1 x z) (op1 y t).
End SopSisS.

End OperationProperties.