Skip to content

Instantly share code, notes, and snippets.

@mathink mathink/ring.v
Created Dec 4, 2015

Embed
What would you like to do?
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" := (equal x y) (at level 70, no associativity).
Notation "x == y :> S" := (equal (s:=S) x y)
(at level 70, y at next level, no associativity).
Class isMap (X Y: Setoid)(f: X -> Y) :=
map_subst:> Proper ((==) ==> (==)) f.
Structure Map (X Y: Setoid) :=
{
map_body:> X -> Y;
prf_Map:> isMap 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 ] ']'").
Class isBinop (X: Setoid)(op: X -> X -> X) :=
binop_subst:> Proper ((==) ==> (==) ==> (==)) op.
Structure Binop (X: Setoid) :=
{
binop:> X -> X -> X;
prf_Binop:> isBinop binop
}.
Existing Instance prf_Binop.
Class Associative `(op: Binop X): Prop :=
associative:>
forall (x y z: X), op x (op y z) == op (op x y) z.
Class LIdentical `(op: Binop X)(e: X): Prop :=
left_identical:> forall x: X, op e x == x.
Class RIdentical `(op: Binop X)(e: X): Prop :=
right_identical:> forall x: X, op x e == x.
Class Identical `(op: Binop X)(e: X): Prop :=
{
identical_l:> LIdentical op e;
identical_r:> RIdentical op e
}.
Existing Instance identical_l.
Existing Instance identical_r.
Coercion identical_l: Identical >-> LIdentical.
Coercion identical_r: Identical >-> RIdentical.
Module Monoid.
Class spec (M: Setoid)(op: Binop M)(e: M) :=
proof {
associative:> Associative op;
identical:> Identical op e
}.
Structure type :=
make {
carrier: Setoid;
op: Binop carrier;
e: carrier;
prf: spec op e
}.
Module Ex.
Existing Instance associative.
Existing Instance identical.
Existing Instance prf.
Notation isMonoid := spec.
Notation Monoid := type.
Coercion associative: isMonoid >-> Associative.
Coercion identical: isMonoid >-> Identical.
Coercion carrier: Monoid >-> Setoid.
Coercion prf: Monoid >-> isMonoid.
Delimit Scope monoid_scope with monoid.
Notation "x * y" := (op _ x y) (at level 40, left associativity): monoid_scope.
Notation "'1'" := (e _): monoid_scope.
End Ex.
End Monoid.
Export Monoid.Ex.
Class LInvertible `{Identical X op e}(inv: Map X X): Prop :=
left_invertible:>
forall (x: X), op (inv x) x == e.
Class RInvertible `{Identical X op e}(inv: Map X X): Prop :=
right_invertible:>
forall (x: X), op x (inv x) == e.
Class Invertible `{Identical X op e}(inv: Map X X): Prop :=
{
invertible_l:> LInvertible inv;
invertible_r:> RInvertible inv
}.
Coercion invertible_l: Invertible >-> LInvertible.
Coercion invertible_r: Invertible >-> RInvertible.
Module Group.
Class spec (G: Setoid)(op: Binop G)(e: G)(inv: Map G G) :=
proof {
is_monoid:> isMonoid op e;
invertible: Invertible inv
}.
Structure type :=
make {
carrier: Setoid;
op: Binop carrier;
e: carrier;
inv: Map carrier carrier;
prf: spec op e inv
}.
Module Ex.
Existing Instance is_monoid.
Existing Instance invertible.
Existing Instance prf.
Notation isGroup := spec.
Notation Group := type.
Coercion is_monoid: isGroup >-> isMonoid.
Coercion invertible: isGroup >-> Invertible.
Coercion carrier: Group >-> Setoid.
Coercion prf: Group >-> isGroup.
Delimit Scope group_scope with group.
Notation "x * y" := (op _ x y) (at level 40, left associativity): group_scope.
Notation "'1'" := (e _): group_scope.
Notation "x ^-1" := (inv _ x) (at level 20, left associativity): group_scope.
End Ex.
End Group.
Export Group.Ex.
Class Commute `(op: Binop X): Prop :=
commute:>
forall a b, op a b == op b a.
Class Distributive (X: Setoid)(add mul: Binop X) :=
{
distributive_l:>
forall a b c, mul a (add b c) = add (mul a b) (mul a c);
distributive_r:>
forall a b c, mul (add a b) c = add (mul a c) (mul b c)
}.
Module Ring.
Class spec (R: Setoid)(add: Binop R)(z: R)(inv: Map R R)(mul: Binop R)(e: R) :=
proof {
add_group: isGroup add z inv;
add_commute: Commute add;
mul_monoid: isMonoid mul e;
distributive: Distributive add mul
}.
Structure type :=
make {
carrier: Setoid;
add: Binop carrier;
z: carrier;
inv: Map carrier carrier;
mul: Binop carrier;
e: carrier;
prf: spec add z inv mul e
}.
Module Ex.
Existing Instance add_group.
Existing Instance add_commute.
Existing Instance mul_monoid.
Existing Instance distributive.
Existing Instance prf.
Notation isRing := spec.
Notation Ring := type.
Coercion add_group: isRing >-> isGroup.
Coercion add_commute: isRing >-> Commute.
Coercion mul_monoid: isRing >-> isMonoid.
Coercion distributive: isRing >-> Distributive.
Coercion carrier: Ring >-> Setoid.
Coercion prf: Ring >-> isRing.
Delimit Scope ring_scope with rng.
Notation "x + y" := (add _ x y): ring_scope.
Notation "x * y" := (mul _ x y): ring_scope.
Notation "'0'" := (z _): ring_scope.
Notation "x ^-1" := (inv _ x) (at level 20, left associativity): ring_scope.
Notation "'1'" := (e _): ring_scope.
End Ex.
Import Ex.
Definition add_id_l {R: Ring}(x: R) := (@left_identical R (add R) (z R) (add_group (spec:=R)) x).
Definition add_id_r {R: Ring}(x: R) := (@right_identical R (add R) (z R) (add_group (spec:=R)) x).
Definition add_inv_l {R: Ring}(x: R) := (@left_invertible R (add R) (z R) (add_group (spec:=R)) (inv R) (add_group (spec:=R)) x).
Definition add_inv_r {R: Ring}(x: R) := (@right_invertible R (add R) (z R) (add_group (spec:=R)) (inv R) (add_group (spec:=R)) x).
Definition mul_id_l {R: Ring}(x: R) := (@left_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).
Definition mul_id_r {R: Ring}(x: R) := (@right_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).
End Ring.
Export Ring.Ex.
Require Import ZArith.
Open Scope Z_scope.
Print Z.
(* Inductive Z : Set := Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z *)
(* For Zpos: Argument scope is [positive_scope] *)
(* For Zneg: Argument scope is [positive_scope] *)
Canonical Structure positive_setoid := Setoid_of (@eq positive).
Canonical Structure Z_setoid := Setoid_of (@eq Z).
Instance Zneg_Proper : Proper ((==:>positive_setoid) ==> ((==:>Z_setoid))) Zneg.
Proof.
now intros p q Heq; simpl in *; subst.
Qed.
Instance Zpos_Proper : Proper ((==:>positive_setoid) ==> ((==:>Z_setoid))) Zpos.
Proof.
now intros p q Heq; simpl in *; subst.
Qed.
(* Group of '+' *)
Program Instance Zplus_is_binop: isBinop (X:=Z_setoid) Zplus.
Canonical Structure Zplus_binop := Build_Binop Zplus_is_binop.
Program Instance Zplus_is_monoid: isMonoid Zplus_binop 0.
Next Obligation.
intros x y z; simpl.
apply Zplus_assoc.
Qed.
Next Obligation.
repeat split.
intros x; simpl.
apply Zplus_0_r.
Qed.
Canonical Structure Zplus_monoid := Monoid.make Zplus_is_monoid.
Program Instance Zinv_is_map: isMap (X:=Z_setoid) Zopp.
Canonical Structure Zinv_map: Map Z_setoid Z_setoid := Build_Map Zinv_is_map.
Program Instance Zplus_is_group: isGroup Zplus_binop 0 Zinv_map.
Next Obligation.
repeat split.
- intros x; simpl.
apply Z.add_opp_diag_l.
- intros x; simpl.
apply Z.add_opp_diag_r.
Qed.
Canonical Structure Zgroup_monoid := Group.make Zplus_is_group.
Program Instance Zplus_commute: Commute Zplus_binop.
Next Obligation.
apply Zplus_comm.
Qed.
(* Monoid of '*' *)
Instance Zmult_is_binop: isBinop (X:=Z_setoid) Zmult.
Proof.
intros x y Heq z w Heq'; simpl in *; subst; auto.
Qed.
Canonical Structure Zmult_binop := Build_Binop Zmult_is_binop.
Program Instance Zmult_is_monoid: isMonoid Zmult_binop 1.
Next Obligation.
intros x y z; simpl.
apply Zmult_assoc.
Qed.
Next Obligation.
repeat split.
- intros x; simpl.
destruct x; auto.
- intros x; simpl.
apply Zmult_1_r.
Qed.
Canonical Structure Zmult_monoid := Monoid.make Zmult_is_monoid.
(* Ring of '+' & '*' *)
Program Instance Z_is_ring: isRing Zplus_binop 0 Zinv_map Zmult_binop 1.
Next Obligation.
split; simpl; intros.
- apply Z.mul_add_distr_l.
- apply Z.mul_add_distr_r.
Qed.
Canonical Structure Z_ring := Ring.make Z_is_ring.
Compute (1 * 2 + 3).
(* = 5 *)
(* : Z *)
Open Scope ring_scope.
Compute (1 * 2 + 3).
(* = 5 *)
(* : Z_ring *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.