Skip to content

Instantly share code, notes, and snippets.

@ryuta-ito

ryuta-ito/symmetric_group.v

Last active September 23, 2018 07:32
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save ryuta-ito/8d7df194a2522de81da76547b19c1335 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save ryuta-ito/8d7df194a2522de81da76547b19c1335 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
symmetric_group.v
Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Definition subset {M : Type} (S T : set M) :=
forall s, belongs s S -> belongs s T.
Definition id {M : Type} (S : set M) (id : M) (bin : M -> M -> M) :=
forall s, belongs s S -> bin s id = s /\ bin id s = s.
Definition identity {M : Type} (S : set M) (bin : M -> M -> M) :=
exists e, id S e bin.
Definition inverse {M : Type} (S : set M) (s s' : M) (bin : M -> M -> M) :=
belongs s' S ->
id S (bin s s') bin /\ id S (bin s' s) bin.
Definition inversible {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall s, belongs s S -> exists s', inverse S s s' bin.
Definition associative {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall a b c,
belongs a S ->
belongs b S ->
belongs c S ->
bin a (bin b c) = bin (bin a b) c.
Definition entire_property {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall x y, belongs x S -> belongs y S -> belongs (bin x y) S.
Definition magma {M : Type} (S : set M) bin :=
entire_property S bin.
Definition semigroup {M : Type} (S : set M) bin :=
magma S bin /\ associative S bin.
Definition monoid {M : Type} (S : set M) bin :=
semigroup S bin /\ identity S bin.
Definition group {M : Type} (S : set M) bin :=
monoid S bin /\ inversible S bin.
Inductive S :=
| a : S
| b : S.
Definition f0 (s : S) :=
match s with
| a => a
| b => b
end.
Definition f1 (s : S) :=
match s with
| a => b
| b => a
end.
Definition comp (f' f: S -> S) :=
fun s => f' (f s).
Definition S_2 := (fun f => f = f0 \/ f = f1).
Axiom extensionality : forall {X Y:Type} (x:X) (f g:X->Y),
f x = g x -> f = g.
Theorem S_2_is_group : group S_2 comp.
Proof.
unfold group,monoid,semigroup.
split.
-
split.
+
split.
*
unfold magma,entire_property,belongs,S_2.
intros.
inversion H; clear H.
--
inversion H0; clear H0.
++
left.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
++
right.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
--
inversion H0; clear H0.
++
right.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
++
left.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
*
unfold associative,belongs,S_2.
intros.
inversion H; clear H.
--
inversion H0; clear H0.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H0; clear H0.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
+
unfold identity,id,belongs,S_2.
exists f0.
intros.
inversion H; clear H.
*
split.
--
rewrite H0.
apply (extensionality a).
reflexivity.
--
rewrite H0.
apply (extensionality a).
reflexivity.
*
split.
--
rewrite H0.
apply (extensionality a).
reflexivity.
--
rewrite H0.
apply (extensionality a).
reflexivity.
-
unfold inversible,inverse,id,belongs,S_2.
intros.
inversion H; clear H.
+
exists f0.
intros.
split; intros.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
+
exists f1.
intros.
split; intros.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment