Skip to content

Instantly share code, notes, and snippets.

@satos---jp
Created June 1, 2014 08:15
Show Gist options
  • Save satos---jp/4111ba1cac980d969339 to your computer and use it in GitHub Desktop.
Save satos---jp/4111ba1cac980d969339 to your computer and use it in GitHub Desktop.
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment