ideal.v

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.