Require Import Stdlib.Arith.Arith.
Import List.ListNotations.
Require Import Utf8 Core Misc Utils IterAdd.


Record ideal {T} {ro : ring_like_op T} := mk_ip
  { i_subset : T → Prop;
    i_zero : i_subset 0%L;
    i_add x y : i_subset x → i_subset y → i_subset (x + y)%L;
    i_mul_l t x : i_subset x → i_subset (t × x)%L;
    i_mul_r x t : i_subset x → i_subset (x × t)%L }.

Declare Scope ideal_scope.
Delimit Scope ideal_scope with I.
Bind Scope ideal_scope with ideal.

Arguments ideal T {ro}.
Arguments i_subset {T ro} i%_I a%_L.

Notation "x '∈' I" := (i_subset I x) (at level 70) : ideal_scope.

Class ideal_ctx T {ro : ring_like_op T} :=
  { ix_os : rngl_has_opp_or_psub T = true }.

Ltac destruct_ix :=
  set (Hos := ix_os).


Theorem forall_pair {A B} {P : A → B → Prop} :
  (∀ a b, P a b) ↔ (∀ ab, P (fst ab) (snd ab)).

Theorem forall_pair_in {A B P l} :
  (∀ ab : A × B, (fst ab, snd ab) ∈ l → P ab) ↔
  (∀ ab : A × B, ab ∈ l → P ab).

Theorem forall_in_seq {A B} da db la lb (P : A → B → Prop) :
  length la = length lb →
  (∀ i,
   i ∈ List.seq 0 (length la) → P (List.nth i la da) (List.nth i lb db)) ↔
  (∃ lab, la = List.map fst lab ∧ lb = List.map snd lab ∧
   ∀ ab, ab ∈ lab → P (fst ab) (snd ab)).
Require Import Stdlib.Logic.PropExtensionality.
Require Import Stdlib.Logic.FunctionalExtensionality.
Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context {ix : ideal_ctx T}.


Theorem I_zero_add a b : a = 0%L → b = 0%L → (a + b = 0)%L.

Theorem I_zero_mul_l a b : b = 0%L → (a × b = 0)%L.

Theorem I_zero_mul_r a b : a = 0%L → (a × b = 0)%L.


Definition I_add_subset I J z :=
  ∃ x y, (x ∈ I)%I ∧ (y ∈ J)%I ∧ z = (x + y)%L.

Arguments I_add_subset (I J)%_I z%_L.

Theorem I_add_zero I J : I_add_subset I J 0%L.

Theorem I_add_add I J :
  ∀ x y, I_add_subset I J x → I_add_subset I J y → I_add_subset I J (x + y)%L.

Theorem I_add_mul_l I J :
  ∀ x y, I_add_subset I J y → I_add_subset I J (x × y).

Theorem I_add_mul_r I J :
  ∀ x y, I_add_subset I J x → I_add_subset I J (x × y).


Definition I_mul_subset_prop I J z lxy :=
  length lxy ≠ 0 ∧
  (∀ x y, (x, y) ∈ lxy → (x ∈ I)%I ∧ (y ∈ J)%I) ∧
  z = ∑ ((x, y) ∈ lxy), x × y.

Definition I_mul_subset I J z := ∃ lxy, I_mul_subset_prop I J z lxy.

Arguments I_mul_subset (I J)%_I z%_L.

Theorem I_mul_zero I J : I_mul_subset I J 0%L.

Theorem I_mul_add I J :
  ∀ x y, I_mul_subset I J x → I_mul_subset I J y → I_mul_subset I J (x + y)%L.

Theorem I_mul_mul_l I J :
  ∀ x y, I_mul_subset I J y → I_mul_subset I J (x × y).

Theorem I_mul_mul_r I J :
  ∀ x y, I_mul_subset I J x → I_mul_subset I J (x × y).


Definition I_zero : ideal T :=
  {| i_subset a := a = 0%L;
     i_zero := eq_refl;
     i_add := I_zero_add;
     i_mul_l := I_zero_mul_l;
     i_mul_r := I_zero_mul_r |}.

Definition I_one : ideal T :=
  {| i_subset a := True;
     i_zero := I;
     i_add _ _ _ _ := I;
     i_mul_l _ _ _ := I;
     i_mul_r _ _ _ := I |}.

Definition I_add (I J : ideal T) : ideal T :=
  {| i_subset := I_add_subset I J;
     i_zero := I_add_zero I J;
     i_add := I_add_add I J;
     i_mul_l := I_add_mul_l I J;
     i_mul_r := I_add_mul_r I J |}.

Definition I_mul (I J : ideal T) : ideal T :=
  {| i_subset := I_mul_subset I J;
     i_zero := I_mul_zero I J;
     i_add := I_mul_add I J;
     i_mul_l := I_mul_mul_l I J;
     i_mul_r := I_mul_mul_r I J |}.


Definition I_ring_like_op : ring_like_op (ideal T) :=
  {| rngl_zero := I_zero;
     rngl_one := I_one;
     rngl_add := I_add;
     rngl_mul := I_mul;
     rngl_opt_opp_or_psub := None;
     rngl_opt_inv_or_pdiv := None;
     rngl_opt_is_zero_divisor := Some (λ _, True);
     rngl_opt_eq_dec := None;
     rngl_opt_leb := None |}.

End a.

Notation "0" := I_zero : ideal_scope.
Notation "1" := I_one : ideal_scope.
Notation "I + J" := (I_add I J) : ideal_scope.
Notation "I * J" := (I_mul I J) : ideal_scope.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context {ix : ideal_ctx T}.

Theorem eq_ideal_eq : ∀ I J,
  i_subset I = i_subset J
  ↔ I = J.

Theorem I_add_subset_comm I J z : I_add_subset I J z = I_add_subset J I z.
Theorem I_add_comm : ∀ I J, (I + J)%I = (J + I)%I.

Theorem I_add_subset_assoc_l I J K x z :
  (x ∈ I)%I → (z ∈ J + K)%I → I_add_subset (I + J) K (x + z)%L.

Theorem I_add_subset_assoc I J K x :
  I_add_subset I (J + K) x = I_add_subset (I + J) K x.
Theorem I_add_assoc : ∀ I J K, (I + (J + K))%I = ((I + J) + K)%I.

Theorem I_add_subset_0_l I x : I_add_subset 0 I x = (x ∈ I)%I.
Theorem I_add_0_l I : (0 + I)%I = I.

Theorem forall_exists_exists_forall {A B} (da : A) (db : B) P Q la :
  (∀ a, a ∈ la → P a ∧ ∃ n, Q a n)
  ↔ ∃ lb, length lb = length la ∧
    ∀ i,
    i ∈ List.seq 0 (length lb)
    → P (List.nth i la da) ∧ Q (List.nth i la da) (List.nth i lb db).
Theorem I_subset_mul_assoc_l :
  ∀ I J K x y z, (x ∈ I → y ∈ J → z ∈ K → x × y × z ∈ I × J × K)%I.

Theorem I_subset_mul_assoc_r :
  ∀ I J K x y z, (x ∈ I → y ∈ J → z ∈ K → x × y × z ∈ I × (J × K))%I.

Theorem I_subset_sum_mul_assoc_l {A} :
  ∀ I J K li (f g h : A → T),
  (∀ i, i ∈ li → (f i ∈ I)%I)
  → (∀ i, i ∈ li → (g i ∈ J)%I)
  → (∀ i, i ∈ li → (h i ∈ K)%I)
  → (∑ (i ∈ li), f i × g i × h i ∈ I × J × K)%I.

Theorem I_subset_sum_mul_assoc_r {A} :
  ∀ I J K li (f g h : A → T),
  (∀ i, i ∈ li → (f i ∈ I)%I)
  → (∀ i, i ∈ li → (g i ∈ J)%I)
  → (∀ i, i ∈ li → (h i ∈ K)%I)
  → (∑ (i ∈ li), f i × g i × h i ∈ I × (J × K))%I.

Theorem I_subset_sum_sum_mul_assoc_l {A B} :
  ∀ I J K li lj (f g h : A → B → T),
  (∀ i j, i ∈ li → j ∈ lj i → (f i j ∈ I)%I)
  → (∀ i j, i ∈ li → j ∈ lj i → (g i j ∈ J)%I)
  → (∀ i j, i ∈ li → j ∈ lj i → (h i j ∈ K)%I)
  → (∑ (i ∈ li), ∑ (j ∈ lj i), f i j × g i j × h i j ∈ I × J × K)%I.

Theorem I_subset_sum_sum_mul_assoc_r {A B} :
  ∀ I J K li lj (f g h : A → B → T),
  (∀ i j, i ∈ li → j ∈ lj i → (f i j ∈ I)%I)
  → (∀ i j, i ∈ li → j ∈ lj i → (g i j ∈ J)%I)
  → (∀ i j, i ∈ li → j ∈ lj i → (h i j ∈ K)%I)
  → (∑ (i ∈ li), ∑ (j ∈ lj i), f i j × g i j × h i j ∈ I × (J × K))%I.

Theorem I_subset_mul_assoc_l_mul_assoc_r I J K :
  ∀ z, (z ∈ I × (J × K) → z ∈ (I × J) × K)%I.
Theorem I_subset_mul_assoc_l_mul_assoc_l I J K :
  ∀ z, (z ∈ (I × J) × K → z ∈ I × (J × K))%I.
Theorem I_mul_subset_assoc I J K x :
  I_mul_subset I (J × K) x = I_mul_subset (I × J) K x.

Theorem I_mul_assoc I J K : (I × (J × K))%I = ((I × J) × K)%I.

Theorem I_mul_subset_1_l I : ∀ x, I_mul_subset 1 I x = (x ∈ I)%I.
Theorem I_mul_1_l : ∀ I : ideal T, (1 × I)%I = I.

Theorem I_mul_subset_add_distr_l_1 I J K :
  ∀ t, (t ∈ I × (J + K) → t ∈ I × J + I × K)%I.
Theorem I_mul_subset_add_distr_r_1 I J K :
  ∀ t, (t ∈ (I + J) × K → t ∈ I × K + J × K)%I.
Theorem I_mul_subset_add_distr_l_2_lemma I J K lab :
  length lab ≠ 0
  → (∀ x y, (x, y) ∈ lab → (x ∈ I)%I ∧ (y ∈ J)%I)
  → (∑ ((x, y) ∈ lab), x × y ∈ I × (J + K))%I.

Theorem I_mul_subset_add_distr_r_2_lemma I J K lab :
  length lab ≠ 0
  → (∀ x y : T, (x, y) ∈ lab → (x ∈ I)%I ∧ (y ∈ K)%I)
  → (∑ ((x, y) ∈ lab), x × y ∈ (I + J) × K)%I.

Theorem I_mul_subset_add_distr_l_2 I J K :
  ∀ t, (t ∈ I × J + I × K → t ∈ I × (J + K))%I.
Theorem I_mul_subset_add_distr_r_2 I J K :
  ∀ t, (t ∈ I × K + J × K → t ∈ (I + J) × K)%I.
Theorem I_mul_subset_add_distr_l I J K x :
  I_mul_subset I (J + K) x = I_add_subset (I × J) (I × K) x.

Theorem I_mul_subset_add_distr_r I J K x :
  I_mul_subset (I + J) K x = I_add_subset (I × K) (J × K) x.

Theorem I_mul_add_distr_l I J K : (I × (J + K))%I = (I × J + I × K)%I.

Theorem I_mul_add_distr_r I J K : ((I + J) × K)%I = (I × K + J × K)%I.

Theorem I_mul_subset_comm :
  rngl_mul_is_comm T = true →
  ∀ I J x, I_mul_subset I J x = I_mul_subset J I x.
Theorem I_opt_mul_comm :
  if rngl_mul_is_comm T then ∀ I J : ideal T, (I × J)%I = (J × I)%I
  else not_applicable.

Theorem I_mul_subset_1_r I : ∀ x, I_mul_subset I 1 x = (x ∈ I)%I.
Theorem I_opt_mul_1_r :
  if rngl_mul_is_comm T then not_applicable else ∀ I : ideal T, (I × 1)%I = I.

Theorem I_opt_mul_add_distr_r :
  if rngl_mul_is_comm T then not_applicable
  else ∀ I J K : ideal T, ((I + J) × K)%I = (I × K + J × K)%I.

Theorem I_opt_integral I J :
  (I × J)%I = 0%I → I = 0%I ∨ J = 0%I ∨ True ∨ True.

Theorem I_characteristic_prop :
  let roi := I_ring_like_op in
  if Nat.b2n (rngl_characteristic T =? 1) =? 0 then
    ∀ i : nat, rngl_of_nat (S i) ≠ 0%L
  else
   (∀ i : nat,
      0 < i < Nat.b2n (rngl_characteristic T =? 1) → rngl_of_nat i ≠ 0%L)
   ∧ rngl_of_nat (Nat.b2n (rngl_characteristic T =? 1)) = 0%L.

Definition I_ring_like_prop : ring_like_prop (ideal T) :=
  let roi := I_ring_like_op in
  {| rngl_mul_is_comm := rngl_mul_is_comm T;
     rngl_is_archimedean := false;
     rngl_is_alg_closed := false;
     rngl_characteristic := Nat.b2n (rngl_characteristic T =? 1);
     rngl_add_comm := I_add_comm;
     rngl_add_assoc := I_add_assoc;
     rngl_add_0_l := I_add_0_l;
     rngl_mul_assoc := I_mul_assoc;
     rngl_mul_1_l := I_mul_1_l;
     rngl_mul_add_distr_l := I_mul_add_distr_l;
     rngl_opt_mul_comm := I_opt_mul_comm;
     rngl_opt_mul_1_r := I_opt_mul_1_r;
     rngl_opt_mul_add_distr_r := I_opt_mul_add_distr_r;
     rngl_opt_add_opp_diag_l := NA;
     rngl_opt_add_sub := NA;
     rngl_opt_sub_add_distr := NA;
     rngl_opt_mul_inv_diag_l := NA;
     rngl_opt_mul_inv_diag_r := NA;
     rngl_opt_mul_div := NA;
     rngl_opt_integral := I_opt_integral;
     rngl_opt_alg_closed := NA;
     rngl_opt_ord := NA;
     rngl_opt_archimedean := NA;
     rngl_characteristic_prop := I_characteristic_prop |}.

End a.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context {ix : ideal_ctx T}.


Axiom i_subset_incl_dec : ∀ I J,
  { ∀ x, i_subset I x → i_subset J x } +
  { ¬ ∀ x, i_subset I x → i_subset J x }.

Definition I_leb (I J : ideal T) := bool_of_sumbool (i_subset_incl_dec I J).

Notation "I '⊂' J" := (i_subset_incl_dec I J) (at level 70) : ideal_scope.
Notation "I ≤ J" := (I_leb I J) : ideal_scope.

Definition I_ring_like_op' : ring_like_op (ideal T) :=
  {| rngl_zero := I_zero;
     rngl_one := I_one;
     rngl_add := I_add;
     rngl_mul := I_mul;
     rngl_opt_opp_or_psub := None;
     rngl_opt_inv_or_pdiv := None;
     rngl_opt_is_zero_divisor := Some (λ _, True);
     rngl_opt_eq_dec := None;
     rngl_opt_leb := Some (I_leb, false) |}.

Theorem I_ord_le_dec I J : {(I ≤ J)%I = true} + {(I ≤ J)%I ≠ true}.

Theorem I_ord_le_refl I : (I ≤ I)%I = true.

Theorem I_ord_le_antisymm I J : (I ≤ J)%I = true → (J ≤ I)%I = true → I = J.

Theorem I_ord_le_trans I J K :
  (I ≤ J)%I = true → (J ≤ K)%I = true → (I ≤ K)%I = true.

Theorem I_ord_mul_le_compat_nonneg I J K L :
  (0 ≤ I)%I = true ∧ (I ≤ K)%I = true
  → (0 ≤ J)%I = true ∧ (J ≤ L)%I = true
  → (I × J ≤ K × L)%I = true.

Theorem I_ord_mul_le_compat_nonpos I J K L :
  (K ≤ I)%I = true ∧ (I ≤ 0)%I = true
  → (L ≤ J)%I = true ∧ (J ≤ 0)%I = true
  → (I × J ≤ K × L)%I = true.

Definition I_ring_like_ord' : ring_like_ord (ideal T) :=
  let roi := I_ring_like_op' in
  {| rngl_ord_le_refl := I_ord_le_refl;
     rngl_ord_le_antisymm := I_ord_le_antisymm;
     rngl_ord_le_trans := I_ord_le_trans;
     rngl_ord_add_le_mono_l := NA;
     rngl_ord_mul_le_compat_nonneg := I_ord_mul_le_compat_nonneg;
     rngl_ord_mul_le_compat_nonpos := I_ord_mul_le_compat_nonpos;
     rngl_ord_le_dec := I_ord_le_dec;
     rngl_ord_total_prop := NA |}.

Definition I_ring_like_prop' : ring_like_prop (ideal T) :=
  let roi := I_ring_like_op' in
  {| rngl_mul_is_comm := rngl_mul_is_comm T;
     rngl_is_archimedean := false;
     rngl_is_alg_closed := false;
     rngl_characteristic := Nat.b2n (rngl_characteristic T =? 1);
     rngl_add_comm := I_add_comm;
     rngl_add_assoc := I_add_assoc;
     rngl_add_0_l := I_add_0_l;
     rngl_mul_assoc := I_mul_assoc;
     rngl_mul_1_l := I_mul_1_l;
     rngl_mul_add_distr_l := I_mul_add_distr_l;
     rngl_opt_mul_comm := I_opt_mul_comm;
     rngl_opt_mul_1_r := I_opt_mul_1_r;
     rngl_opt_mul_add_distr_r := I_opt_mul_add_distr_r;
     rngl_opt_add_opp_diag_l := NA;
     rngl_opt_add_sub := NA;
     rngl_opt_sub_add_distr := NA;
     rngl_opt_mul_inv_diag_l := NA;
     rngl_opt_mul_inv_diag_r := NA;
     rngl_opt_mul_div := NA;
     rngl_opt_integral := I_opt_integral;
     rngl_opt_alg_closed := NA;
     rngl_opt_ord := I_ring_like_ord';
     rngl_opt_archimedean := NA;
     rngl_characteristic_prop := I_characteristic_prop |}.

End a.