Skip to content

Instantly share code, notes, and snippets.

@mathink mathink/ideal.v
Last active Dec 6, 2015

Embed
What would you like to do?
Module Ideal.
Open Scope ring_scope.
Class spec (R: Ring)(P: R -> Prop) :=
proof {
contain_subst: Proper ((==) ==> flip impl) P;
add_close:
forall x y,
P x -> P y -> P (x + y);
inv_close:
forall x,
P x -> P (x^-1);
z_close:
P 0;
mul_close:
forall x y,
P x -> P y -> P (x * y);
left_mul:
forall a x,
P x -> P (a * x);
right_mul:
forall a x,
P x -> P (x * a)
}.
Structure type (R: Ring) :=
make {
contain: R -> Prop;
prf: spec contain
}.
Module Ex.
Existing Instance prf.
Existing Instance contain_subst.
Notation isIdeal := spec.
Notation Ideal := type.
Coercion prf: Ideal >-> isIdeal.
Arguments isIdeal (R P): clear implicits.
End Ex.
End Ideal.
Export Ideal.Ex.
Instance Zn_is_ideal (n: Z): isIdeal Z_ring `(exists x, m = x * n).
Proof.
split.
- Show.
(* 1 focused subgoals (unfocused: 6) *)
(* , subgoal 1 (ID 704) *)
(* n : Z *)
(* ============================ *)
(* Proper ((==) ==> flip impl) (fun m : Z_ring => exists x : Z, m = x * n) *)
(* (dependent evars:) *)
intros x y Heq P; simpl.
now rewrite Heq; auto.
- Show.
(* 1 focused subgoals (unfocused: 5) *)
(* , subgoal 1 (ID 705) *)
(* n : Z *)
(* ============================ *)
(* forall x y : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> *)
(* (exists x0 : Z, y = x0 * n) -> exists x0 : Z, (x + y)%rng = x0 * n *)
(* (dependent evars:) *)
intros x y [p Hp] [q Hq]; subst.
exists (p + q).
now rewrite <- Z.mul_add_distr_r.
- Show.
(* 1 focused subgoals (unfocused: 4) *)
(* , subgoal 1 (ID 706) *)
(* n : Z *)
(* ============================ *)
(* forall x : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> exists x0 : Z, (x ^-1)%rng = x0 * n *)
(* (dependent evars:) *)
intros x [p Hp]; subst; simpl.
exists (-p).
now rewrite Zopp_mult_distr_l.
- Show.
(* 1 focused subgoals (unfocused: 3) *)
(* , subgoal 1 (ID 707) *)
(* n : Z *)
(* ============================ *)
(* exists x : Z, 0%rng = x * n *)
(* (dependent evars:) *)
now (exists 0).
- Show.
(* 1 focused subgoals (unfocused: 2) *)
(* , subgoal 1 (ID 708) *)
(* n : Z *)
(* ============================ *)
(* forall x y : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> *)
(* (exists x0 : Z, y = x0 * n) -> exists x0 : Z, (x * y)%rng = x0 * n *)
(* (dependent evars:) *)
intros x y [p Hp] [q Hq]; subst.
exists ((p * q) * n).
rewrite <- Z.mul_shuffle1.
now rewrite !Z.mul_assoc.
- Show.
(* 1 focused subgoals (unfocused: 1) *)
(* , subgoal 1 (ID 709) *)
(* n : Z *)
(* ============================ *)
(* forall a x : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> exists x0 : Z, (a * x)%rng = x0 * n *)
(* (dependent evars:) *)
intros a x [p Hp]; subst.
exists (a * p).
rewrite Z.mul_assoc.
rewrite Z.mul_shuffle0.
now rewrite Z.mul_comm.
- Show.
(* 1 focused subgoals (unfocused: 0) *)
(* , subgoal 1 (ID 710) *)
(* n : Z *)
(* ============================ *)
(* forall a x : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> exists x0 : Z, (x * a)%rng = x0 * n *)
(* (dependent evars:) *)
intros a x [p Hp]; subst.
exists (p * a).
now rewrite Z.mul_shuffle0.
Qed.
Definition Zn_ideal (n: Z) := Ideal.make (Zn_is_ideal n).
Goal Ideal.contain (Zn_ideal 2) 10.
Proof.
simpl.
(* 1 subgoals, subgoal 1 (ID 979) *)
(* ============================ *)
(* exists x : Z, 10 = x * 2 *)
(* (dependent evars:) *)
now exists 5.
Qed.
Goal forall n,
Ideal.contain (Zn_ideal 2) (n * 2).
Proof.
simpl; intros.
now exists n.
Qed.
Goal forall n,
~ Ideal.contain (Zn_ideal 2) (n * 2 + 1).
Proof.
intros n H; simpl in H.
assert (H': exists x, n * 2 + 1 = 2 * x).
{
destruct H as [m Hm]; exists m.
now rewrite (Z.mul_comm 2 m).
}
rewrite <- Zeven_ex_iff in H'.
revert H'.
apply Zodd_not_Zeven.
rewrite Zodd_ex_iff.
now exists n; rewrite Z.mul_comm.
Qed.
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.