(** * Prelude

   Definitions of operations and standard properties on them.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

Global Generalizable All Variables.

Require Export Program.Basics.
Require Import Morphisms Setoid.
Require Import RelationClasses.
Open Local Scope equiv_scope.

Lemma PER_refl_l `{ P : PER A R } : Π {x y}, R x y -> R x x.
Proof. intros. transitivity y ; auto. symmetry ; auto. Qed.

Lemma PER_refl_r `{ P : PER A R } : Π {x y}, R x y -> R y y.
Proof. intros. transitivity x ; auto. symmetry ; auto. Qed.

Ltac add_morphisms H := 
  match type of H with
    ?R ?x ?y =>
    let Hl := fresh H in let Hr := fresh H in
      assert(Hl:=PER_refl_l H:Proper _ x) ; assert(Hr:=PER_refl_r H:Proper _ y)
  end.

Open Local Scope signature_scope.

Instance pointwise_subrelation `{ ref : Reflexive A R, sub : subrelation B S₀ S₁ } :
  subrelation (R ==> S₀) (pointwise_relation A S₁) | 4.
Proof. firstorder. Qed.

(* Class Relation α := relation_of_Relation : relation α. *)

(* Instance Relation_DefaultRelation (( R : Relation α )) : DefaultRelation R. *)

Definition make_infix {α β δ} (f : α -> β -> δ) := f.

(* Notation " x [?]  y " := (make_infix (_:Relation _) x y) (at level 90). *)
Notation " x [ R ]  y " := (make_infix R x y) (at level 90).

Class Associative {α} (R : relation α) (f : α -> α -> α) :=
  assoc : Π x y z, f x (f y z) [R] f (f x y) z.

Class Commutative {α} (R : relation α) {β} (f : β -> β -> α) :=
  comm : f [pointwise_relation β (pointwise_relation β R)] (flip f).

Lemma is_comm `{ E: Equivalence α eqα, C: Commutative α (R:=eqα) α f, M: Proper _ (eqα ==> eqα ==> eqα) f } : 
  (eqα ==> eqα ==> eqα) f (flip f).
Proof. intros. simpl_relation. rewrite H, H0. setoid_rewrite comm at 2. reflexivity. Qed.

Lemma commutative `{ C : Commutative α (R:=R) β f } : Π x y, f x y [R] f y x.
Proof. intros. apply C ; reflexivity. Qed.

(** A generic definition from which all flavors of inverse, neutral and absorbant can be derived. *)

Class LeftLaw {α} (R : relation α) {β δ} (f : δ -> β -> α) (inv : β -> δ) (e : β -> α) :=
  left_law : Π x, f (inv x) x [R] e x.

Instance left_law_mor
  `{ eqa : Equivalence α eqα, eqb : Equivalence β eqβ, eqd : Equivalence δ eqδ } :
  Proper ((eqδ ==> eqβ ==> eqα) ==> (eqβ ==> eqδ) ==> (eqβ ==> eqα) ==> iff) (LeftLaw eqα).
Proof. simpl_relation. unfold LeftLaw.
  add_morphisms H ; add_morphisms H0. setoid_rewrite H. 
  setoid_rewrite H1. setoid_rewrite H0. reflexivity.
Qed.

Class RightLaw {α} (R : relation α) {β δ} (f : δ -> β -> α) (inv : δ -> β) (e : δ -> α) :=
  right_law_is_left :> LeftLaw R (flip f) inv e.
  
Lemma right_law `{ RightLaw α R β δ f inv e } : Π x, f x (inv x) [R] (e x).
Proof. intros ; apply right_law_is_left. Qed.

Class Law {α} (R : relation α) {β} (f : β -> β -> α) (inv : β -> β) (e : β -> α) :=
  { is_left_law :> LeftLaw R f inv e ;
    is_right_law :> RightLaw R f inv e }.

(** Inverses *)

Class LeftInverse {α} (R : relation α) {β δ} (f : δ -> β -> α) (inv : β -> δ) (e : α) :=
  left_inverse_law :> LeftLaw R f inv (const e).

Lemma left_inverse `{ LeftInverse α R β δ f inv e } : Π x, f (inv x) x [R] e.
Proof. intuition. Qed.

Class RightInverse {α} (R : relation α) {β δ} (f : δ -> β -> α) (inv : δ -> β) (e : α) :=
  right_inverse_is_left :> LeftInverse R (flip f) inv e.
  
Lemma right_inverse `{ RightInverse α R β δ f inv e } : Π x, f x (inv x) [R] e.
Proof. intros ; apply right_inverse_is_left. Qed.

Class Inverse {α} (R : relation α) {β} (f : β -> β -> α) (inv : β -> β) (e : α) :=
  { is_left_inverse :> LeftInverse R f inv e ;
    is_right_inverse :> RightInverse R f inv e }.

Class LeftNeutral {α} (R : relation α) {β} (f : β -> α -> α) (e : β) :=
  neutral_law :> LeftLaw R f (const e) id.

Lemma left_neutral `{ LeftNeutral α R β f e } : Π x, f e x [R] x.
Proof. intuition. Qed.

Class RightNeutral {α} (R : relation α) {β} (f : α -> β -> α) (e : β) :=
  right_neutral_is_left :> LeftNeutral R (flip f) e.

Lemma right_neutral `{ RightNeutral α R β f e } : Π x, f x e [R] x.
Proof. intros ; apply right_neutral_is_left. Qed.

Class Neutral {α} (R : relation α) (f : α -> α -> α) (e : α) :=
  { is_left_neutral :> LeftNeutral R f e ;
    is_right_neutral :> RightNeutral R f e }.

Class LeftAbsorbant {α} (R : relation α) {β δ} (f : δ -> β -> α) (e : δ) (e' : α) :=
  left_absorbant_law :> LeftLaw R f (const e) (const e').

Lemma left_absorbant `{ LeftAbsorbant α R β δ f e e' } : Π x, f e x [R] e'.
Proof. intuition. Qed.

Class RightAbsorbant {α} (R : relation α) {β δ} (f : β -> δ -> α) (e : δ) (e' : α) :=
  right_absorbant_is_left :> LeftAbsorbant R (flip f) e e'.

Lemma right_absorbant `{ RightAbsorbant α R β δ f e e' } : Π x, f x e [R] e'.
Proof. intros ; apply right_absorbant_is_left. Qed.

Class Absorbant {α} (R : relation α) (f : α -> α -> α) (e : α) :=
  { is_left_absorbant :> LeftAbsorbant R f e e ;
    is_right_absorbant :> RightAbsorbant R f e e }.

Class LeftDistributive {α} (R : relation α) {β} (f : β -> α -> α) (g : α -> α -> α) :=
  left_distributive : Π x y z, f x (g y z) [R] g (f x y) (f x z).

Instance left_distributive_mor `{ eqa : Equivalence α eqα, eqb : Equivalence β eqβ } :
  Proper ((eqβ ==> eqα ==> eqα) ==> (eqα ==> eqα ==> eqα) ==> iff) (LeftDistributive eqα).
Proof. intros. intros f f' ff' g g' gg'. unfold LeftDistributive. 
  add_morphisms ff'. add_morphisms gg'. 
  setoid_rewrite <- ff'. setoid_rewrite <- gg'. reflexivity.
Qed.

Class RightDistributive {α} (R : relation α) {β} (f : α -> β -> α) (g : α -> α -> α) :=
  right_distributive_is_left :> LeftDistributive R (flip f) g.

Lemma right_distributive `{ RD : RightDistributive α R β f g } : Π x y z, f (g y z) x [R] g (f y x) (f z x).
Proof. intros. apply RD. Qed.

Class Distributive {α} (R : relation α) (f : α -> α -> α) (g : α -> α -> α) :=
  { is_left_distributive :> LeftDistributive R f g ;
    is_right_distributive :> RightDistributive R f g }.