coq_practice_33.v

Require Import Arith.

Module Type Monoid.
  Parameter G : Type.
  Parameter mult : G -> G -> G.
  Parameter E : G.
  Axiom mult_assoc :
    forall x y z : G, mult x (mult y z) = mult (mult x y) z.
  Axiom identity_element1 :
    forall x : G, mult x E = mult E x.
  Axiom identity_element2 :
    forall x : G, mult E x = x.
End Monoid.

Print Monoid.

Module BoolList_Monoid <: Monoid.
  Definition G := list bool.
Print app.
Type app.
Type bool.
Type list.
Type list bool.
Type (nil : list bool).
Type app.
  Definition mult := fun p q : list bool => app  p q.
  Lemma mult_assoc : forall x y z : G, mult x (mult y z) = mult (mult x y) z.
  Proof.
    intro.
    induction x.
    intros.
    simpl.
    reflexivity.
    intros.
    simpl.
    assert (mult x (mult y z) = mult (mult x y) z).
    apply (IHx y z).
    rewrite H.
    reflexivity.
  Qed.
Locate "%".
  Definition E := nil : list bool.
  Lemma identity_element1 : forall x : G, mult x E = mult E x.
  Proof.
    unfold G.
    unfold mult.
    unfold E.
    intros.
    assert ((x ++ nil)%list = x).
      induction x.
      simpl.
      trivial.
      simpl.
      rewrite IHx.
      trivial.
    simpl.
    apply H.
  Qed.
  Lemma identity_element2 :forall x : G, mult E x = x.
  Proof.
    unfold G.
    unfold mult.
    unfold E.
    intros.
    induction x.
    simpl.
    trivial.
    simpl.
    trivial.
  Qed.
End BoolList_Monoid.
    
Module Monoid_with_Power(M:Monoid).
Print Monoid.
  Fixpoint pow (g : M.G) (p :  nat) : M.G := 
    match p with 
    | O => M.E
    | S q => M.mult (pow g q) g
    end.
  
  Lemma pow_comm_sub : forall g p,M.mult g (pow g p) = M.mult (pow g p) g.
  Proof.
    intros.
    induction p.
    simpl.
    apply M.identity_element1.
    simpl.
    
    rewrite M.mult_assoc.
    rewrite IHp.
    trivial.
  Qed.
    
  Lemma pow_e : forall p,pow M.E p = M.E.
  Proof.
    intros.
    induction p.
    simpl.
    trivial.
    simpl.
    rewrite IHp.
    apply M.identity_element2.
  Qed.
  Lemma pow_lemma1 : forall g p q,M.mult (pow g p) (pow g q) = pow g (p+q).
  Proof.
    intros.
    induction p.
      intros.
      simpl.
      apply M.identity_element2.

      simpl.
      rewrite <- pow_comm_sub.
      rewrite <- M.mult_assoc.
      rewrite <- pow_comm_sub.
      rewrite <- IHp.
      trivial.
  Qed.


  Lemma pow_comm : forall g p q,M.mult (pow g p) (pow g q) = M.mult (pow g q) (pow g p).
  Proof.
    intros.
    rewrite pow_lemma1.
    rewrite pow_lemma1.
    replace (p+q) with (q+p).
    trivial.
    ring.
  Qed.
      
  Lemma pow_lemma2 : forall g p q,pow (pow g p) q = pow g (p*q).
  Proof.
    intro.
    intro.
    induction p.
      intros.
      simpl.
      apply pow_e.
      
      intros.
      simpl.
      rewrite <- pow_lemma1.
      rewrite <- IHp.
      induction q.
        simpl.
        rewrite M.identity_element2.
        trivial.
        simpl.
        rewrite IHq.
        assert (forall r s,M.mult (M.mult (pow g q) r) s = M.mult (pow g q) (M.mult r s)).
          intros.
          rewrite M.mult_assoc.
          trivial.
        rewrite H.
        rewrite H.
        replace (M.mult (pow (pow g p) q) (M.mult (pow g p) g)) with (M.mult g (M.mult (pow (pow g p) q) (pow g p))).
        trivial.
        rewrite <- pow_comm_sub.
        rewrite M.mult_assoc.
        assert ((M.mult g (pow g p)) = (pow g (p+1))).
          rewrite <- pow_lemma1.
          simpl.
          rewrite M.identity_element2.
          apply pow_comm_sub.
        rewrite H0.
        rewrite <- pow_comm_sub.
        rewrite H0.
        rewrite IHp.
        apply pow_comm.
  Qed.
End Monoid_with_Power.


Module Monoid_bool_list_with_Power := Monoid_with_Power(BoolList_Monoid).