Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Theorem Prover Advent Calendar day 20.
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
Structure Setoid :=
{
carrier:> Type;
equal: relation carrier;
prf_Setoid:> Equivalence equal
}.
Existing Instance prf_Setoid.
Notation Setoid_of eq := (@Build_Setoid _ eq _).
Notation "(== :> S )" := (equal (s:=S)).
Notation "(==)" := (== :> _).
Notation "x == y :> S" := (equal (s:=S) x y)
(at level 70, y at next level, no associativity).
Notation "x == y" := (x == y :> _) (at level 70, no associativity).
Structure Map (X Y: Setoid) :=
{
map_body:> X -> Y;
prf_Map:> Proper ((==) ==> (==)) map_body
}.
Existing Instance prf_Map.
Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" :=
(makeMap (fun x => .. (makeMap (fun y => p)) ..))
(at level 200, x binder, y binder, right associativity,
format "'[' [ x .. y :-> '/ ' p ] ']'").
Structure Binop (X: Setoid) :=
{
binop:> X -> X -> X;
prf_Binop:> Proper ((==) ==> (==) ==> (==)) binop
}.
Existing Instance prf_Binop.
Structure Magma :=
{
magma_setoid:> Setoid;
magma_binop: Binop magma_setoid
}.
Arguments magma_binop {m}.
Notation "x \dot y" := (magma_binop (m:=_) x y)
(at level 60, right associativity,
format "x \dot y").
Class Associative (m: Magma): Prop :=
associative:
forall (x y z: m), (x \dot y) \dot z == x \dot (y \dot z).
Class LIdentical (m: Magma)(e: m): Prop :=
left_identical: forall x: m, e \dot x == x.
Class RIdentical (m: Magma)(e: m): Prop :=
right_identical: forall x: m, x \dot e == x.
Class Identical (m: Magma)(e: m): Prop :=
{
identical_l:> LIdentical e;
identical_r:> RIdentical e
}.
Existing Instance identical_l.
Existing Instance identical_r.
Class LInvertible `{Identical m e}(inv: Map m m): Prop :=
left_invertible:
forall (x: m), (inv x) \dot x == e.
Class RInvertible `{Identical m e}(inv: Map m m): Prop :=
right_invertible:
forall (x: m), x \dot (inv x) == e.
Class Invertible `{Identical m e}(inv: Map m m): Prop :=
{
invertible_l:> LInvertible inv;
invertible_r:> RInvertible inv
}.
Class Divisible (m: Magma)(divL: Binop m)(divR: Binop m): Prop :=
{
divisible_l:
forall (a b: m), (divL a b) \dot a == b;
divisible_r:
forall (a b: m), a \dot (divR a b) == b
}.
Structure Quasigroup :=
{
qg_magma:> Magma;
qg_divL: Binop qg_magma;
qg_divR: Binop qg_magma;
prf_Quasigroup:> Divisible qg_divL qg_divR
}.
Existing Instance prf_Quasigroup.
Structure Loop :=
{
loop_qg:> Quasigroup;
loop_unit: loop_qg;
prf_Loop:> Identical loop_unit
}.
Existing Instance prf_Loop.
Structure Group_1 :=
{
group_loop:> Loop;
prf_Group_1:> Associative group_loop
}.
Existing Instance prf_Group_1.
Structure Semigroup :=
{
sg_magma:> Magma;
prf_Semigroup:> Associative sg_magma
}.
Existing Instance prf_Semigroup.
Structure Monoid :=
{
monoid_sg:> Semigroup;
monoid_unit: monoid_sg;
prf_Monoid:> Identical monoid_unit
}.
Existing Instance prf_Monoid.
Structure Group_2 :=
{
group_monoid:> Monoid;
group_inv: let m := group_monoid in Map m m;
prf_Group_2:> Invertible group_inv
}.
Existing Instance prf_Group_2.
Program Definition inv_Group_1 (g: Group_1): Map g g :=
[ x :-> qg_divL g x (loop_unit g) ].
Next Obligation.
intros x y Heq; simpl; rewrite Heq; reflexivity.
Qed.
Instance inv_Group_1_Invertible (g: Group_1)
: Invertible (inv_Group_1 g).
Proof.
split.
intros x; simpl.
apply divisible_l.
intros x; simpl.
Lemma qg_div_LR (g: Group_1):
forall x: g,
qg_divL g x (loop_unit g) == qg_divR g x (loop_unit g).
Proof.
intros x; simpl.
rewrite <- right_identical at 1.
rewrite <- (left_identical (qg_divR g x (loop_unit g))).
rewrite <- (divisible_r x (loop_unit g)) at 2.
rewrite <- (divisible_l x (loop_unit g)) at 3.
rewrite associative.
reflexivity.
Qed.
rewrite qg_div_LR; apply divisible_r.
Qed.
Definition sg_Group_1 (g: Group_1): Semigroup :=
{|
sg_magma := g
|}.
Definition monoid_Group_1 (g: Group_1): Monoid :=
{|
monoid_sg := sg_Group_1 g
|}.
Definition group_Group_1 (g: Group_1): Group_2 :=
{|
group_monoid := monoid_Group_1 g;
group_inv := inv_Group_1 g
|}.
Program Definition divL_Group_2 (g: Group_2): Binop g :=
{|
binop x y := y \dot group_inv g x
|}.
Next Obligation.
intros x x' Heqx y y' Heqy; simpl in *.
rewrite Heqx, Heqy; reflexivity.
Qed.
Program Definition divR_Group_2 (g: Group_2): Binop g :=
{|
binop x y := group_inv g x \dot y
|}.
Next Obligation.
intros x x' Heqx y y' Heqy; simpl in *.
rewrite Heqx, Heqy; reflexivity.
Qed.
Instance div_Group_2_Divisible (g: Group_2)
: Divisible (divL_Group_2 g) (divR_Group_2 g).
Proof.
split; intros x y; simpl.
now rewrite associative, left_invertible, right_identical.
now rewrite <- associative, right_invertible, left_identical.
Qed.
Definition qg_Group_2 (g: Group_2): Quasigroup :=
{|
qg_magma := g ;
qg_divL := divL_Group_2 g;
qg_divR := divR_Group_2 g
|}.
Definition loop_Group_2 (g: Group_2): Loop :=
{|
loop_qg := qg_Group_2 g;
loop_unit := monoid_unit g
|}.
Definition group_Group_2 (g: Group_2): Group_1 :=
{|
group_loop := loop_Group_2 g
|}.
Class isGroup (m: Magma)(e: m)(inv: Map m m) :=
{
group_identical:> Identical e;
group_invertible:> Invertible inv;
group_associative:> Associative m
}.
Structure Group :=
{
group_magma:> Magma;
group_unit: group_magma;
group_inverse: Map group_magma group_magma;
prf_Group:> isGroup group_unit group_inverse
}.
Notation make_Group m e inv := (@Build_Group m e inv _).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment