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).