Library Coq.ssr.ssrfun




Require Import ssreflect.

This file contains the basic definitions and notations for working with functions. The definitions provide for:
[fun (x : xT) (y : yT) => E] | == binary function with (some) explicit, [fun x (y : T) => E] / independent domain types for each argument
Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. sval u == the x of u : {x : T | P x}. s2val u == the x of u : {x : T | P x & Q x}. The properties of sval u, s2val u are given by lemmas svalP, s2valP, and s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 and pair, e.g., have /all_sig[f fP] (x : T): {y : U | P y} by ... yields an f : T -> U such that fP : forall x, P (f x). *** In addition to their casual use in functional programming, identity functions are often used to trigger static unification as part of the construction of dependent Records and Structures. For example, if we need a structure sT over a type T, we take as arguments T, sT, and a "dummy" function T -> sort sT: Definition foo T sT & T -> sort sT := ... We can avoid specifying sT directly by calling foo (@id T), or specify the call completely while still ensuring the consistency of T and sT, by calling @foo T sT idfun. The phant_id type allows us to extend this trick to non-Type canonical projections. It also allows us to sidestep dependent type constraints when building explicit records, e.g., given Record r := R {x; y : T(x)}. if we need to build an r from a given y0 while inferring some x0, such that y0 : T(x0), we pose Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking the dependent type constraint y0 : T(x0).
right_distributive op1 op2 <-> op distributes over add to the right: x op1 (y op2 z) = (x op1 z) op2 (x op1 z). interchange op1 op2 <-> op1 and op2 satisfy an interchange law: (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). Note that interchange op op is a commutativity property. left_injective op <-> op is injective in its left argument: x op y = z op y -> x = z. right_injective op <-> op is injective in its right argument: x op y = x op z -> y = z. left_loop inv op <-> op, inv obey the inverse loop left axiom: (inv x) op (x op y) = y for all x, y, i.e., op (inv x) is always a left inverse of op x rev_left_loop inv op <-> op, inv obey the inverse loop reverse left axiom: x op ((inv x) op y) = y, for all x, y. right_loop inv op <-> op, inv obey the inverse loop right axiom: (x op y) op (inv y) = x for all x, y. rev_right_loop inv op <-> op, inv obey the inverse loop reverse right axiom: (x op (inv y)) op y = x for all x, y. Note that familiar "cancellation" identities like x + y - y = x or x - y + y = x are respectively instances of right_loop and rev_right_loop The corresponding lemmas will use the K and NK/VK suffixes, respectively.
The file also contains some basic lemmas for the above concepts. Lemmas relative to cancellation laws use some abbreviated suffixes: K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). LR - a lemma moving an operation from the left hand side of a relation to the right hand side, like canLR: cancel g f -> x = g y -> f x = y. RL - a lemma moving an operation from the right to the left, e.g., canRL. Beware that the LR and RL orientations refer to an "apply" (back chaining) usage; when using the same lemmas with "have" or "move" (forward chaining) the directions will be reversed!.

Set Implicit Arguments.

Parsing / printing declarations.
Reserved Notation "p .1" (at level 2, left associativity, format "p .1").
Reserved Notation "p .2" (at level 2, left associativity, format "p .2").
Reserved Notation "f ^~ y" (at level 10, y at level 8, no associativity,
  format "f ^~ y").
Reserved Notation "@^~ x" (at level 10, x at level 8, no associativity,
  format "@^~ x").
Reserved Notation "[ 'eta' f ]" (at level 0, format "[ 'eta' f ]").
Reserved Notation "'fun' => E" (at level 200, format "'fun' => E").

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

Reserved Notation "f =1 g" (at level 70, no associativity).
Reserved Notation "f =1 g :> A" (at level 70, g at next level, A at level 90).
Reserved Notation "f =2 g" (at level 70, no associativity).
Reserved Notation "f =2 g :> A" (at level 70, g at next level, A at level 90).
Reserved Notation "f \o g" (at level 50, format "f \o '/ ' g").
Reserved Notation "f \; g" (at level 60, right associativity,
  format "f \; '/ ' g").

Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99,
  x ident, format "{ 'morph' f : x / a >-> r }").
Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99,
  x ident, format "{ 'morph' f : x / a }").
Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'morph' f : x y / a >-> r }").
Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'morph' f : x y / a }").
Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
  x ident, format "{ 'homo' f : x / a >-> r }").
Reserved Notation "{ 'homo' f : x / a }" (at level 0, f at level 99,
  x ident, format "{ 'homo' f : x / a }").
Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'homo' f : x y / a >-> r }").
Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'homo' f : x y / a }").
Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'homo' f : x y /~ a }").
Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
  x ident, format "{ 'mono' f : x / a >-> r }").
Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99,
  x ident, format "{ 'mono' f : x / a }").
Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'mono' f : x y / a >-> r }").
Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'mono' f : x y / a }").
Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99,
  x ident, y ident, format "{ 'mono' f : x y /~ a }").

Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id' T").
Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'").

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' a ]" (at level 0,
  format "[ 'rec' a ]").
Reserved Notation "[ 'rec' a , b ]" (at level 0,
  format "[ 'rec' a , b ]").
Reserved Notation "[ 'rec' a , b , c ]" (at level 0,
  format "[ 'rec' a , b , c ]").
Reserved Notation "[ 'rec' a , b , c , d ]" (at level 0,
  format "[ 'rec' a , b , c , d ]").
Reserved Notation "[ 'rec' a , b , c , d , e ]" (at level 0,
  format "[ 'rec' a , b , c , d , e ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f ]" (at level 0,
  format "[ 'rec' a , b , c , d , e , f ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g ]" (at level 0,
  format "[ 'rec' a , b , c , d , e , f , g ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h ]" (at level 0,
  format "[ 'rec' a , b , c , d , e , f , g , h ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h , i ]" (at level 0,
  format "[ 'rec' a , b , c , d , e , f , g , h , i ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h , i , j ]" (at level 0,
  format "[ 'rec' a , b , c , d , e , f , g , h , i , j ]").

Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.

Notations for pair/conjunction projections
Notation "p .1" := (fst p) : pair_scope.
Notation "p .2" := (snd p) : 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).

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

Shorthand for some basic equality lemmas.

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.
Force at least one implicit when used as a view.

A predicate for singleton types.
Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0.

Lemma unitE : all_equal_to tt.

A generic wrapper type

#[universes(template)]
Structure wrapped T := Wrap {unwrap : T}.
Canonical wrap T x := @Wrap T x.


Delimit Scope fun_scope with FUN.
Open Scope fun_scope.

Notations for argument transpose
Notation "f ^~ y" := (fun x => f x y) : fun_scope.
Notation "@^~ x" := (fun f => f x) : fun_scope.

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

#[universes(template)]
Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT.

Section SimplFun.

Variables aT rT : Type.

Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x.

End SimplFun.

Coercion fun_of_simpl : simpl_fun >-> Funclass.

Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope.
Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope.
Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope.
Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E))
  (only parsing) : fun_scope.
Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E])
  (only parsing) : fun_scope.
Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E])
  (only parsing) : fun_scope.
Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E])
  (only parsing) : fun_scope.
Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" := (fun x : T => [fun y : U => E])
  (only parsing) : fun_scope.

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

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 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 : core.

Notation "f1 =1 f2" := (eqfun f1 f2) : fun_scope.
Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A)) : fun_scope.
Notation "f1 =2 f2" := (eqrel f1 f2) : fun_scope.
Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A)) : fun_scope.

Section Composition.

Variables A B C : Type.

Definition comp (f : B -> A) (g : C -> B) x := f (g x).
Definition catcomp g f := comp 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 "f1 \o f2" := (comp f1 f2) : fun_scope.
Notation "f1 \; f2" := (catcomp f1 f2) : fun_scope.

Notation "[ 'eta' f ]" := (fun x => f x) : fun_scope.

Notation "'fun' => E" := (fun _ => E) : fun_scope.

Notation id := (fun x => x).
Notation "@ 'id' T" := (fun x : T => x) (only parsing) : fun_scope.

Definition idfun T x : T := x.

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

The empty type.

Notation void := Empty_set.

Definition of_void T (x : void) : T := match x with end.

Strong sigma types.

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

Refinement types.
Prenex Implicits and renaming.
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).

Morphism property for unary and binary functions
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).

Homomorphism property for unary and binary relations
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).

Stability property for unary and binary relations
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)) : type_scope.
Notation "{ 'morph' f : x / a }" :=
  (morphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'morph' f : x y / a >-> r }" :=
  (morphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'morph' f : x y / a }" :=
  (morphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'homo' f : x / a >-> r }" :=
  (homomorphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'homo' f : x / a }" :=
  (homomorphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'homo' f : x y / a >-> r }" :=
  (homomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'homo' f : x y / a }" :=
  (homomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'homo' f : x y /~ a }" :=
  (homomorphism_2 f (fun y x => a) (fun x y => a)) : type_scope.
Notation "{ 'mono' f : x / a >-> r }" :=
  (monomorphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'mono' f : x / a }" :=
  (monomorphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'mono' f : x y / a >-> r }" :=
  (monomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'mono' f : x y / a }" :=
  (monomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'mono' f : x y /~ a }" :=
  (monomorphism_2 f (fun y x => a) (fun 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.

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 : nonPropType} : injective (@Some T).

Lemma of_voidK T : pcancel (of_void T) [fun _ => None].

cancellation lemmas for dependent type casts.
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 inj_compr : injective (f \o h) -> injective 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).

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