# Library Coq.field.LegacyField_Theory

Require Import List.
Require Import Peano_dec.
Require Import LegacyRing.
Require Import LegacyField_Compl.

Record Field_Theory : Type :=
{A : Type;
Aplus : A -> A -> A;
Amult : A -> A -> A;
Aone : A;
Azero : A;
Aopp : A -> A;
Aeq : A -> A -> bool;
Ainv : A -> A;
Aminus : option (A -> A -> A);
Adiv : option (A -> A -> A);
RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq;
Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}.

Inductive ExprA : Set :=
| EAzero : ExprA
| EAone : ExprA
| EAplus : ExprA -> ExprA -> ExprA
| EAmult : ExprA -> ExprA -> ExprA
| EAopp : ExprA -> ExprA
| EAinv : ExprA -> ExprA
| EAvar : nat -> ExprA.

Lemma eqExprA_O : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}.

Definition eq_nat_dec := Eval compute in eq_nat_dec.
Definition eqExprA := Eval compute in eqExprA_O.

Fixpoint mult_of_list (e:list ExprA) : ExprA :=
match e with
| nil => EAone
| e1 :: l1 => EAmult e1 (mult_of_list l1)
end.

Section Theory_of_fields.

Variable T : Field_Theory.

Let AT := A T.
Let AplusT := Aplus T.
Let AmultT := Amult T.
Let AoneT := Aone T.
Let AzeroT := Azero T.
Let AoppT := Aopp T.
Let AeqT := Aeq T.
Let AinvT := Ainv T.
Let RTT := RT T.
Let Th_inv_defT := Th_inv_def T.

Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (
Azero T) (Aopp T) (Aeq T) (RT T).

Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.

Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.

Lemma AplusT_assoc :
forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).

Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.

Lemma AmultT_assoc :
forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).

Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.

Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.

Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.

Lemma AmultT_AplusT_distr :
forall r1 r2 r3:AT,
AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3).

Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2.

Lemma r_AmultT_mult :
forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2.

Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.

Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.

Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.

Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.

Lemma Rmult_neq_0_reg :
forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT.

Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
AT :=
match e with
| EAzero => AzeroT
| EAone => AoneT
| EAplus e1 e2 => AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
| EAmult e1 e2 => AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
| EAopp e => Aopp T (interp_ExprA lvar e)
| EAinv e => Ainv T (interp_ExprA lvar e)
| EAvar n => assoc_2nd AT nat eq_nat_dec lvar n AzeroT
end.

Definition merge_mult :=
(fix merge_mult (e1:ExprA) : ExprA -> ExprA :=
fun e2:ExprA =>
match e1 with
| EAmult t1 t2 =>
match t2 with
| EAmult t2 t3 => EAmult t1 (EAmult t2 (merge_mult t3 e2))
| _ => EAmult t1 (EAmult t2 e2)
end
| _ => EAmult e1 e2
end).

Fixpoint assoc_mult (e:ExprA) : ExprA :=
match e with
| EAmult e1 e3 =>
match e1 with
| EAmult e1 e2 =>
merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2))
(assoc_mult e3)
| _ => EAmult e1 (assoc_mult e3)
end
| _ => e
end.

Definition merge_plus :=
(fix merge_plus (e1:ExprA) : ExprA -> ExprA :=
fun e2:ExprA =>
match e1 with
| EAplus t1 t2 =>
match t2 with
| EAplus t2 t3 => EAplus t1 (EAplus t2 (merge_plus t3 e2))
| _ => EAplus t1 (EAplus t2 e2)
end
| _ => EAplus e1 e2
end).

Fixpoint assoc (e:ExprA) : ExprA :=
match e with
| EAplus e1 e3 =>
match e1 with
| EAplus e1 e2 =>
merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3)
| _ => EAplus (assoc_mult e1) (assoc e3)
end
| _ => assoc_mult e
end.

Lemma merge_mult_correct1 :
forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) =
interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)).

Lemma merge_mult_correct :
forall (e1 e2:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).

Lemma assoc_mult_correct1 :
forall (e1 e2:ExprA) (lvar:list (AT * nat)),
AmultT (interp_ExprA lvar (assoc_mult e1))
(interp_ExprA lvar (assoc_mult e2)) =
interp_ExprA lvar (assoc_mult (EAmult e1 e2)).

Lemma assoc_mult_correct :
forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.

Lemma merge_plus_correct1 :
forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) =
interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)).

Lemma merge_plus_correct :
forall (e1 e2:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).

Lemma assoc_plus_correct :
forall (e1 e2:ExprA) (lvar:list (AT * nat)),
AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) =
interp_ExprA lvar (assoc (EAplus e1 e2)).

Lemma assoc_correct :
forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (assoc e) = interp_ExprA lvar e.

Fixpoint distrib_EAopp (e:ExprA) : ExprA :=
match e with
| EAplus e1 e2 => EAplus (distrib_EAopp e1) (distrib_EAopp e2)
| EAmult e1 e2 => EAmult (distrib_EAopp e1) (distrib_EAopp e2)
| EAopp e => EAmult (EAopp EAone) (distrib_EAopp e)
| e => e
end.

Definition distrib_mult_right :=
(fix distrib_mult_right (e1:ExprA) : ExprA -> ExprA :=
fun e2:ExprA =>
match e1 with
| EAplus t1 t2 =>
EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2)
| _ => EAmult e1 e2
end).

Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA :=
match e1 with
| EAplus t1 t2 =>
EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2)
| _ => distrib_mult_right e2 e1
end.

Fixpoint distrib_main (e:ExprA) : ExprA :=
match e with
| EAmult e1 e2 => distrib_mult_left (distrib_main e1) (distrib_main e2)
| EAplus e1 e2 => EAplus (distrib_main e1) (distrib_main e2)
| EAopp e => EAopp (distrib_main e)
| _ => e
end.

Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).

Lemma distrib_mult_right_correct :
forall (e1 e2:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (distrib_mult_right e1 e2) =
AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).

Lemma distrib_mult_left_correct :
forall (e1 e2:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (distrib_mult_left e1 e2) =
AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).

Lemma distrib_correct :
forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (distrib e) = interp_ExprA lvar e.

Lemma mult_eq :
forall (e1 e2 a:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar a <> AzeroT ->
interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) ->
interp_ExprA lvar e1 = interp_ExprA lvar e2.

Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA :=
match e with
| EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2)
| _ => EAmult a e
end.

Definition multiply (e:ExprA) : ExprA :=
match e with
| EAmult a e1 => multiply_aux a e1
| _ => e
end.

Lemma multiply_aux_correct :
forall (a e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (multiply_aux a e) =
AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).

Lemma multiply_correct :
forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (multiply e) = interp_ExprA lvar e.

Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA :=
match m with
| EAmult m0 m1 =>
match eqExprA m0 (EAinv a) with
| left _ => m1
| right _ => EAmult m0 (monom_remove a m1)
end
| _ =>
match eqExprA m (EAinv a) with
| left _ => EAone
| right _ => EAmult a m
end
end.

Definition monom_simplif_rem :=
(fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA :=
fun m:ExprA =>
match a with
| EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m)
| _ => monom_remove a m
end).

Definition monom_simplif (a m:ExprA) : ExprA :=
match m with
| EAmult a' m' =>
match eqExprA a a' with
| left _ => monom_simplif_rem a m'
| right _ => m
end
| _ => m
end.

Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
match e with
| EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2)
| _ => monom_simplif a e
end.

Lemma monom_remove_correct :
forall (e a:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar a <> AzeroT ->
interp_ExprA lvar (monom_remove a e) =
AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).

Lemma monom_simplif_rem_correct :
forall (a e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar a <> AzeroT ->
interp_ExprA lvar (monom_simplif_rem a e) =
AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).

Lemma monom_simplif_correct :
forall (e a:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar a <> AzeroT ->
interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e.

Lemma inverse_correct :
forall (e a:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar a <> AzeroT ->
interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e.

End Theory_of_fields.

Notation AplusT_sym := AplusT_comm (only parsing).
Notation AmultT_sym := AmultT_comm (only parsing).