Instantly share code, notes, and snippets.

# mathink/group_advent_2014.v Created Dec 20, 2014

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 _).