(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*                               Oct 1st 1996                               *)
(*                                                                          *)
(****************************************************************************)
(*                              Inverses_Group.v                            *)
(****************************************************************************)

Require Export Group.

Set Implicit Arguments.
Unset Strict Implicit.
    
(* The Monoid of inverse pairs on a Monoid *)

Section inv_def.

Variable A : Monoid.

(* The set Inverses_set of inverse pairs on A *)

Structure Inverses : Type := 
  {Inv_elt_l : A;
   Inv_elt_r : A;
   Prf_invs1 : Inverses_rel Inv_elt_l Inv_elt_r;
   Prf_invs2 : Inverses_rel Inv_elt_r Inv_elt_l}.

Definition Inverses_eq (x y : Inverses) := Inv_elt_l x =_S Inv_elt_l y.

Lemma Inverses_equiv : Equivalence Inverses_eq.
Proof.
(* Goal: @Equivalence Inverses Inverses_eq *)
apply Build_Equivalence.
(* Goal: @Reflexive Inverses Inverses_eq *)
(* Goal: @Partial_equivalence Inverses Inverses_eq *)
unfold Reflexive in |- *.
(* Goal: forall x : Inverses, Inverses_eq x x *)
(* Goal: @Partial_equivalence Inverses Inverses_eq *)
intro x; unfold Inverses_eq in |- *. 
(* Goal: @Equal (Mcarrier A) (Inv_elt_l x) (Inv_elt_l x) *)
(* Goal: @Partial_equivalence Inverses Inverses_eq *)
apply Refl.
(* Goal: @Partial_equivalence Inverses Inverses_eq *)
apply Build_Partial_equivalence.
(* Goal: @Transitive Inverses Inverses_eq *)
(* Goal: @Symmetric Inverses Inverses_eq *)
unfold Transitive in |- *.
(* Goal: forall (x y z : Inverses) (_ : Inverses_eq x y) (_ : Inverses_eq y z), Inverses_eq x z *)
(* Goal: @Symmetric Inverses Inverses_eq *)
intros x y z H1 H2; unfold Inverses_eq in |- *. 
(* Goal: @Equal (Mcarrier A) (Inv_elt_l x) (Inv_elt_l z) *)
(* Goal: @Symmetric Inverses Inverses_eq *)
apply Trans with (Inv_elt_l y); assumption.
(* Goal: @Symmetric Inverses Inverses_eq *)
unfold Symmetric in |- *.
(* Goal: forall (x y : Inverses) (_ : Inverses_eq x y), Inverses_eq y x *)
intros x y H; unfold Inverses_eq in |- *. 
(* Goal: @Equal (Mcarrier A) (Inv_elt_l y) (Inv_elt_l x) *)
apply Sym; assumption.
Qed.

Canonical Structure Inverses_setoid : Setoid := Inverses_equiv.

(* General group theory equational reasoning *)

Lemma Eq_abb'a' :
 forall a b a' b' : A,
 Inverses_rel a a' -> Inverses_rel b b' -> Inverses_rel (a +_M b) (b' +_M a').
Proof.
(* Goal: forall (a b a' b' : Carrier (Mcarrier A)) (_ : @Inverses_rel A a a') (_ : @Inverses_rel A b b'), @Inverses_rel A (@ApMop A a b) (@ApMop A b' a') *)
intros a b a' b' i j.
(* Goal: @Monoid_idr Inverses_setoid Inverses_op Inverses_unit *)
red in |- *.
(* (a.b).b'.a' = e *)
(* Goal: @Equal (Mcarrier A) (@ApMop A (@ApMop A a b) (@ApMop A b' a')) (Munit A) *)
(* *) apply Trans with (a +_M (b +_M (b' +_M a'))).
(* Goal: @Equal (Mcarrier A) (@ApMop A (@ApMop A a b) (@ApMop A b' a')) (@ApMop A a (@ApMop A b (@ApMop A b' a'))) *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a (@ApMop A b (@ApMop A b' a'))) (Munit A) *)
apply Mass1.
(* a.b.b'.a' = e *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a (@ApMop A b (@ApMop A b' a'))) (Munit A) *)
(* *) apply Trans with (a +_M a'). 
(* a.b.b'.a' = a.a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a (@ApMop A b (@ApMop A b' a'))) (@ApMop A a a') *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
apply (Map2_l (Mop A) (b1:=b +_M (b' +_M a')) (b2:=a') a).
(* b.b'.a' = a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A b (@ApMop A b' a')) a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
(* *) apply Trans with (b +_M b' +_M a').
(* Goal: @Equal (Mcarrier A) (@ApMop A b (@ApMop A b' a')) (@ApMop A (@ApMop A b b') a') *)
(* Goal: @Equal (Mcarrier A) (@ApMop A (@ApMop A b b') a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
apply Mass.
(* (b.b').a' = a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A (@ApMop A b b') a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
(* *) apply Trans with (Munit A +_M a'). 
(* Goal: @Equal (Mcarrier A) (@ApMop A (@ApMop A b b') a') (@ApMop A (Munit A) a') *)
(* Goal: @Equal (Mcarrier A) (@ApMop A (Munit A) a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
apply (Map2_r (Mop A) (a1:=b +_M b') (a2:=Munit A) a').
(* Goal: @Equal (Mcarrier A) (@ApMop A b b') (Munit A) *)
(* Goal: @Equal (Mcarrier A) (@ApMop A (Munit A) a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
apply j.
(* e.a' = a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A (Munit A) a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
apply Midl.
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
apply i.
Qed.

(* Composition operation on Inverses_setoid *)

 Section inverses_comp_def.

 Variable x y : Inverses_setoid.

 Definition Inv_comp_elt_l := Inv_elt_l x +_M Inv_elt_l y.

 Definition Inv_comp_elt_r := Inv_elt_r y +_M Inv_elt_r x.

 Lemma Inv_comp_invs1 : Inverses_rel Inv_comp_elt_l Inv_comp_elt_r.
 Proof.
(* Goal: @Inverses_rel A Inv_comp_elt_l Inv_comp_elt_r *)
 exact (Eq_abb'a' (Prf_invs1 x) (Prf_invs1 y)).
 Qed.

 Lemma Inv_comp_invs2 : Inverses_rel Inv_comp_elt_r Inv_comp_elt_l.
 Proof.
(* Goal: @Inverses_rel A Inv_comp_elt_r Inv_comp_elt_l *)
 exact (Eq_abb'a' (Prf_invs2 y) (Prf_invs2 x)).
 Qed.

 Canonical Structure Inverses_comp : Inverses_setoid :=
   Build_Inverses Inv_comp_invs1 Inv_comp_invs2.

 End inverses_comp_def.

Lemma Inverses_congl : Map2_congl_law Inverses_comp.
Proof.
(* Goal: @Map2_congl_law Inverses_setoid Inverses_setoid Inverses_setoid Inverses_comp *)
unfold Map2_congl_law in |- *.
(* Goal: forall (b1 b2 a : Carrier Inverses_setoid) (_ : @Equal Inverses_setoid b1 b2), @Equal Inverses_setoid (Inverses_comp a b1) (Inverses_comp a b2) *)
intros x y z.
(* Goal: forall _ : @Equal Inverses_setoid x y, @Equal Inverses_setoid (Inverses_comp z x) (Inverses_comp z y) *)
elim x; elim y; elim z; simpl in |- *.
(* Goal: forall (Inv_elt_l Inv_elt_r : Carrier (Mcarrier A)) (Prf_invs1 : @Inverses_rel A Inv_elt_l Inv_elt_r) (Prf_invs2 : @Inverses_rel A Inv_elt_r Inv_elt_l) (Inv_elt_l0 Inv_elt_r0 : Carrier (Mcarrier A)) (Prf_invs3 : @Inverses_rel A Inv_elt_l0 Inv_elt_r0) (Prf_invs4 : @Inverses_rel A Inv_elt_r0 Inv_elt_l0) (Inv_elt_l1 Inv_elt_r1 : Carrier (Mcarrier A)) (Prf_invs5 : @Inverses_rel A Inv_elt_l1 Inv_elt_r1) (Prf_invs6 : @Inverses_rel A Inv_elt_r1 Inv_elt_l1) (_ : Inverses_eq (@Build_Inverses Inv_elt_l1 Inv_elt_r1 Prf_invs5 Prf_invs6) (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4)), Inverses_eq (Inverses_comp (@Build_Inverses Inv_elt_l Inv_elt_r Prf_invs1 Prf_invs2) (@Build_Inverses Inv_elt_l1 Inv_elt_r1 Prf_invs5 Prf_invs6)) (Inverses_comp (@Build_Inverses Inv_elt_l Inv_elt_r Prf_invs1 Prf_invs2) (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4)) *)
intros a a' p p' a0 a0' p0 p0' a1 a1' p1 p1' H.
(* Goal: Inverses_eq (Inverses_comp (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses b1 b1' p1 p1')) (Inverses_comp (@Build_Inverses b0 b0' p0 p0') (@Build_Inverses b1 b1' p1 p1')) *)
unfold Inv_comp_elt_l, Inv_comp_elt_r in |- *; simpl in |- *.
(* Goal: Inverses_eq (Inverses_comp (@Build_Inverses a a' p p') (@Build_Inverses a1 a1' p1 p1')) (Inverses_comp (@Build_Inverses a a' p p') (@Build_Inverses a0 a0' p0 p0')) *)
apply (Prf_map2_congl (Mop A) (b1:=a1) (b2:=a0) a); trivial.
Qed.

Lemma Inverses_congr : Map2_congr_law Inverses_comp.
Proof.
unfold Map2_congr_law in |- *; simple induction a1; simple induction a2;
 simpl in |- *.
(* Goal: forall (Inv_elt_l Inv_elt_r : Carrier (Mcarrier A)) (Prf_invs1 : @Inverses_rel A Inv_elt_l Inv_elt_r) (Prf_invs2 : @Inverses_rel A Inv_elt_r Inv_elt_l) (b : Inverses) (_ : Inverses_eq (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses Inv_elt_l Inv_elt_r Prf_invs1 Prf_invs2)), Inverses_eq (Inverses_comp (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) b) (Inverses_comp (@Build_Inverses Inv_elt_l Inv_elt_r Prf_invs1 Prf_invs2) b) *)
intros b0 b0' p0 p0' z; elim z.
(* Goal: forall (Inv_elt_l Inv_elt_r : Carrier (Mcarrier A)) (Prf_invs1 : @Inverses_rel A Inv_elt_l Inv_elt_r) (Prf_invs2 : @Inverses_rel A Inv_elt_r Inv_elt_l) (_ : Inverses_eq (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses b0 b0' p0 p0')), Inverses_eq (Inverses_comp (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses Inv_elt_l Inv_elt_r Prf_invs1 Prf_invs2)) (Inverses_comp (@Build_Inverses b0 b0' p0 p0') (@Build_Inverses Inv_elt_l Inv_elt_r Prf_invs1 Prf_invs2)) *)
intros b1 b1' p1 p1' H.
(* Goal: Inverses_eq (Inverses_comp (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses b1 b1' p1 p1')) (Inverses_comp (@Build_Inverses b0 b0' p0 p0') (@Build_Inverses b1 b1' p1 p1')) *)
unfold Inv_comp_elt_l, Inv_comp_elt_r in |- *; simpl in |- *.
(* Goal: Inverses_eq (Inverses_comp (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses b1 b1' p1 p1')) (Inverses_comp (@Build_Inverses b0 b0' p0 p0') (@Build_Inverses b1 b1' p1 p1')) *)
apply (Prf_map2_congr (Mop A) (a1:=Inv_elt_l0) (a2:=b0) b1); trivial.
Qed.

Definition Inverses_op := Build_Map2 Inverses_congl Inverses_congr.

(* The Monoid of inverse pairs *)

Lemma Mass_Inverses : Monoid_ass Inverses_op.
Proof.
(* Goal: @Monoid_idr Inverses_setoid Inverses_op Inverses_unit *)
red in |- *.
simple induction x; simple induction y; simple induction z; simpl in |- *;
 intros.
(* Goal: Inverses_eq (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Build_Inverses Inv_elt_l1 Inv_elt_r1 Prf_invs5 Prf_invs6) (@Build_Inverses Inv_elt_l2 Inv_elt_r2 Prf_invs7 Prf_invs8))) (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses Inv_elt_l1 Inv_elt_r1 Prf_invs5 Prf_invs6)) (@Build_Inverses Inv_elt_l2 Inv_elt_r2 Prf_invs7 Prf_invs8)) *)
unfold Inverses_comp, Inv_comp_elt_l, Inv_comp_elt_r in |- *; simpl in |- *.
(* Goal: Inverses_eq (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Build_Inverses Inv_elt_l1 Inv_elt_r1 Prf_invs5 Prf_invs6) (@Build_Inverses Inv_elt_l2 Inv_elt_r2 Prf_invs7 Prf_invs8))) (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Build_Inverses Inv_elt_l1 Inv_elt_r1 Prf_invs5 Prf_invs6)) (@Build_Inverses Inv_elt_l2 Inv_elt_r2 Prf_invs7 Prf_invs8)) *)
apply (Prf_monoid_ass Inv_elt_l0 Inv_elt_l1 Inv_elt_l2).
Qed.

Lemma Inverses_unit_invs : Inverses_rel (Munit A) (Munit A).
Proof.
(* Goal: @Inverses_rel A (Munit A) (Munit A) *)
apply (Prf_monoid_idl (Munit A)).
Qed.

Canonical Structure Inverses_unit :=
  Build_Inverses Inverses_unit_invs Inverses_unit_invs.

Lemma Midl_Inverses : Monoid_idl Inverses_op Inverses_unit.
Proof.
(* Goal: @Monoid_idr Inverses_setoid Inverses_op Inverses_unit *)
red in |- *.
(* Goal: forall x : Carrier Inverses_setoid, @Equal Inverses_setoid x (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op x Inverses_unit) *)
simple induction x; simpl in |- *; intros.
(* Goal: Inverses_eq (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op Inverses_unit (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4)) (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) *)
unfold Inverses_eq, Inv_comp_elt_l in |- *; simpl in |- *.
(* Goal: @Equal (Mcarrier A) (Inv_comp_elt_l Inverses_unit (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4)) Inv_elt_l0 *)
apply (Prf_monoid_idl Inv_elt_l0).
Qed.

Lemma Midr_Inverses : Monoid_idr Inverses_op Inverses_unit.
Proof.
(* Goal: @Monoid_idr Inverses_setoid Inverses_op Inverses_unit *)
red in |- *.
(* Goal: forall x : Carrier Inverses_setoid, @Equal Inverses_setoid x (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op x Inverses_unit) *)
simple induction x; simpl in |- *; intros.
(* Goal: Inverses_eq (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) (@Ap2 Inverses_setoid Inverses_setoid Inverses_setoid Inverses_op (@Build_Inverses Inv_elt_l0 Inv_elt_r0 Prf_invs3 Prf_invs4) Inverses_unit) *)
apply (Prf_monoid_idr Inv_elt_l0).
Qed.

Canonical Structure Inverses_Monoid :=
  Build_Monoid Mass_Inverses Midl_Inverses Midr_Inverses.

(* opposite operation *)

Definition Opposite (x : Inverses_setoid) : Inverses_setoid :=
  Build_Inverses (Prf_invs2 x) (Prf_invs1 x).

Lemma Opposite_map_law : Map_law Opposite.
Proof.
red in |- *; intros x y.
elim x; elim y; simpl in |- *; unfold Inverses_eq in |- *; simpl in |- *.
intros a a' aa' a'a b b' bb' b'b ba.
(* *) apply Trans with (b' +_M Munit A).
apply Midr.
(* *) apply Trans with (b' +_M (a +_M a')).
unfold ApMop in |- *; apply Map2_l.
apply Sym; trivial.
(* *) apply Trans with (y := b' +_M a +_M a').
(* Goal: @Equal (Mcarrier A) (@ApMop A b (@ApMop A b' a')) (@ApMop A (@ApMop A b b') a') *)
(* Goal: @Equal (Mcarrier A) (@ApMop A (@ApMop A b b') a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
apply Mass.
(* Goal: @Equal (Mcarrier A) (@ApMop A (@ApMop A b b') a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
(* *) apply Trans with (Munit A +_M a').
(* Goal: @Equal (Mcarrier A) (@ApMop A (Munit A) a') a' *)
(* Goal: @Equal (Mcarrier A) (@ApMop A a a') (Munit A) *)
2: apply Midl.
unfold ApMop in |- *; apply Map2_r.
(* *) apply Trans with (b' +_M b).
2: assumption.
unfold ApMop in |- *; apply Map2_l.
apply Sym; trivial.
Qed.

Canonical Structure Opposite_map := Build_Map Opposite_map_law.

Lemma Inverses_invl : Group_invl Opposite_map.
Proof.
(* Goal: @Group_invr Inverses_Monoid Opposite_map *)
red in |- *; simple induction x; trivial.
Qed.

Lemma Inverses_invr : Group_invr Opposite_map.
Proof.
(* Goal: @Group_invr Inverses_Monoid Opposite_map *)
red in |- *; simple induction x; trivial.
Qed.

Canonical Structure Inverses_group := Build_Group Inverses_invl Inverses_invr.

End inv_def.
