(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Order Theory with Classes.

   A bit of Group Theory.


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

*)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Set Implicit Arguments.
Unset Strict Implicit.

Require Export Order.Bounds.
Require Export Order.Operations.
Require Import Order.Relations.
Require Import List.

Coercion is_true b := b = true.

Require Import Coq.Bool.Bool.

Definition bool_leibniz : bool -> bool -> Prop := eq.

Definition bool_leiniz_equiv : Equivalence bool bool_leibniz := eq_equivalence.

Definition booleq : bool -> bool -> Prop := fun x y => eqb x y.

Program Instance eqb_equiv : Equivalence bool eqb.

  Next Obligation.
  Proof. destruct x ; simpl ; constructor. Qed.

  Next Obligation.
  Proof. destruct x ; destruct y ; simpl ; try constructor; auto. Qed.

  Next Obligation.
  Proof. destruct x ; destruct y ; destruct z ; simpl in * ; try constructor; auto. Qed.

Instance Morphism (eqb ==> iff) is_true.
Proof.
  reduce. destruct x ; destruct y ; simpl ; intuition. inversion H. inversion H.
Qed.

Fixpoint boolean_predicate l : Type :=
  match l with 
    | nil => bool
    | cons A args => A -> boolean_predicate args
  end.

Fixpoint reflect_relation l : forall (R : predicate l) (p : boolean_predicate l), Prop :=
  match l with
    | nil => fun R p => R <-> p
    | cons A args => fun R p =>
      forall x, reflect_relation (R x) (p x)
  end.

Open Local Scope signature_scope.

Infix "≡" := equiv (at level 70).

Class [ eqa : Equivalence A eqA ] => Group (law : A -> A -> A) :=
  grp_law_morphism :> Morphism (eqA ==> eqA ==> eqA) law ;
  grp_assoc : associative law ;
  grp_id : A ;
  grp_identity_neutral : neutral law grp_id ;
  grp_inv : A -> A ;
  grp_inverse_cancel : forall x, law (grp_inv x) x ≡ grp_id.

Definition law [ Group A eqA law ] := law.

Typeclasses unfold law grp_id grp_inv.

Notation "1" := grp_id : group_scope.
Notation " x ⁻¹ " := (grp_inv x) (at level 10) : group_scope.
Infix "∙" := law (left associativity, at level 40) : group_scope.

Definition monic [ Equivalence A ] (op : A -> A) (invop : A -> A) :=
  forall x y : A, op x ≡ invop y -> x ≡ y.

Definition cancel [ Equivalence A ] (op : A -> A) (invop : A -> A) :=
  forall x : A, op (invop x) ≡ x. 

Definition inverses [ Equivalence A ] (op : A -> A) (invop : A -> A) :=
  forall x : A, invop (op x) ≡ op (invop x).

Open Local Scope group_scope.

Definition invlaw [ Group A eqA mul ] := flip mul.

Infix "∙⁻¹" := invlaw (left associativity, at level 40) : group_scope.
    
Section GroupIdentities.

  Context [ G : Group A eqA mul ].

  Lemma mulgA : forall x₁ x₂ x₃ : A, x₁ ∙ (x₂ ∙ x₃) ≡ x₁ ∙ x₂ ∙ x₃.
  Proof.
    intros. rewrite (grp_assoc x₁). reflexivity.
  Qed.
  
  Lemma mul1g : forall x : A, 1 ∙ x ≡ x.
  Proof.
    intros. rewrite (grp_identity_neutral x). reflexivity.
  Qed.

  Lemma mulVg : forall x : A, x⁻¹ ∙ x ≡ 1.
  Proof.
    intros. rewrite (grp_inverse_cancel x). reflexivity.
  Qed.

  Lemma mulg_l : forall z x y : A, x ≡ y -> z ∙ x ≡ z ∙ y.
  Proof. order. Qed.

  Lemma mulg_r : forall z x y : A, x ≡ y -> x ∙ z ≡ y ∙ z.
  Proof. order. Qed.

  Lemma mulg_injl : forall x : A, injective (law x).
  Proof.
    red. intros.
    apply (mulg_l (x⁻¹)) in H.
    do 2 rewrite mulgA in H.
    rewrite (mulVg x) in H. do 2 rewrite mul1g in H.
    assumption.
  Qed.

  Lemma mulgV : forall x : A, x ∙ x⁻¹ ≡ 1.
  Proof.
    intros.
    rewrite <- (mul1g (x ∙ x⁻¹)).
    setoid_rewrite <- (mulVg (x ∙ x⁻¹)) at 1.
    rewrite <- mulgA.
    rewrite <- mulgA.
    rewrite (mulgA (x⁻¹) x (x⁻¹)).
    rewrite mulVg.
    rewrite mul1g.
    rewrite mulVg.
    reflexivity.
  Qed.

  Instance grp_inv_morphism : Morphism (eqA ==> eqA) grp_inv.
  Proof.
    simpl_relation. equivify.
    apply (@mulg_injl x). rewrite mulgV.
    rewrite H. rewrite mulgV. reflexivity.
  Qed.

  Lemma mulg1 : forall x : A, x ∙ 1 ≡ x.
  Proof.
    intros. rewrite <- (mulVg x). rewrite mulgA. rewrite mulgV. apply mul1g.
  Qed.

  Lemma mulg_invl : forall x : A, inverses (law x) (law (x⁻¹)).
  Proof.
    red. intros. 
    do 2 rewrite mulgA.
    rewrite (mulVg x), (mulgV x).
    reflexivity.
  Qed.

  Lemma invg1 : 1⁻¹ ≡ 1.
  Proof.
    setoid_rewrite <- (mulgV 1) at 2.
    rewrite mul1g. reflexivity.
  Qed.

  Lemma invgV : forall x : A, (x⁻¹)⁻¹ ≡ x.
  Proof.
    intros. apply (@mulg_injl (x⁻¹)).
    rewrite mulgV, mulVg. reflexivity.
  Qed.

  Lemma invg_inj : injective grp_inv.
  Proof.
    red. intros. rewrite <- (invgV x₁).
    rewrite H. apply invgV. 
  Qed.
  
  Lemma invg_mul : forall x₁ x₂ : A, (x₁ ∙ x₂)⁻¹ ≡ x₂⁻¹ ∙ x₁⁻¹.
  Proof. intros. 
    apply (@mulg_injl (x₁ ∙ x₂)).
    setoid_rewrite <- mulgA at 2.
    setoid_rewrite (mulgA x₂). rewrite 2!mulgV, mul1g, mulgV. 
    reflexivity.
  Qed.

  Theorem mulg_s₁ : forall a b : A, (b ∙ a ⁻¹) ∙ a ≡ b.
  Proof.
    intros. rewrite <- mulgA, mulVg, mulg1. reflexivity.
  Qed.

  Theorem mulg_s₂ : forall a b : A, (b ∙ a) ∙ a⁻¹ ≡ b.
  Proof.
    intros. rewrite <- mulgA, mulgV, mulg1. reflexivity.
  Qed.

  Lemma mulg_injr : forall x : A, injective (invlaw x).
  Proof.
    red. intros.
    unfold invlaw, flip in H.
    apply (mulg_r (x⁻¹)) in H.
    do 2 rewrite <- mulgA in H.
    rewrite (mulgV x) in H. do 2 rewrite mulg1 in H.
    assumption.
  Qed.

End GroupIdentities.

Existing Instance grp_inv_morphism.

Hint Rewrite @mulgA @mul1g @mulg1 @mulgV @mulVg : group.
Hint Rewrite @invg1 @invgV @invg_mul @mulg_s₁ @mulg_s₂ : group.

Definition conj [ Group A ] (x y : A) := x⁻¹ ∙ y ∙ x.

Notation " x ^ y " := (conj y x).

Section Conjugation.

  Context [ G : Group A ].

  Lemma conjgE : forall x y : A, x ^ y ≡ y⁻¹ ∙ x ∙ y.
  Proof. reflexivity. Qed.

  Lemma conjg1 : conj 1 ≡ id.
  Proof.
    reduce ; equivify. unfold conj, id. 
    rewrite invg1, mulg1, mul1g. reflexivity.
  Qed.

  Lemma conj1g : forall x : A, 1 ^ x ≡ 1.
  Proof. intro. unfold conj.    
    rewrite mulg1, mulVg. reflexivity.
  Qed.

  Ltac simpl_mul := 
    repeat rewrite invg_mul ;
    repeat rewrite <- mulgA ; repeat apply mulg_l ;
      try reflexivity.

  Lemma conjg_mul : forall x₁ x₂ y : A, (x₁ ∙ x₂) ^ y ≡ x₁ ^ y ∙ x₂ ^ y.
  Proof. intros. unfold conj.    
    simpl_mul.
    rewrite mulgA, mulgV, mul1g.  reflexivity.
  Qed.

  Lemma conjg_invg : forall x y : A, (x⁻¹) ^ y ≡ (x ^ y)⁻¹.
  Proof. intros. unfold conj.
    simpl_mul. symmetry. apply invgV. 
  Qed.

  Lemma conjg_conj : forall x y₁ y₂ : A, (x ^ y₁) ^ y₂ ≡ x ^ (y₁ ∙ y₂).
  Proof.
    intros. unfold conj. simpl_mul. 
  Qed.

  Lemma conjg_inj : forall y : A, injective (conj y).
  Proof.
    red. unfold conj. intros.
    repeat rewrite <- mulgA in H.
    apply mulg_injl in H. apply mulg_injr in H. assumption.
  Qed.

End Conjugation.

Require Import Coq.Program.Program.

Notation set A := (A -> bool).

Class [ grp : Group A eqA mul ] => SubGroup (s : set A) :=
  subgrp_morphism :> Morphism (eqA ==> eqb) s ;
  subgrp_id : s grp_id ;
  subgrp_inv : forall x : object s, s (grp_inv (`x)) ;
  subgrp_law : forall x y : object s, s (mul (`x) (`y)).

Definition bool_iff (x y : bool) : Prop :=
  x <-> y.

Lemma leibniz_bool_iff : RelationClasses.relation_equivalence bool_iff bool_leibniz.
Proof. 
  red. intros. unfold bool_iff, bool_leibniz in *. 
  split ; intros. destruct H.
  destruct x ; destruct x0 ; auto.
  elim H ; auto. constructor.
  elim H0 ; auto. constructor.
  subst. reflexivity.
Qed.

Instance leibniz_sub_bool_iff : RelationClasses.subrelation bool_iff bool_leibniz.
Proof. red. intros.
(*   rewrite leibniz_bool_iff in H.*)
Admitted.

Existing Instance bool_leiniz_equiv.

Section SubGroup.

  Context [ G : Group A eqA mul, s : ! SubGroup G H ].

  Lemma subgrp1 : H 1.
  Proof. apply subgrp_id. Qed.

  Lemma subgrpV : forall x : A, H x -> H (x⁻¹).
  Proof. intros. apply (subgrp_inv (exist _ x H0)). Qed.

  Lemma subgrpM : forall x y : A, H x -> H y -> H (x ∙ y).
  Proof. intros. apply (subgrp_law (exist _ x H0) (exist _ y H1)). Qed.

  Lemma subgrpMl : forall x y : A, H x -> H (x ∙ y) ≡ H y.
  Proof. intros.
    apply RelationClasses.is_subrelation. 
    split ; intros.
    apply subgrpV in H0.
    pose (subgrpM H0 H1) as H2.
    rewrite mulgA, (mulVg x), mul1g in H2.
    assumption.

    apply subgrpM ; auto.
  Qed.

  Lemma subgrpMr : forall x y : A, H y -> H (x ∙ y) ≡ H x.
  Proof. intros. 
    apply RelationClasses.is_subrelation.
    split ; intros. 

    apply subgrpV in H0.
    rewrite <- (mulg_s₂ y x). apply subgrpM ; auto.

    apply subgrpM ; auto.
  Qed.

  Lemma subgrpVl : forall x : A, H (x⁻¹) -> H x.
  Proof.
    intros. apply subgrpV in H0. rewrite invgV in H0. assumption.
  Qed.

End SubGroup.

(** Nothing to prove, full_subset x is True and the morphism is trivial. *) 

Program Instance [ G : Group A eqA mul ] => group_subgroup :
  SubGroup G (fun _ => true).

  Next Obligation.
  Proof. constructor. Qed.

Definition lcoset [ grp : Group A ] (H : set A) (x : A) : set A :=
  fun y => H (x⁻¹ ∙ y).

Definition rcoset [ grp : Group A ] (H : set A) (x : A) : set A :=
  fun y => H (y ∙ x⁻¹).

Section Cosets.

  Context [ G : Group A, S : ! SubGroup G H ].

  Instance rcoset_refl : Reflexive (rcoset H).
  Proof.
    red. intros. rewrite mulgV. apply subgrp1. 
  Qed.

  Instance rcoset_sym : Symmetric (rcoset H).
  Proof. red. intros.
    pose (subgrpV H0) as H'.
    autorewrite with group in H'. assumption.
  Qed.

  Instance rcoset_trans : Transitive (rcoset H).
  Proof. red. intros.
    pose (subgrpM H1 H0) as H'.
    autorewrite with group in H'.
    assumption.
  Qed.

  Program Instance rcoset_equivalence : Equivalence _ (rcoset H).

  Lemma rcoset_1 : rcoset H 1 ≡ H.
  Proof. 
    do 2 red ; intros. 
    apply RelationClasses.is_subrelation.
    red.
    unfold rcoset. 
    autorewrite with group. reflexivity.
  Qed.

End Cosets.

Existing Instance rcoset_equivalence.

Require Import SetoidList.

Class [ eqa : Equivalence A eqA ] => FiniteType :=
  enum : list A ;
  enum_nodup : NoDupA eqA enum ;
  enum_complete : forall x : A, InA eqA x enum.

Definition card [ F : FiniteType A ] (s : set A) : nat := length (filter s enum).

Class [ grp : Group A eqA (eqa:=eqa) mul ] => FiniteGroup := 
  finite_group_type :> FiniteType eqa.

Class [ fgrp : FiniteGroup A eqA (eqa:=eqa) (grp:=grp) ] => FiniteSubGroup (s : set A) :=
  finsubgrp_subgrp :> SubGroup grp s.

Definition finite_rcoset [ grp : FiniteGroup A eqA ] (H : set A) (x : A) : set A :=
  fun y => H (x⁻¹ ∙ y).

Section Lagrange.

  Context [ G : FiniteGroup A eqA mul ].
  Context [ S : ! FiniteSubGroup G H ].

  Lemma card_rcoset : forall x : A, card (rcoset H x) = card H.
  Proof.
    intros. unfold card. 
    induction enum.

      simpl. refl.

      simpl.
      unfold rcoset.
      cut (H (a ∙ x ⁻¹) = H a).
      intros H2 ; rewrite H2.
      destruct (H a). 
      simpl. rewrite <- IHl. reflexivity.
      assumption.

      refine (subgrpMr _ _).
      refine (subgrpV _).
      
  Admitted.
End Lagrange.