(** * Algebra AI-1 : Laws of composition; associativity; commutativity
  Copyright INRIA (2010) Apics Team (Jose Grimm).
*)

Require Export algebra3.

Set Implicit Arguments.
(* $Id: algebra4.v,v 1.13 2010/06/14 06:25:46 grimm Exp $ *)

Import RationalIntegers.
Import Transformation.

Module BasicAlgebra.
(** ** AI-1.1  Laws of composition *)

Definition magma (x:Set)(p:EEE):= Operations.is_law2I p x.

Lemma magma_ex1: magma Bnat card_plus.
Proof. ir. red. red. ir. fprops.
Qed.

Lemma magma_ex2: forall x,  magma (powerset x) union2.
Proof. ir. red. red. ir. rwi powerset_inc_rw H.  rwi powerset_inc_rw H0.
  rw powerset_inc_rw. red. ir. nin (union2_or H1). app H. app H0.
Qed.

Definition operation_product (p p' : EEE) := 
  fun u v => J (p (P u) (P v)) (p' (Q u) (Q v)).

Lemma prod_is_magma: forall x x' p p',
  magma x p -> magma x' p' -> 
  magma (product  x x')(operation_product p p').
Proof. ir. red. red. ir. uf operation_product. awi H1. awi H2.
  aw. intuition.
Qed.

Definition operation_productt (In:Set)   (p :In-> EEE) := 
  fun u v => gbcreate (fun i:In => p i (V (Ro i) u) (V (Ro i) v)).


Lemma productb_is_magma: forall(In:Set) (x :In-> Set)  (p :In-> EEE),
  (forall i:In, magma (x i) (p i)) -> 
  magma (productt x) (operation_productt p).
Proof. ir. red. red. ir. rwi productt_pr H0. rwi productt_pr H1.
  rw productt_pr. uf operation_productt. ee. app  fgraph_gbcreate.
  rww domain_gbcreate. ir. rw V_gbcreate. app (H i).
Qed. 

Definition operation_function (I:Set)(p:EEE) :=
  fun u v => L I (fun i=> p (V i u) (V i v)).

Lemma operation_function_is_magma: forall In  x p,
  magma x p -> magma (set_of_gfunctions In x)  (operation_function In p).
Proof.  ir. red. red. ir. nin (set_of_gfunctions_inc H0).
  nin (set_of_gfunctions_inc H1).
  uf operation_function. 
  set (g:= BL  (fun i : Set => p (V i a) (V i b)) In x). 
  set (f:= L In (fun i : Set => p (V i a) (V i b))). assert (f = graph g). tv.
  change (inc f (set_of_gfunctions (source g) (target g))). rw H4.
  app inc_set_of_gfunctions. uf g. app af_function. red. ir. app H.
  ee. wr H11. change (inc (W c x0) x). wr H10. app inc_W_target. rww H9.
  ee. wr H8. change (inc (W c x1) x). wr H7. app inc_W_target. rww H6.
Qed.

Definition sub_magma (x:Set)(p:EEE)(y:Set) := (magma y p) & (sub y x).

Lemma sub_magma_pr: forall x p y a b,
  sub_magma x p y -> inc a y -> inc b y -> inc (p a b) y.
Proof. ir. red in H. ee. app H. 
Qed.

Definition idempotent (x:Set)(p:EEE)(h:Set):= inc h x & p h h = h.

Lemma singleton_magma: forall x p a,
  sub_magma x p (singleton a) = idempotent x p a.
Proof. ir. app iff_eq. ir.  red in H. ee.  red in H. red in H. ee. 
  assert (inc a (singleton a)). fprops.
  red; ee. app H0.  app singleton_eq. app H.
  ir. red in H. ee. red. ee.  red. red. ir. assert (a0=a). app singleton_eq.
  assert (b=a). app singleton_eq. rw H3; rw H4; rw H0. fprops.
  red; ir. rww (singleton_eq H1).
Qed.

Definition p_of_sets x p a b := 
  Zo x (fun y=> exists u, exists v, inc u a & inc v b & y = p u v).
 
Lemma prod_of_sets_pr: forall x p a b u v,
  magma x p -> sub a x -> sub b x -> inc u a -> inc v b -> 
  inc (p u v) (p_of_sets x p a b).
Proof. ir. uf p_of_sets. Ztac. exists u. exists v. intuition. 
Qed. 

Lemma p_of_sets_is_magma: forall x p,
  magma (powerset x) (p_of_sets x p).
Proof. ir.  red. red. intros a b.  repeat rw powerset_inc_rw. ir.
  red. ir. ufi p_of_sets H1. Ztac. am.
Qed.

Lemma sub_magma_pr0: forall x p a,
  magma x p -> sub a x  ->  
  sub (p_of_sets x p a a) a = magma a p.
Proof. ir. app iff_eq. ir.  red. red.  ir. app H1. app prod_of_sets_pr.
  ir.  red. ir. ufi p_of_sets H2. Ztac. nin H4. nin H4. ee. rw H6.
  app H1.
Qed.

Definition opposite_law f:EEE := fun x y => f y x.

Lemma opposite_magma: forall E p, magma E p -> magma E (opposite_law p).
Proof. ir. red. red. ir. uf opposite_law. app H.
Qed.

Definition l_morphism (p p':EEE) (u:Set) (f:EE) :=
  forall a b, inc a u -> inc b u  ->f (p a b) = p' (f a) (f b).
Definition ma_morphism (p p':EEE)(m:Set) :=
  l_morphism p p' (sourceU m) (ev m).


Hint Rewrite ev_Uidentity source_Uidentity1: aw.


Lemma id_morphism: forall x p,
  magma (Ul x) p -> ma_morphism p p (Uidentity x).
Proof. ir. red.  aw. red. ir.  aw. app H.
Qed.

Lemma compose_ma_morphism: forall p p' p'' f g,
  magma (sourceU f) p 
  -> ma_morphism p p' f ->  ma_morphism p' p'' g ->
  Ucomposable g f -> ma_morphism p p'' (Ucompose g f).
Proof. unfold ma_morphism. ir. red.  rw source_Ucompose1.  ir.
  red in H2. ee. repeat rww ev_Ucompose.  wr H1. wrr H0. uf sourceU. rw H6. 
  change( inc (ev f a) (targetU f)). app mor_inc_ev. 
  uf sourceU. rw H6. change (inc (ev f b) (targetU f)). app mor_inc_ev. app H.
Qed.

Lemma isomorphism_pr: forall p p' f,
  magma(sourceU f) p -> magma (targetU f) p' -> Ubijective f
  -> ma_morphism p p' f -> ma_morphism p' p (Uinverse f).
Proof. ir. red. red. uf sourceU. uf Uinverse. rw source_Ucreate. ir.
  assert (Ha:inc (p' a b) (targetU f)). app H0. 
  repeat rww ev_Ucreate. 
  cp (Ubijective_transformation_bijective H1). nin H1. nin H1. nin H7.
  nin (surjective_pr8 H6 H3).  ufi sourceU  H9.
  nin (surjective_pr8 H6 H4).  ufi sourceU  H11.
  nin (surjective_pr8 H6 Ha).  ufi sourceU  H13.
  app H8. app H. rw H13. rww H2. rww H9. rww H11.
Qed.


Lemma mor_restrict: forall p p' f z,
  ma_morphism p p' f ->  magma (Ul z) p ->
  sub (Ul z) (Ul (sourceC f)) ->  ma_morphism p p' (mor_restr f z).
Proof. ir. red. red. uf sourceU. rw source_mor_restr. ir. 
  repeat  rww ev_mor_restr.  app H. app H1. app H1. app H0. 
Qed.

(** ** AI-1.1 Composition of an ordered sequence of elements *)
Import List. 


Definition mor_app_nelist(m:Set)(hyp:Uaxioms m)
  (l: nelist (Ul (sourceC m))): (nelist (Ul (targetC m))) :=
  ne_map  (mor_to_arrow hyp) l.

Definition mor_app_list(m:Set)(hyp:Uaxioms m)
  (l: list (Ul (sourceC m))): (list (Ul (targetC m))) :=
  map  (mor_to_arrow hyp) l.

Lemma inc_ne_compose: forall (y x:Set) (p:EEE) (l:nelist Set),
  magma y p -> sub x y -> nelist_subset l x -> inc (ne_compose p l) y.
Proof. ir. induction l. simpl. inversion H1. app H0.
  simpl. inversion H1. app H. app H0. app IHl.
Qed.


Lemma inc_n_compose: forall (y x:Set) (p:EEE) (e:Set) (l:list Set),
  magma y p -> sub x y -> list_subset l x -> inc e y -> inc (n_compose p e l) y.
Proof. ir. induction l. simpl. inversion H1. am. inversion H1.  
  induction l.  app H0. simpl. app H. app H0. app IHl.
Qed.

(*
Check list_Ro_inv_pr.

Lemma mor_of_comp2: forall (e e':Set)(p p':EEE)(m:Set)(hyp:Uaxioms m)
  (l : list (sourceU m)),
  magma (sourceU m) p
  -> ma_morphism p p' m ->  e' = ev m e -> 
  n_compose p' e' (mor_app_list hyp l) = ev m (n_compose p e l) .
Proof. ir. induction l. simpl. am.
  induction l. simpl. ap (mor_to_arrow_pr a hyp).  
  simpl. rw H0. simpl in IHl. wrr IHl. wrr (mor_to_arrow_pr a hyp).
  app R_inc. ap (inc_ncompose_aux1 e a0 l H).
Qed.



Lemma mor_of_comp2: forall (e e':Set)(p p':EEE)(m:Set)(hyp:Uaxioms m)
  (l : list (sourceU m)),
  magma (sourceU m) p
  -> ma_morphism p p' m ->  e' = ev m e -> 
  n_compose p' e' (mor_app_list hyp l) = ev m (n_compose p e l) .
Proof. ir. induction l. simpl. am.
  induction l. simpl. ap (mor_to_arrow_pr a hyp).  
  simpl. rw H0. simpl in IHl. wrr IHl. wrr (mor_to_arrow_pr a hyp).
  app R_inc. ap (inc_ncompose_aux1 e a0 l H).
Qed.

Lemma mor_of_comp: forall (p p':EEE)(m:Set)(hyp:Uaxioms m)
  (l : nelist (sourceU m)),
  magma (sourceU m) p
  -> ma_morphism p p' m ->
  ne_compose p' (mor_app_nelist hyp l) = ev m (ne_compose p l) .
Proof. ir. induction l. simpl. ap (mor_to_arrow_pr x hyp). 
  simpl. rww H0. wr (mor_to_arrow_pr x hyp). wrr IHl. 
  app R_inc. app inc_necompose. fprops.
Qed.

Lemma mor_of_comp2: forall (e e':Set)(p p':EEE)(m:Set)(hyp:Uaxioms m)
  (l : list (sourceU m)),
  magma (sourceU m) p
  -> ma_morphism p p' m ->  e' = ev m e -> 
  n_compose p' e' (mor_app_list hyp l) = ev m (n_compose p e l) .
Proof. ir. induction l. simpl. am.
  induction l. simpl. ap (mor_to_arrow_pr a hyp).  
  simpl. rw H0. simpl in IHl. wrr IHl. wrr (mor_to_arrow_pr a hyp).
  app R_inc. ap (inc_ncompose_aux1 e a0 l H).
Qed.
*)

(** A1-1-3 Associative laws *)

Definition p_associativity E p :=
  forall a b c, inc a E -> inc b E -> inc c E ->
    p (p a b) c = p a (p b c).

Definition identity_prop E p e :=
  (inc e E) & (forall a, inc a E-> p a e = a)  &
  (forall a, inc a E-> p e a = a).

Definition a_magma E p := magma E p & p_associativity E p.
Definition u_magma E p e := magma E p & identity_prop E p e.
Definition ua_magma E p e :=  
  magma E p & identity_prop E p e & p_associativity E p.

(*
Lemma neconcat_assoc: forall (y x:Set)(p:EEE)(l1 l2: nelist x),
  a_magma y p -> sub x y -> 
  p (ne_compose p l1)(ne_compose p l2) = ne_compose p (ne_append l1 l2).
Proof. ir. induction l1. simpl. tv. simpl. red in H. ee. rw H1.
  rww IHl1. app H0. app R_inc. app inc_necompose. app inc_necompose.
Qed.

Lemma nconcat_assoc: forall (y x:Set)(p:EEE)(e:Set)(l1 l2: list x),
  ua_magma y p e -> sub x y ->
  p (n_compose p e l1)(n_compose p e l2) = n_compose p e (app l1 l2).
Proof. ir. nin H.  nin H1; red in H1. ee.
  induction l1. simpl. ee. app H4. app inc_ncompose. 
  simpl. induction l1. simpl. induction l2. simpl. app H3. app H0. app R_inc. 
  tv. set (lhs:= p (p (Ro a) (n_compose p e (a0 :: l1))) (n_compose p e l2)).
  simpl. uf lhs. rw H2. app uneq.  app H0. app R_inc. 
  app inc_ncompose. app inc_ncompose.
Qed.

Lemma ne_gen_assoc: forall (y x:Set)(p:EEE)(l: nelist (nelist x))
  (H:magma y p) (H1:sub x y),  p_associativity y p ->
  ne_compose p (ne_map (fun u => Bo(inc_necompose u H H1)) l) =
  ne_compose p (ne_flatten l).
Proof. ir. induction l. simpl. rw B_eq. tv. simpl. 
  wrr (neconcat_assoc (y:=y)). rww IHl. rww B_eq. red. ee. am. am.
Qed.




Lemma gen_assoc: forall (y x:Set)(p:EEE)(e:Set)(l: list (list x)),
  a_magma y p -> sub x y ->  identity_prop y p e ->
  nn_compose p e l = n_compose p e (flatten l).
Proof. ir. induction l. simpl. tv. simpl. wrr (nconcat_assoc (y:=y)).
  rww IHl.  set (ft:=n_compose p e a). set (rm:=(n_compose p e (flatten l))).
  induction l. simpl in rm.  uf rm. induction H1. induction H2. rww H2.
  uf ft. app inc_ncompose. red in H; ee;am. tv.
Qed.
*)

(*
Lemma ne_gen_assoc: forall (y x:Set)(p:EEE)(l: nelist (nelist x)),
  a_magma y p -> sub x y -> nee_compose p l = ne_compose p (ne_flatten l).
Proof. ir. induction l. simpl. tv. simpl. wrr (neconcat_assoc (y:=y)). rww IHl. 
Qed.


Lemma gen_assoc: forall (y x:Set)(p:EEE)(e:Set)(l: list (list x)),
  a_magma y p -> sub x y ->  identity_prop y p e ->
  nn_compose p e l = n_compose p e (flatten l).
Proof. ir. induction l. simpl. tv. simpl. wrr (nconcat_assoc (y:=y)).
  rww IHl.  set (ft:=n_compose p e a). set (rm:=(n_compose p e (flatten l))).
  induction l. simpl in rm.  uf rm. induction H1. induction H2. rww H2.
  uf ft. app inc_ncompose. red in H; ee;am. tv.
Qed.
*)

(*


Fixpoint nee_compose(x:Set)(p:EEE)(l: nelist(nelist x)):Set :=
  match l with 
    | singl a => ne_compose p a 
    | necons a b => p (ne_compose p a) (nee_compose p b)
end.


Fixpoint nn_compose(x:Set)(p:EEE)(e:Set)(l: list(list x)):Set :=
  match l with 
    | nil => e 
    | a :: nil => n_compose p e a
    | a :: b => p (n_compose p e a) (nn_compose p e b)
end.


Lemma inc_neecompose:forall (y x:Set)(p:EEE)(l:nelist (nelist x)),
  magma y p -> sub x y -> inc (nee_compose p l) y.
Proof. ir. induction l. simpl. app inc_necompose. simpl. app H. 
  app inc_necompose.
Qed.
  
Lemma inc_nncompose:forall (y x:Set)(p:EEE)(e:Set)(l:list (list x)),
  magma y p -> sub x y -> inc e y->inc (nn_compose p e l) y.
Proof. ir. induction l. simpl. am. simpl.    
  induction l.  app inc_ncompose.  app H. app inc_ncompose.
Qed.


Definition nee_compose_aux(x:Set)(p:EEE)(H:magma x p)
  (l: nelist(nelist x)): (nelist x) :=
  ne_map (fun a => (Bo (inc_necompose_aux a H))) l.


Definition nn_compose_aux(x:Set)(p:EEE)(e:Set)(H:magma x p)(He: inc e x)
  (l: list(list x)): (list x) :=
  map (fun a => (Bo (inc_ncompose_aux a H He))) l.

*)




End BasicAlgebra.
Export BasicAlgebra.








(* Formule 2 page I.4 *) 
 (* le lemme est bizarre *)

(* Page I.4 Paragraph 1 number 3 *) 

(* Theoreme 1 *) 

Fixpoint nelist_of (x:Set)(y:x)(n:nat) : nelist x:=
  match n with 
    | 0 => singl y
    | 1 => singl y 
    | S k => necons y (nelist_of y k)
end.

Require Export List.

Fixpoint list_of (x:Set)(y:x)(n:nat) : list x:=
  match n with 
    | 0 => nil
    | S k => y :: (list_of y k)
end.


Lemma pos_has_prec: forall n:nat, n > 0 -> exists n0:nat, n = S n0.
Proof. ir. red in H. red in H. induction H. exists 0. tv.  exists m. tv.
Qed.

Lemma nelist_concat: forall (x:Set)(y:x)(n m:nat),
  n > 0 -> m > 0 ->
  ne_append (nelist_of y n)(nelist_of y m) = nelist_of y (n+m). 
Proof. ir. assert (exists n0:nat, n = S n0). app pos_has_prec.  
   assert (exists m0:nat, m = S m0). app pos_has_prec. nin H1; nin H2.
   rw H1. rw H2. clear H1.  
   induction x0. simpl. tv. simpl. app nelist_simpl2.
Qed.

Lemma list_concat: forall (x:Set)(y:x)(n m:nat),
  app (list_of y n)(list_of y m) = list_of y (n+m). 
Proof. ir. induction n.  simpl. tv. simpl. rw IHn. tv. Qed. 

Lemma succ_is_pos: forall n:nat, S n> 0.
Proof. ir. red. red. app le_n_S. app le_O_n.  Qed.

Lemma prod_of_succ_is_pos: forall n m:nat, S n * S m > 0.
Proof. ir. red. red. assert (1=1*1). ring.  rw H.
  app mult_le_compat. app le_n_S. app le_O_n. app le_n_S. app le_O_n. Qed.

Lemma nelist_concat2:forall (x:Set)(y:x)(n m:nat),
  n>0 -> m>0 -> 
  ne_flatten(nelist_of(nelist_of y n) m) = nelist_of y (n*m).
Proof. ir. assert (exists n0:nat, n = S n0). app pos_has_prec.  
   assert (exists m0:nat, m = S m0).  app pos_has_prec. nin H1; nin H2.  
   rw H1; rw H2. clear H2. clear H1.  
   induction x1. assert (S x0 * 1 = S x0 ). ring. rw H1. simpl. tv.
   set(mm:= S x1).  fold mm in IHx1.
   set(rhs:=nelist_of y (S x0 * S mm)).
   set (il:=nelist_of y (S x0)). fold il in IHx1. 
   simpl. set (aux:=ne_flatten (nelist_of il mm)). fold aux in IHx1.  
   simpl in aux. fold aux. rw IHx1. uf il.  rw nelist_concat. uf rhs.
   assert(S x0 * S mm= S x0 + S x0 * mm). ring.  rww H1. app succ_is_pos.
   uf mm. app prod_of_succ_is_pos.
Qed.

Lemma list_concat2:forall (x:Set)(y:x)(n m:nat),
  flatten(list_of( list_of y n) m) = list_of y (n*m).
Proof. ir. induction m. assert (n*0=0). ring.  rw H. simpl. tv.
  simpl. rw IHm. assert (n* S m = n + (n* m)). ring. rw H. rww list_concat.
Qed.

Definition ne_power(x:Set)(p:EEE)(y:Set)(hyp: inc y x)(n:nat) :=
  ne_compose p (nelist_of (Bo hyp)  n).

Definition n_power(x:Set)(p:EEE)(e:Set)(y:Set)(hyp: inc y x)(n:nat) :=
  n_compose p e (list_of (Bo hyp)  n).

Lemma inc_ne_power: forall(x:Set)(p:EEE)(y:Set)(hyp: inc y x)(n:nat),
  a_magma x p->inc (ne_power p hyp n) x.
Proof. ir.  uf ne_power. app inc_necompose.  red in H; ee; am. red; tv. Qed.

Lemma inc_n_power: forall(x:Set)(p:EEE)(y:Set)(e:Set)(hyp: inc y x)(n:nat),
  a_magma x p->identity_prop x p e -> inc (n_power p e hyp n) x.
Proof. ir. uf n_power. app inc_ncompose.  red in H; ee; am. red; tv. 
  red in H0. ee. am. Qed.

Lemma n_power_0:forall (x:Set)(p:EEE)(y:Set)(H:inc y x)(e:Set),
  n_power p e H 0= e.
Proof. ir. uf n_power. simpl. tv. Qed.

Lemma n_power_1:forall (x:Set)(p:EEE)(y:Set)(H:inc y x)(e:Set),
  n_power p e H 1= y.
Proof. ir. uf n_power. simpl. app B_eq. Qed.

Lemma ne_power_1:forall (x:Set)(p:EEE)(y:Set)(H:inc y x),
  ne_power p H 1= y.
Proof. ir. uf ne_power. simpl. app B_eq. Qed.

Lemma n_power_S:forall (x:Set)(p:EEE)(y:Set)(H:inc y x)(e:Set)(n:nat),
  y = p y e-> n_power p e H (S n)= p y (n_power p e H n).
Proof. ir. uf n_power. uf list_of. rw n_compose_next. tv. am. Qed.

Lemma ne_power_S:forall (x:Set)(p:EEE)(y:Set)(H:inc y x)(n:nat),
  n>0 -> ne_power p H (S n)= p y (ne_power p H n).
Proof. ir. uf ne_power. assert (exists n0:nat, n = S n0). app pos_has_prec.
  nin H1.  rw H1.  uf nelist_of. rw ne_compose_next. tv. Qed.

Lemma ne_n_power:forall  (x:Set)(p:EEE)(y:Set)(H:inc y x)(e:Set)(n:nat),
  n>0 ->  y = p y e-> ne_power p H n = n_power p e H n.
Proof. ir. pose (pos_has_prec H0). nin e0. rw H2. clear H2. induction x0.
  rw n_power_1; rw ne_power_1; tv.  rw n_power_S. rw ne_power_S. rww IHx0.
  app succ_is_pos. am.
Qed.


Lemma ne_power_mult:forall (x:Set)(p:EEE)(y:Set)(H:inc y x)(n m:nat),
  a_magma x p -> n>0 -> m>0 ->
   ne_power p H (n+m) = p (ne_power p H n) (ne_power p H m).
Proof.  ir.  uf ne_power. rw (neconcat_assoc(y:=x)).
  rww nelist_concat. am. red;tv.
Qed.

Lemma n_power_mult:forall (x:Set)(p:EEE)(y:Set)(H:inc y x)(e:Set)(n m:nat),
  a_magma x p -> identity_prop x p e ->
   n_power p e H (n+m) = p (n_power p e H n) (n_power p e H  m).
Proof. ir. uf n_power. rw (nconcat_assoc(y:=x)). 
  rww list_concat. am. red;tv. am.
Qed.

Lemma nn_power_mult:forall (x:Set)(p:EEE)(e:Set)(y:Set)(H:inc y x)(n m:nat)
  (Ha:a_magma x p)(Hb:identity_prop x p e),
   n_power p e H (n*m) = n_power p e (inc_n_power  H n Ha Hb) m.
Proof. ir. induction m. assert (n*0=0).  ring. rw H0. uf n_power. simpl. tv.
  assert (n * S m= n + n*m). ring. rw H0. rww n_power_mult. rw IHm. clear IHm. 
  rw n_power_S. tv.  cp Hb. red in Hb. ee. sy; app H3. app inc_n_power.  
Qed.

Lemma nne_power_mult:forall (x:Set)(p:EEE)(y:Set)(H:inc y x)(n m:nat)
  (Ha:a_magma x p), n>0 -> m >0 ->
   ne_power p H (n*m) = ne_power p (inc_ne_power  H n Ha) m.
Proof. ir. 
  assert (exists n0:nat, n = S n0). app pos_has_prec.  
  assert (exists m0:nat, m = S m0).  app pos_has_prec. nin H2; nin H3.  
  rw H2; rw H3. clear H3. induction x1. rw ne_power_1.  
  assert (S x0 *1= S x0).  ring. rww H3.
  assert ((S x0) * S (S x1) = (S x0) + (S x0)*(S x1)). ring. rw H3.
  rww ne_power_mult. rw IHx1. clear IHx1. rw ne_power_S. tv.
  app succ_is_pos. app succ_is_pos.  app prod_of_succ_is_pos. 
Qed.

(* page A1.6. Paragraph 1 number 4*)

Lemma amagma_is_magma: forall(x:Set)(p:EEE), a_magma x p -> magma x p.
Proof. ir. red in H. ee. am. Qed.

Lemma monoid_is_amagma: forall (g:Set), monoid_axioms g -> 
  a_magma (Ul g) (dplus g).
Proof. ir. red in H. red in H. ee. red. split. red. app H0. red. app H1.
Qed.

Lemma ring_is_amagma: forall (g:Set), ring_axioms g -> a_magma (Ul g) (dmult g).
Proof. ir. red in H. red in H. ee. red. split. red. app H0. red. app H2.
Qed.

Lemma monoid_is_magma: forall (g:Set), monoid_axioms g -> magma (Ul g) (dplus g).
Proof. ir. app amagma_is_magma. app monoid_is_amagma. Qed.

Lemma ring_is_magma: forall (g:Set), ring_axioms g -> magma (Ul g) (dmult g).
Proof. ir. app amagma_is_magma. app ring_is_amagma. Qed.

Hint Resolve ring_is_amagma ring_is_magma monoid_is_amagma monoid_is_magma
  amagma_is_magma : bs. 
Ltac bs:= auto with bs. 

Lemma magma_intersection: forall (p:EEE)(x:Set),
  nonempty x ->
  (forall y:Set, inc y x -> magma y p) -> magma (intersection x) p.
Proof. ir. red. red. ir. app intersection_inc.  ir.
  assert (inc a y). apply intersection_forall with x. am. am.
  assert (inc b y). apply intersection_forall with x. am. am.
  ufi magma H0. ufi Operations.is_law2I H0. app H0. 
Qed.

Definition generated_by (x:Set)(p:EEE)(y:Set) :=
 intersection(Zo (powerset x) (fun z=> (magma z p) & (sub y z))).

Lemma generated_by_magma: forall (x:Set)(p:EEE)(y:Set),
  magma x p -> sub y x -> magma (generated_by x p y) p.
Proof. ir.  uf generated_by. app magma_intersection. 
  exists x. Ztac. app inc_x_powerset_x. ir. Ztac. am.
Qed.

Lemma generated_by_contains: forall (p:EEE)(x y:Set),
  magma x p -> sub y x -> sub y (generated_by x p y).
Proof. ir. uf generated_by. red. ir. app intersection_inc. exists x. Ztac.
  app inc_x_powerset_x. ir. Ztac. app H5.
Qed.

Lemma generated_by_smallest: forall (p:EEE)(x y z:Set),
  magma x p ->  sub y x -> sub_magma x p z -> 
  sub y z -> sub (generated_by x p y) z.
Proof. ir. red in H1; ee. uf generated_by. apply intersection_sub. Ztac. 
  app powerset_inc. 
Qed.

Lemma generated_by_small: forall (p:EEE)(x y :Set),
  magma x p -> sub y x -> sub (generated_by x p y) x.
Proof. ir. app generated_by_smallest. red; split. am. red. tv.
Qed.

Lemma generated_by_submagma: forall (p:EEE)(x y :Set),
  magma x p -> sub y x -> sub_magma x p (generated_by x p y).
Proof. ir. split. app generated_by_magma. app generated_by_small. Qed.


Lemma magma_image_bis: forall (p p':EEE)(f:Set)(x:Set),
  ma_morphism p p' f -> sub_magma (sourceU f) p x -> 
  magma (mor_image x f) p'.
Proof.  ir. red.  red. ir. rwi mor_image_inc_rw H1. rwi mor_image_inc_rw H2.
  nin H1; nin H2. ee. rw mor_image_inc_rw. red in H0; ee. 
  exists (p x0 x1). ee. app H0. wr H4; wr H3. app H. app H5. app H5.
Qed.

Lemma magma_image: forall (p p':EEE)(m:Set),
  ma_morphism p p' m -> magma (sourceU m) p -> 
  magma (mor_range m) p'.
Proof. ir.  rw range_is_image. apply magma_image_bis with p. am.
  red. split. am. red; tv.
Qed.

Lemma magma_inv_image: forall (p p':EEE)(m:Set)(z:Set),
  ma_morphism p p' m -> magma (sourceU m) p ->  magma z p' -> 
  mor_saxioms m-> magma (mor_inv_image z m) p.
Proof. ir. red; red. ir. pose (mor_inv_image_pr H2 H3).  
  pose (mor_inv_image_pr  H2 H4). ee. red in H.
  app mor_inv_image_inc. app H0. rww H. app H1.
Qed.

Lemma stable_same:forall (p p':EEE)(f g x:Set),
  ma_morphism p p' f  -> ma_morphism p p' g -> sourceC f = sourceC g->
  sub_magma  (sourceU f) p x  -> magma (Zo (x) (fun y=> ev f y = ev g y)) p.
Proof. ir. red. red. ir. Ztac. clear H4. Ztac. clear H3. red in H2. ee. Ztac.
  red in H. rww H. rw H6; rw H7. sy. red in H0. app H0. ufi sourceU H3. 
  uf sourceU.
  wr H1. app H3.  ufi sourceU H3. uf sourceU. wr H1. app H3. app H3. app H3.
Qed.

Lemma created_mor: forall (p p':EEE)(f:Set)(x:Set),
  let u := (sourceU f) in
  ma_morphism p p' f -> sub x u -> magma u p -> mor_saxioms f->
  (mor_image (generated_by u p x) f) = 
  generated_by (mor_image u f)  p' (mor_image x f).
Proof.  ir.
  set (barx:= (generated_by u p x)).
  set (barf:= generated_by (mor_image u f) p' (mor_image x f)).
  assert (sub barx u). uf barx. app generated_by_small.
  assert(sub (mor_image x f) (mor_image u f)). app increasing_image.
  assert (magma (mor_image u f) p'). apply magma_image_bis with p; try am.
  red. split. am. red; tv.
  assert(magma (mor_image barx f) p'). 
  uf barx. apply magma_image_bis with p; try am. app generated_by_submagma.
  assert (sub barf (mor_image barx f)). 
  uf barf. app generated_by_smallest.  
  red. split. am. app increasing_image.  app increasing_image. 
  uf barx. app generated_by_contains.
  assert (sub barx (mor_inv_image barf f)).
  uf barx. app generated_by_smallest. red. split. 
  apply magma_inv_image with p'; try am.
  uf barf. app generated_by_magma.  uf u. app inverse_image_sub.
  app sub_inv_image. uf barf. app generated_by_contains. 
  assert (sub (mor_image barx f) barf). 
  apply sub_inv_image2. am. am. am.
  app extensionality.
Qed.


Definition finite_combs (x:Set)(p:EEE)(y:Set) :=
  Zo x (fun w => exists l:nelist y, w = ne_compose p l).

(* proposition 2 page A I.7 *) 
Lemma generated_is_finite_combs:forall(x:Set)(p:EEE)(y:Set),
  a_magma x p -> sub y x-> generated_by x p y = finite_combs x p y.
Proof. ir.  set (K:=generated_by x p y). set  (Q:= finite_combs x p y).
  assert(sub y Q). uf Q; uf sub; ir. uf finite_combs. Ztac. 
  exists (singl (Bo H1)). uf ne_compose. sy. app B_eq.
  assert (sub Q x). uf Q. uf finite_combs. uf sub;ir. Ztac. am.
  assert (forall l:nelist y, inc (ne_compose p l) K). ir.
  assert (magma K p). uf K; app generated_by_magma. red in H; ee;am.
  assert (sub y K). uf K; app generated_by_contains. red in H; ee;am.  
  induction l. simpl. app H4. app R_inc. simpl. app H3. app H4. app R_inc.
  assert (sub Q K). uf Q; uf sub; uf finite_combs. ir. Ztac. nin H6. rww H6.
  assert (sub_magma x p Q). red; ir. ee. red. red. uf Q; uf finite_combs. ir.
  Ztac.  clear H6. Ztac. clear H5. Ztac. red in H; ee. app H.
  nin H8; nin H9. exists (ne_append x1 x0). wr (neconcat_assoc (y:=x)).
  rw H5; rww H8.
  am.  am. am. assert (sub K Q). uf K. app generated_by_smallest.
  red in H; ee; am. app extensionality.
Qed.

Definition idempotent (x:Set)(p:EEE)(h:Set):= inc h x & p h h = h.

(* section 1; number 5, page A1.7 *)



Definition ac_magma (x:Set)(p:EEE):= (a_magma x p) & (pcommutativity x p).

Definition commutant (u:Set)(p:EEE)(a:Set) := 
  Zo u (fun y=> forall x:Set, inc x a -> commutes p x y).
 
Lemma commutes_symm: forall (f:EEE)(x y:Set),
  commutes f x y -> commutes f y x.
Proof. uf commutes. ir. sy. tv. Qed.

Lemma commutant_sub_u: forall (u:Set)(p:EEE)(x:Set), 
  sub (commutant u p x) u.
Proof. ir. red. ir.  ufi commutant H. Ztac.  am. Qed.

Lemma commutant_contravariant: forall (u:Set)(f:EEE)(x x':Set), 
  sub x x' -> sub (commutant u f x') (commutant u f x).
Proof. ir. red. ir. ufi commutant H0. Ztac. uf commutant.
  app Z_inc. ir. app H2. app H.
Qed.

Lemma commutant_union2: forall (u:Set)(f:EEE)(x x':Set), 
  commutant u f (union2 x x') =  
  intersection2 (commutant u f x) (commutant u f x').
Proof. uf commutant. ir. set_extens. pose (Z_all H). ee. clear H.
  app intersection2_inc.  Ztac. ir. app H1. app union2_first.
  Ztac. ir.  app H1. app union2_second.
  pose (intersection2_first H).  pose (intersection2_second H).
  pose (Z_all i);pose (Z_all i0); ee.
  app Z_inc. ir. rwi inc_union2_rw H4. nin H4. app H3. app H1.
Qed.


Lemma sub_bicommutant:  forall (u:Set)(f:EEE)(x:Set), 
  sub x u -> sub x (commutant u f (commutant u f x)).
Proof. ir. red. ir. unfold commutant. Ztac. ir. Ztac. app commutes_symm.
  app H3.
Qed.

Lemma eq_tricommautant:  forall (u:Set)(f:EEE)(x:Set), sub x u -> 
  commutant u f (commutant u f (commutant u f x)) = (commutant u f x).
Proof. ir.  apply extensionality. 
  set (y:=(commutant u f (commutant u f x))).
  assert (sub x y).  uf y. app sub_bicommutant. app commutant_contravariant. 
  app sub_bicommutant. red. ir. ufi commutant H0. Ztac. am.
Qed.

Definition pcommutes (g:Set):= commutes (dplus g).
Definition pcommutant (g:Set) := commutant (Ul g) (dplus g).
Definition mcommutes (g:Set):= commutes (dmult g).
Definition mcommutant (g:Set) := commutant (Ul g) (dmult g).

Lemma inc_commutant_rw: forall (u:Set)(f:EEE)(x z:Set), magma u f -> sub x u ->
  inc z (commutant u f x) = 
  (inc z u & forall y:Set, inc y x -> commutes f y z).
Proof. ir. uf commutant; uf commutes. ap iff_eq. 
  ir. ufi commutant H0. Ztac. am. am. 
  ir.  ee. Ztac.
Qed.

Lemma inc_pcommutant_rw: forall (g x z:Set),
  monoid_axioms g ->  sub x (Ul g) ->  
  inc z (pcommutant g x) = 
  (inc z (Ul g) & forall y:Set, inc y x -> pcommutes g y z).
Proof. ir. uf pcommutant; uf pcommutes. app inc_commutant_rw. 
  red. red in H. red in H. ee. app H1.
Qed.

Lemma inc_mcommutant_rw: forall (g x z:Set), ring_axioms g ->  sub x (Ul g) -> 
  inc z (mcommutant g x) = 
  (inc z (Ul g) & forall y, inc y x -> mcommutes g y z).
Proof. ir. uf mcommutant; uf mcommutes. app inc_commutant_rw. 
  red. red in H. red in H. ee. app H1.
Qed.

Lemma commutes_op: forall (u:Set)(f:EEE)(x y z:Set), 
  a_magma u f -> inc x u -> inc y u -> inc z u 
  -> commutes f x y -> commutes f x z
  -> commutes f x (f y z).
Proof. uf commutes. ir. red in H. ee. red in H5. rww H5.  wr H4. 
  wrr H5. rw H3. rww H5. 
Qed.

Lemma commutant_magma: forall u (p:EEE) x, a_magma u p ->  sub x u
  -> sub_magma u p (commutant u p x).
Proof. ir. red. ee. assert (magma u p). bs. red. red. ir.
  rwii inc_commutant_rw H3. rwii inc_commutant_rw H2.
  rww inc_commutant_rw. ee. mp. ir. apply commutes_op with u. am. 
  app H0. am. am. app H5. app H4.  app commutant_sub_u.
Qed.

Definition set_commutation (p:EEE) x y:=
  forall (a b:Set), inc a x -> inc b y -> commutes p a b.

Lemma set_commutation_generated: forall (u:Set)(p:EEE)(x y:Set),
  a_magma u p -> sub x u -> sub y u ->
  set_commutation p x y ->
  set_commutation p (generated_by u p x) (generated_by u p y).
Proof. ir. set (sx:=generated_by u p x) ; set (sy :=generated_by u p y).
  assert (Hx:magma u p). red in H; ee;am.
  set(x':= commutant u p x). 
  pose (Ha:=commutant_magma H H0). fold x' in Ha. cp Ha. red in H3;ee.
  pose (Hb:=commutant_magma H H4). cp Hb. red in H5;ee.
  assert(sub x (commutant u p x')). uf x'; app sub_bicommutant.
  assert(sub y x').  red; ir. red in H2. uf x'. rww inc_commutant_rw. ee. 
  app H1. ir. app H2.   
  assert(sub sx  (commutant u p x')). uf sx. app generated_by_smallest. 
  assert (sub sy x'). unfold sy. app generated_by_smallest. 
  red. ir. assert (inc a (commutant u p x')). app H9. 
  rwii inc_commutant_rw H13. ee. app commutes_symm. app H14. app H10. 
Qed.



Lemma pcommutes_plus: forall (g x y z:Set), monoid_axioms g -> inc x (Ul g) ->
  inc y (Ul g) -> inc z (Ul g) -> pcommutes g x y -> pcommutes g x z ->
  pcommutes g x (dplus g y z).
Proof. uf pcommutes. ir.  apply commutes_op with (Ul g); try am. bs. 
Qed.

Lemma mcommutes_mult: forall (g x y z:Set), ring_axioms g -> inc x (Ul g) ->
  inc y (Ul g) -> inc z (Ul g) -> mcommutes g x y -> mcommutes g x z ->
  mcommutes g x (dmult g y z).
Proof. uf mcommutes. ir.  apply commutes_op with (Ul g); try am. bs. 
Qed.


Lemma pcommutant_magma:  forall (g x:Set), monoid_axioms g -> sub x (Ul g) ->
  sub_magma (Ul g) (dplus g) (pcommutant g x).
Proof.  ir. uf pcommutant. apply commutant_magma; try am. bs. 
Qed.

Lemma mcommutant_magma: forall (g x:Set), ring_axioms g -> sub x (Ul g) ->
  sub_magma (Ul g) (dmult g) (mcommutant g x).
Proof. ir. uf mcommutant. apply commutant_magma; try am. bs. 
Qed.


Lemma generated_by_singleton:forall (x:Set)(p:EEE)(a:Set)(hyp:inc a x),
  a_magma x p ->
  generated_by x p (singleton a) = Zo (x)(fun w=> exists n:nat,
    n>0 & w= ne_power p hyp n).
Proof. ir. set (s1:=Zo x (fun w : Set => exists n : nat, n > 0 
  & w = ne_power p hyp n)). set (sa:=(singleton a)).
  set (s2:=generated_by x p (singleton a) ).
  assert(Ha:=H). red in H; ee.
  assert(Hb:sub (singleton a) x). red. ir. assert(x0=a). app singleton_eq.
  rww H2.
  assert (sub s1 x). red. ir. ufi s1 H1. Ztac. am. 
  assert (sub sa s1). uf sa. red. ir. assert(x0=a). app singleton_eq. rw H3.
  uf s1. Ztac. exists 1. ee. red. red. app le_refl. sy; rw ne_power_1. tv.
  assert (sub_magma x p s1). red. ee. red.  red. uf s1. ir. Ztac. clear H4.
  Ztac. clear H3. nin H6. nin H7. ee. Ztac.
  exists (x1+x0). ee. red. red. red in H6. red in H6. app le_plus_trans.
  rw H8. rw H7. sy. app ne_power_mult. am.
  assert (sub s2 s1). uf s2. app generated_by_smallest. 

  assert (sub s1 s2). red. ir. ufi s1 H5. Ztac. induction H7. ee.
  assert (exists n:nat, x1 = S n). app pos_has_prec. nin H9. rw H8. rw H9.
  assert (sub s2 x). red. ir. app H1. app H4. clear H9.
  assert (inc a s2). pose (generated_by_contains H Hb). app s.
  app singleton_inc. 
  induction x2. rww ne_power_1. rw ne_power_S. 
 pose (generated_by_magma H Hb).
  uf s2. app m.  app succ_is_pos. app extensionality.
Qed. 

Lemma power_commutes: forall (u:Set)(p:EEE)(x y:Set)
  (Ha:a_magma u p) (Hx:inc x u)(Hy:inc y u)(n m :nat),
  commutes p x y -> n>0 -> m>0 ->
  commutes p (ne_power p Hx n)(ne_power p Hy m).
Proof. ir. set (six:= singleton x). set (siy:= singleton y).
  assert (set_commutation p six siy). red. ir.
  assert (a = x). ufi six  H2. app singleton_eq. 
  assert (b = y). ufi siy H3. app singleton_eq.  rw H4; rw H5; am.
  set (gx := (generated_by u p six)). set (gy := (generated_by u p siy)).
  assert (inc (ne_power p Hx n) gx).
  uf gx. uf six. rw (generated_by_singleton  Hx Ha). Ztac. app inc_ne_power.
  exists n. intuition.
  assert (inc (ne_power p Hy m) gy).
  uf gy. unfold siy. rw (generated_by_singleton  Hy Ha). Ztac. 
  app inc_ne_power. exists m. intuition.
  assert (set_commutation p gx gy).  uf gx; uf gy.
  app set_commutation_generated. uf six. red.  ir.  assert (x0=x). 
  app singleton_eq. rww H6. red. ir. assert (x0=y). app singleton_eq. rww H6. 
  app H5.
Qed.

Lemma power_commutes_gen: forall (u:Set)(p:EEE)(e:Set)(x y:Set)
  (Ha:a_magma u p) (Hx:inc x u)(Hy:inc y u)(n m :nat),
  identity_prop u p e -> commutes p x y ->
  commutes p (n_power p e Hx n)(n_power p e Hy m).
Proof. ir. induction n. set(w:=(n_power p e Hy m)).
  assert (inc w u). uf w. app inc_n_power.
  uf n_power. simpl. red. red in H. ee.
  transitivity w. app H3. sy. app H2.
  set(xn:= (n_power p e Hx (S n))). induction m. uf n_power. simpl.
  assert (inc xn u). uf xn. app inc_n_power.
  red. red in H. ee. transitivity xn. app H2. sy. app H3.
  assert(ne_power p Hx (S n)=xn). uf xn. app ne_n_power. app succ_is_pos.
  red in H. ee. sy. app H1.
  assert(ne_power p Hy (S m) = n_power p e Hy (S m)).
  app ne_n_power. app succ_is_pos. red in H. ee. sy. app H2. 
  wr H1; wr H2. app power_commutes. app succ_is_pos.  app succ_is_pos.
Qed.
  
Lemma generated_by_ac: forall (u:Set)(p:EEE)(x:Set),
  a_magma u p-> sub x u-> pcommutativity x p->
  ac_magma (generated_by u p x) p.
Proof. ir. assert (sub (generated_by u p x) u). app generated_by_small. bs.
  red. split. red. split. app generated_by_magma. bs.
  red. ir. red in H.  ee. app H6. app H2. app H2.  app H2.
  set (w:=generated_by u p x). assert (set_commutation p w w).
  uf w. app set_commutation_generated. app H3.
Qed.


Definition morphism_plus (g g':Set) := ma_morphism (dplus g)(dplus g').
Definition morphism_mult (g g':Set) := ma_morphism (dmult g)(dmult g').
Definition p_center (x:Set)(p:EEE):= commutant x p x.
Definition m_center (g:Set):= pcommutant g (Ul g).
Definition r_center (g:Set):= mcommutant g (Ul g).
Definition p_central (u:Set)(p:EEE)(x:Set) := inc x (p_center u p).
Definition m_central (g x:Set) := inc x (m_center g).
Definition r_central (g x:Set) := inc x (r_center g).

Lemma inc_pcenter_rw: forall (u:Set)(p:EEE)(z:Set),  magma u p->
  p_central u p z =  (inc z u & forall y, inc y u -> commutes p y z).
Proof. ir. uf p_central. uf p_center. rww inc_commutant_rw. app sub_refl.
Qed.

Lemma sub_pcenter_u: forall (u:Set)(p:EEE),  magma u p-> sub (p_center u p) u.
Proof. ir.  red. ir. ufi p_center H0. ufi commutant H0. Ztac. am.
Qed.

Lemma inc_mcenter_rw: forall (g z:Set), monoid_axioms g ->
  m_central g z =  (inc z (Ul g) & forall y, inc y (Ul g) -> pcommutes g y z).
Proof. ir. uf pcommutes. wrr inc_pcenter_rw. bs.
Qed.

Lemma inc_rcenter_rw: forall (g z:Set), ring_axioms g ->
  r_central g z =  (inc z (Ul g) & forall y, inc y (Ul g) -> mcommutes g y z).
Proof. ir. uf mcommutes. wrr inc_pcenter_rw. bs.
Qed.

Lemma pcenter_stable: forall (u:Set)(p:EEE)(x y z:Set), a_magma u p->
  p_central u p x -> p_central u p y -> p_central u p (p x y).
Proof. uf p_central. uf p_center. ir. assert (sub u u). app sub_refl. 
  pose (commutant_magma H H2). red in (type of s).  ee. app H3. 
Qed.

Lemma pcenter_amagma: forall (u:Set)(p:EEE)(x y z:Set), a_magma u p->
  sub_magma u p (p_center u p).
Proof.  ir. unfold p_center. app commutant_magma. app sub_refl. 
Qed.

Lemma m_center_comm: forall (u:Set)(p:EEE)(x y:Set), a_magma u p ->
  p_central u p x -> p_central u p y -> p x y = p y x.
Proof. ir. rwii inc_pcenter_rw  H0. rwii inc_pcenter_rw  H1. ee.
  unfold commutes in H2. app H2. bs. bs.
Qed.

Definition hom_product (p':EEE)(f g:Set):=
  Ucreate (sourceC f) (targetC f) (fun x:Set=> p' (ev f x) (ev g x)).
  
Lemma magma_hom_prod: forall (p p':EEE)(f g:Set),
  magma (sourceU f) p -> ac_magma (targetU f) p' -> 
  sourceC f = sourceC g -> targetC f = targetC g -> 
  mor_saxioms f -> mor_saxioms g ->
  ma_morphism p p' f  -> ma_morphism p p' g
  -> ma_morphism p p' (hom_product p' f g).
Proof. ir. red. red. uf hom_product. uf sourceU. rw source_Ucreate. ir.
  repeat rww ev_Ucreate.
  assert (inc a (Ul (sourceC g))). wrr H1.
  assert (inc b (Ul (sourceC g))). wrr H1.
  rww H5. rww H6.
  set (fa:= ev f a); set (fb:= ev f b); set (ga:= ev g a); set (gb:= ev g b). 
  assert (inc fa (targetU f)). uf fa; app mor_inc_target.
  assert (inc fb (targetU f)). uf fb;  app mor_inc_target.
  assert (inc ga (targetU f)). uf targetU; uf ga; rww H2. 
  change (inc (ev g a) (targetU g)). app mor_inc_target.
  assert (inc gb (targetU f)). uf targetU;  uf gb; rww H2.
  change (inc (ev g b) (targetU g)). app mor_inc_target.
  ufi ac_magma H0. ufi a_magma H0. ee. red in H15; red in H16. 
  assert (p' fb (p' ga gb) = p' ga (p' fb gb)).
  wrr H16. wrr H16. assert (p' fb ga = p' ga fb). app H15. wrr H17.
  rww H16. rww H16. rww H17. app H0. app H0. app H.
Qed.

(* Page A I.10 paragraph 1  number 6 *)
Import Relation.

Definition compatible_equivalence(u:Set)(p:EEE)(r:Set):=
  forall (x y x' y':Set), inc x u -> inc x' u -> inc y u -> inc y' u
    -> related r x x' -> related r y y' -> related r (p x y) (p x' y').

Definition quotient_law(p:EEE)(r:Set):=
  fun x y => W (p (rep x) (rep y)) (canon_proj r).

Definition compatible_eq (u:Set)(p:EEE)(r:Set):=
  (compatible_equivalence u p r) &(u= substrate r) &(is_equivalence r).

(*
Lemma compatible_eq_prod: forall (u:Set)(p:EEE)(r:Set),
  u= substrate r -> compatible_equivalence u p r = 
  compatible_with_equivs (fun x => p (P x)(Q x)) (prod_of_relation r r) r.
Proof. ir. uf compatible_equivalence. uf compatible_with_equivs.
  app iff_eq. ir. pose(prod_of_rel_pr H1). ee.
  pose (inc_relate_substrate H4).  pose (inc_relate_substrate H5). ee.
  rewrite <- H in H6, H7, H8, H9.   app H0.
  ir. set (a:=J x y). set (b:= J x' y').
  assert (x = P a). uf a; rww pr1_pair. rw H7.
  assert (y = Q a). uf a; rww pr2_pair. rw H8.
  assert (x' = P b). uf b; rww pr1_pair. rw H9.
  assert (y' = Q b). uf b; rww pr2_pair. rw H10.
  app H0. app prod_of_rel_inpr. ee. uf a; app pair_is_pair.
  uf b; app pair_is_pair. wr H7; wrr H9. wr H8; wrr H10.
Qed.

Lemma compatible_eq_magma: forall (u:Set)(p:EEE)(r:Set),
  is_relation r-> u= substrate r -> compatible_equivalence u p r = 
  magma r (operation_product p p).
Proof. ir.  uf operation_product. uf compatible_equivalence. 
  app iff_eq. ir.  red.  red.  ir.  app H1. rw H0. app inc_pr1_substrate.
  rw H0. app inc_pr2_substrate. rw H0. app inc_pr1_substrate. 
  rw H0. app inc_pr2_substrate. red.  assert (J (P a) (Q a) =a).
  app pair_recov. app H. rww H4. assert (J (P b) (Q b) =b).
  app pair_recov. app H. red. rww H4.
  ir. set (a:= J x x'); set (b:= J y y'). assert (inc a r). uf a; app H6.
  assert (inc b r). uf b; app H7. pose (H1 a b H8 H9). simpl in i.
  assert (x = P a). uf a; rww pr1_pair. wri H10 i.
  assert (x' = Q a). uf a; rww pr2_pair. wri H11 i.
  assert (y = P b). uf b; rww pr1_pair. wri H12 i.
  assert (y' = Q b). uf b; rww pr2_pair. wri H13 i. am.
Qed.

Lemma quotient_law_magma: forall (u:Set)(p:EEE)(r:Set),
 compatible_eq u p r -> magma u p 
 -> magma (quotient r) (quotient_law p r).
Proof. ir.  red in H. ee. rwi H1 H; rwi H1 H0. red. red. ir. uf quotient_law. 
  assert(inc (p (rep a) (rep b)) (substrate r)). app H0. 
  app inc_rep_substrate. app inc_rep_substrate.
  rw W_canon_proj. app inc_class_quotient. am.
Qed. 

Lemma quotient_law_pr: forall (u:Set)(p:EEE)(r:Set)(x y:Set),
  compatible_eq  u p r ->
  magma u p -> inc  x u-> inc y u ->
  V (p x y) (canon_proj r) = quotient_law p r (V x (canon_proj r))
  (V y (canon_proj r)). 
Proof. ir.  red in H. ee. assert (inc x (substrate r)). wrr H3.
  assert (inc y (substrate r)). wrr H3. 
  assert (inc (p x y) (substrate r)). wr H3; app H0.
  assert (related r x (rep (class r x))). app related_rep_class.
  assert (related r y (rep (class r y))). app related_rep_class.
  assert(inc (rep (class r y)) u). rw H3. app inc_rep_substrate. 
  app (inc_class_quotient H4 H6).
  assert(inc (rep (class r x)) u). rw H3. app inc_rep_substrate. 
  app (inc_class_quotient H4 H5).
  uf quotient_law. repeat rww canon_proj_pr. wr related_class_eq. app H. am.
  app reflexivity. wr H3. app H0.
Qed.

Lemma quotient_law_comm: forall (u:Set)(p:EEE)(r:Set),
  compatible_eq u p r ->  magma u p ->  
  pcommutativity u p -> pcommutativity (quotient r) (quotient_law p r).
Proof. ir. red. ir.  red.  uf quotient_law.
  app uneq2. red in H. ee. rwi H4 H1. app H1.  app inc_rep_substrate. 
  app inc_rep_substrate. 
Qed.

Lemma quotient_law_assoc: forall (u:Set)(p:EEE)(r:Set),
  compatible_eq u p r ->  a_magma u p ->  
  a_magma (quotient r) (quotient_law p r).
Proof. ir.  red.  ee. app (quotient_law_magma H). bs. red. ir. red in H. ee.
  uf quotient_law. set (a' := rep a);set (b' := rep b);set (c' := rep c).
  red in  H0. ee. rwi H4 H0. rwi H4 H.
  assert (inc a' (substrate r)). uf a'. app inc_rep_substrate. 
  assert (inc b' (substrate r)). uf b'. app inc_rep_substrate. 
  assert (inc c' (substrate r)). uf c'. app inc_rep_substrate. 
  assert(inc (p a' b') (substrate r)). app H0.
  assert(inc (p b' c') (substrate r)). app H0.
  assert (inc (rep (class r (p b' c'))) (substrate r)). app inc_rep_substrate. 
  app inc_class_quotient.
  assert (inc (rep (class r (p a' b'))) (substrate r)). app inc_rep_substrate. 
  app inc_class_quotient.
  assert (inc (p a' (rep (class r (p b' c')))) (substrate r)). app H0.
  assert (inc (p (rep (class r (p a' b'))) c') (substrate r)). app H0.
  repeat rww canon_proj_pr. 
  set (aa:=rep (class r (p a' b'))). assert (related r (p a' b') aa).
  uf aa.  app related_rep_class.
  assert (class r (p aa c') = class r (p (p a' b') c')).
  wr related_class_eq. uf aa. app H. app symmetricity. app reflexivity. am.
  app reflexivity. rw H17.
  set (bb:=rep (class r (p b' c'))). assert (related r (p b' c') bb).
  uf bb. app related_rep_class.
  assert (class r (p a' bb) = class r (p a' (p b' c'))). 
  wr related_class_eq. uf bb. app H. app reflexivity. app symmetricity. am.
  app reflexivity. rw H19. rwi H4 H6. rww H6. 
Qed.


Lemma can_proj_morphism: forall (u:Set)(p:EEE)(r:Set),
  compatible_eq u p r -> magma u p ->  
  l_morphism p (quotient_law p r) u (fun x=> (V x (canon_proj r))).
Proof. ir. red in H. ee. rwi H1 H0. rwi H1 H. rw H1. 
  red. ir.
  assert (inc (p a b) (substrate r)). app H0.
  assert (inc (rep (class r a)) (substrate r)). app inc_rep_substrate. 
  app inc_class_quotient.  
  assert (inc (rep (class r b)) (substrate r)). app inc_rep_substrate. 
  app inc_class_quotient.
  uf quotient_law. repeat rww canon_proj_pr. wrr related_class_eq.
  app H.  app related_rep_class.  app related_rep_class.
  app reflexivity. app H0.
Qed.

Lemma quotient_law_assoc2: forall (u:Set)(p:EEE)(r:Set),
  compatible_eq u p r ->  a_magma u p ->  
  a_magma (quotient r) (quotient_law p r).
Proof. ir.  red.  ee. app (quotient_law_magma H). bs. red. ir.
  red in H0. ee. cp (can_proj_morphism H H0).
  red in H. ee. rwi H6 H5.  rwi H6 H0. rwi H6 H4.
  assert (V (rep a)(canon_proj r) =a). app canon_proj_show_surjective.
  assert (V (rep b)(canon_proj r) =b). app canon_proj_show_surjective.
  assert (V (rep c)(canon_proj r) =c). app canon_proj_show_surjective.
  assert (inc (rep a) (substrate r)). app inc_rep_substrate.
  assert (inc (rep b) (substrate r)). app inc_rep_substrate.
  assert (inc (rep c) (substrate r)). app inc_rep_substrate.
  pose (H5 (rep a)(rep b) H11 H12).  simpl in e. rwi H8 e. rwi H9 e. wr e.
  assert (inc (p (rep a) (rep b)) (substrate r)). app H0.
  pose (H5 _ _ H14 H13). simpl in e0. rwi H10 e0. wr e0. clear e; clear e0.
  pose (H5 _ _ H12 H13).  simpl in e. rwi H9 e. rwi H10 e. wr e.
  assert (inc (p (rep b) (rep c)) (substrate r)). app H0.
  pose (H5 _ _ H11 H15). simpl in e0. rwi H8 e0. wr e0.
  rww H4.
Qed.

Lemma quotient_morphism: forall (u:Set)(p p':EEE)(r:Set)(f:EE),
  compatible_eq u p r ->  magma u p ->  
  l_morphism (quotient_law p r) p' (quotient r) f =
  l_morphism p p' u (fun x  => f(V x (canon_proj  r))).
Proof. ir. uf l_morphism. app iff_eq. ir. ufi quotient_law H1.
  red in H.  ee. rewrite H4 in *.
  set (a':=(V a (canon_proj r))). assert (inc a' (quotient r)). uf a'.
  rww canon_proj_pr. app inc_class_quotient. 
  set (b':=(V b (canon_proj r))). assert (inc b' (quotient r)). uf b'.
  rww canon_proj_pr. app inc_class_quotient. 
  wrr H1. app uneq.
  assert( inc (p a b) (substrate r)). app H0.
  assert (inc (rep a') (substrate r)). app inc_rep_substrate.
  assert (inc (rep b') (substrate r)). app inc_rep_substrate.
  assert (inc (p (rep a')(rep b')) (substrate r)). app H0.
  rww canon_proj_pr. rww canon_proj_pr. wrr related_class_eq. app H.
  uf a'.  rww canon_proj_pr. app related_rep_class.
  uf b'.  rww canon_proj_pr. app related_rep_class. app reflexivity.
  ir. red in H. ee. rewrite H4 in *.
  assert (inc (rep a) (substrate r)). app inc_rep_substrate.
  assert (inc (rep b) (substrate r)). app inc_rep_substrate.
  assert (inc (p (rep a)(rep b)) (substrate r)). app H0.
  uf quotient_law. rww canon_proj_pr. wrr canon_proj_pr. 
  rw (H1 _ _ H6 H7). rww canon_proj_pr.  rww canon_proj_pr. 
  rww class_rep. rww class_rep. 
Qed.

Lemma compatible_same_value_equivalence: forall (p p':EEE)(m:Set),
  ma_morphism p p' m -> magma (sourceU m) p->
  compatible_eq (U sourceU m) p (same_value_equivalence (sourceU m) (ev m)).
Proof. ir. red. ee. red. ir. 
  assert (inc (p x y) (U (source m))). app H0.
  assert (inc (p x' y') (U (source m))). app H0.
  wrr same_value_eq_pr. wri same_value_eq_pr H5; try am.  
  wri same_value_eq_pr H6; try am.
  transitivity (p' (ev m x) (ev m y)). app H. rww H5; rww H6. sy. app H.
  sy. app same_value_eq_substrate. app same_value_eq_equivalence.
Qed. 

Lemma same_val_eq_compatible_eq:forall (m:Set),
  compatible_with_equiv (ev m) (same_value_equivalence (sourceU m) (ev m)).
Proof. ir. red.  ir. ufi same_value_equivalence H. ufi related H. Ztac.
  rwi pr1_pair H1.  rwi pr2_pair H1. am.
Qed.

Lemma same_val_eq_morphism:forall (p p':EEE)(m:Set),
  ma_morphism p p' m -> magma (sourceU m) p->
  let r :=  (same_value_equivalence (sourceU m) (ev m)) in
    let f := (function_on_quotient r (ev m)) in 
      (l_morphism (quotient_law p r) p' (quotient r) (fun x => V x f)).
Proof. ir. 
  assert (compatible_eq (U (source m)) p r). uf r. 
  app (compatible_same_value_equivalence H H0). red in H1.
  assert(compatible_with_equiv (ev m) r). uf r. app same_val_eq_compatible_eq.
  ee.  red. ir. uf f.
  set (a':=rep a). assert (inc a' (substrate r)). uf a'. app inc_rep_substrate.
  assert (V a' (canon_proj r)=a). rww canon_proj_pr. uf a'. app class_rep. 
  set (b':=rep b). assert (inc b' (substrate r)). uf b'. app inc_rep_substrate.
  assert (V b' (canon_proj r)=b). rww canon_proj_pr. uf b'. app class_rep. 
  assert (inc a' (U (source m))). rww H3.
  assert (inc b' (U (source m))). rww H3.
  assert (inc (p a' b') (U (source m))). app H0.
  assert(inc (quotient_law p r a b) (quotient r)). uf quotient_law.
  uf canon_proj.  aw. app inc_class_quotient. wr H3. app H13. wr H3. app H13. 
  wr H8. wrr function_on_quotient_pr. rw H8.
  wr H10. wrr function_on_quotient_pr. rw H10. wrr H. 
  uf function_on_quotient. aw. uf fun_on_quotient. 
  assert (inc (rep (quotient_law p r a b)) (U (source m))). rw H3.
  app inc_rep_substrate. rw (same_value_eq_pr (ev m) H15 H13). fold r.
  assert(inc (p (rep a) (rep b)) (substrate r)).  wr H3. app H13.
  uf quotient_law. rw canon_proj_pr. app symmetricity. app related_rep_class.
  am.
Qed.

Lemma same_val_eq_isomorphism:forall (p p':EEE)(m:Set),
  ma_morphism p p' m -> magma (sourceU m) p-> mor_saxioms m->
  let r :=  (same_value_equivalence (sourceU m) (ev m)) in
    let f := (function_on_quotient r (ev m)) in 
      ((l_morphism (quotient_law p r) p' (quotient r) (fun x => V x f))
        & (Map.injective (quotient r) (targetU m) f)).
Proof. ir. ee. apply (same_val_eq_morphism H H0).
  assert (compatible_eq (U (source m)) p r). uf r. 
  app (compatible_same_value_equivalence H H0). red in H2.
  assert(compatible_with_equiv (ev m) r). uf r. app same_val_eq_compatible_eq.
  ee. red. ee.  red.  uf f. uf function_on_quotient. ee.  aw. aw. red. 
  ir.  rwi Function.range_inc_rw H6. nin H6. ee. 
  rwi Function.create_domain H6. rw H7. aw. uf fun_on_quotient.
  red in H1. red in H1. ee. app H1. rw H4. app inc_rep_substrate. aw.
  red.  ir. ufi f H8. ufi function_on_quotient H8. 
  rwi Function.create_V_rewrite  H8. rwi Function.create_V_rewrite  H8.
  ufi fun_on_quotient H8. wr (related_rep_rep H5 H6 H7). uf r.
  wrr same_value_eq_pr. rw H4. app inc_rep_substrate.  
  rw H4. app inc_rep_substrate. am. am.
Qed.

*)

End Bourbaki1.

Export Bourbaki1.

Module Bourbaki2.
 (* Page A I.12 section 2*)


Lemma monoid_zero_identity: forall (g:Set),
  monoid_axioms g -> identity_prop (Ul g) (dplus g)(zero g).
Proof. ir. red in H. red in H. ee. red. ee. am. ir. ee.  app H2. app H3.
Qed.

Lemma ring_one_identity: forall (g:Set),
  ring_axioms g -> identity_prop (Ul g) (dmult g)(one g).
Proof. ir. red in H. red in H. ee. red. ee. am. ir. ee.  app H3. app H4.
Qed.

Lemma ident_unique: forall (x:Set)(p:EEE)(e e':Set), 
   (identity_prop x p e &  identity_prop x p e') -> e=e'.
Proof. ir.  ee. red in H; red in H0. ee. pose (H2 _ H). wr e0.
  pose (H3 _ H0). am. 
Qed.

Lemma ident_central: forall (x:Set)(p:EEE)(e e':Set), 
  magma x p -> identity_prop x p e -> p_central x p e.
Proof. ir. rww inc_pcenter_rw. red in H0. ee. am. uf commutes. ir.
  pose (H1 _ H3). pose (H2 _ H3). transitivity y.  am. sy. am.
Qed.

  
End Bourbaki2.
Export Bourbaki2.