Timings for Field_theory.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./setoid_ring/Field_theory.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./setoid_ring/Field_theory.timing
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms.
Require Import ZArith_base.
(* Set Universe Polymorphism. *)
Bind Scope R_scope with R.
Delimit Scope R_scope with ring.
Local Open Scope R_scope.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
Variable (rdiv : R->R->R) (rinv : R->R).
Variable req : R -> R -> Prop.
Notation "0" := rO : R_scope.
Notation "1" := rI : R_scope.
Infix "+" := radd : R_scope.
Infix "-" := rsub : R_scope.
Infix "*" := rmul : R_scope.
Infix "/" := rdiv : R_scope.
Notation "- x" := (ropp x) : R_scope.
Notation "/ x" := (rinv x) : R_scope.
Infix "==" := req (at level 70, no associativity) : R_scope.
(* Equality properties *)
Variable Rsth : Equivalence req.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Variable SRinv_ext : forall p q, p == q -> / p == / q.
Record almost_field_theory : Prop := mk_afield {
AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req;
AF_1_neq_0 : ~ 1 == 0;
AFdiv_def : forall p q, p / q == p * / q;
AFinv_l : forall p, ~ p == 0 -> / p * p == 1
}.
Variable AFth : almost_field_theory.
Let ARth := (AF_AR AFth).
Let rI_neq_rO := (AF_1_neq_0 AFth).
Let rdiv_def := (AFdiv_def AFth).
Let rinv_l := (AFinv_l AFth).
Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
Add Morphism ropp with signature (req ==> req) as ropp_ext.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
exact (ARsub_ext Rsth Reqe ARth).
Add Morphism rinv with signature (req ==> req) as rinv_ext.
Let eq_trans := Setoid.Seq_trans _ _ Rsth.
Let eq_sym := Setoid.Seq_sym _ _ Rsth.
Let eq_refl := Setoid.Seq_refl _ _ Rsth.
Let radd_0_l := ARadd_0_l ARth.
Let radd_comm := ARadd_comm ARth.
Let radd_assoc := ARadd_assoc ARth.
Let rmul_1_l := ARmul_1_l ARth.
Let rmul_0_l := ARmul_0_l ARth.
Let rmul_comm := ARmul_comm ARth.
Let rmul_assoc := ARmul_assoc ARth.
Let rdistr_l := ARdistr_l ARth.
Let ropp_mul_l := ARopp_mul_l ARth.
Let ropp_add := ARopp_add ARth.
Let rsub_def := ARsub_def ARth.
Let radd_0_r := ARadd_0_r Rsth ARth.
Let rmul_0_r := ARmul_0_r Rsth ARth.
Let rmul_1_r := ARmul_1_r Rsth ARth.
Let ropp_0 := ARopp_zero Rsth Reqe ARth.
Let rdistr_r := ARdistr_r Rsth Reqe ARth.
Bind Scope C_scope with C.
Delimit Scope C_scope with coef.
Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
Variable ceqb : C->C->bool.
Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
Notation "0" := cO : C_scope.
Notation "1" := cI : C_scope.
Infix "+" := cadd : C_scope.
Infix "-" := csub : C_scope.
Infix "*" := cmul : C_scope.
Notation "- x" := (copp x) : C_scope.
Infix "=?" := ceqb : C_scope.
Notation "[ x ]" := (phi x) (at level 0).
Let phi_0 := (morph0 CRmorph).
Let phi_1 := (morph1 CRmorph).
Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef.
generalize ((morph_eq CRmorph) c c').
destruct (c =? c')%coef; auto.
(* Power coefficients : Cpow *)
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
Variable get_sign : C -> option C.
Variable get_sign_spec : sign_theory copp ceqb get_sign.
Variable cdiv:C -> C -> C*C.
Variable cdiv_th : div_theory req cadd cmul phi cdiv.
Let rpow_pow := (rpow_pow_N pow_th).
(* Polynomial expressions : (PExpr C) *)
Bind Scope PE_scope with PExpr.
Delimit Scope PE_scope with poly.
Notation NPEeval := (PEeval rO rI radd rmul rsub ropp phi Cp_phi rpow).
Notation "P @ l" := (NPEeval l P) (at level 10, no associativity).
Notation "0" := (PEc 0) : PE_scope.
Notation "1" := (PEc 1) : PE_scope.
Infix "+" := PEadd : PE_scope.
Infix "-" := PEsub : PE_scope.
Infix "*" := PEmul : PE_scope.
Notation "- e" := (PEopp e) : PE_scope.
Infix "^" := PEpow : PE_scope.
Definition NPEequiv e e' := forall l, e@l == e'@l.
Infix "===" := NPEequiv (at level 70, no associativity) : PE_scope.
Instance NPEequiv_eq : Equivalence NPEequiv.
split; red; unfold NPEequiv; intros; [reflexivity|symmetry|etransitivity];
eauto.
Instance NPEeval_ext : Proper (eq ==> NPEequiv ==> req) NPEeval.
Notation Nnorm :=
(norm_subst cO cI cadd cmul csub copp ceqb cdiv).
Notation NPphi_dev :=
(Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign).
Notation NPphi_pow :=
(Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign).
(* add abstract semi-ring to help with some proofs *)
Add Ring Rring : (ARth_SRth ARth).
(* additional ring properties *)
Lemma rsub_0_l r : 0 - r == - r.
Lemma rsub_0_r r : r - 0 == r.
rewrite rsub_def, ropp_0; ring.
(***************************************************************************
Properties of division
***************************************************************************)
Theorem rdiv_simpl p q : ~ q == 0 -> q * (p / q) == p.
transitivity (/ q * q * p); [ ring | ].
Instance rdiv_ext: Proper (req ==> req ==> req) rdiv.
intros p1 p2 Ep q1 q2 Eq.
now rewrite !rdiv_def, Ep, Eq.
Lemma rmul_reg_l p q1 q2 :
~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
assert (H' : p * (q1 / p) == p * (q2 / p)).
now rewrite !rdiv_def, !rmul_assoc, EQ.
now rewrite !rdiv_simpl in H'.
Theorem field_is_integral_domain r1 r2 :
~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0.
transitivity (/r1 * r1 * r2).
now rewrite <- rmul_assoc, H2.
Theorem ropp_neq_0 r :
~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0.
setoid_replace (- r) with (- (1) * r).
apply field_is_integral_domain; trivial.
now rewrite <- ropp_mul_l, rmul_1_l.
Theorem rdiv_r_r r : ~ r == 0 -> r / r == 1.
rewrite rdiv_def, rmul_comm.
Theorem rdiv1 r : r == r / 1.
transitivity (1 * (r / 1)).
symmetry; apply rdiv_simpl.
Theorem rdiv2 a b c d :
~ b == 0 ->
~ d == 0 ->
a / b + c / d == (a * d + c * b) / (b * d).
assert (~ b * d == 0) by now apply field_is_integral_domain.
apply rmul_reg_l with (b * d); trivial.
rewrite rdiv_simpl; trivial.
now rewrite <- rmul_assoc, (rmul_comm d), rmul_assoc, rdiv_simpl.
now rewrite (rmul_comm c), <- rmul_assoc, rdiv_simpl.
Theorem rdiv2b a b c d e :
~ (b*e) == 0 ->
~ (d*e) == 0 ->
a / (b*e) + c / (d*e) == (a * d + c * b) / (b * (d * e)).
assert (~ b == 0) by (contradict H; rewrite H; ring).
assert (~ e == 0) by (contradict H; rewrite H; ring).
assert (~ d == 0) by (contradict H0; rewrite H0; ring).
assert (~ b * (d * e) == 0)
by (repeat apply field_is_integral_domain; trivial).
apply rmul_reg_l with (b * (d * e)); trivial.
rewrite rdiv_simpl; trivial.
transitivity ((b * e) * (a / (b * e)) * d);
[ ring | now rewrite rdiv_simpl ].
transitivity ((d * e) * (c / (d * e)) * b);
[ ring | now rewrite rdiv_simpl ].
Theorem rdiv5 a b : - (a / b) == - a / b.
now rewrite !rdiv_def, ropp_mul_l.
Theorem rdiv3b a b c d e :
~ (b * e) == 0 ->
~ (d * e) == 0 ->
a / (b*e) - c / (d*e) == (a * d - c * b) / (b * (d * e)).
rewrite !rsub_def, rdiv5, ropp_mul_l.
Theorem rdiv6 a b :
~ a == 0 -> ~ b == 0 -> / (a / b) == b / a.
assert (Hk : ~ a / b == 0).
transitivity (b * (a / b)).
apply rmul_reg_l with (a / b); trivial.
rewrite (rmul_comm (a / b)), rinv_l; trivial.
transitivity (/ a * a * (/ b * b)); [ | ring ].
now rewrite !rinv_l, rmul_1_l.
Theorem rdiv4 a b c d :
~ b == 0 ->
~ d == 0 ->
(a / b) * (c / d) == (a * c) / (b * d).
assert (~ b * d == 0) by now apply field_is_integral_domain.
apply rmul_reg_l with (b * d); trivial.
rewrite rdiv_simpl; trivial.
transitivity (b * (a / b) * (d * (c / d))); [ ring | ].
rewrite !rdiv_simpl; trivial.
Theorem rdiv4b a b c d e f :
~ b * e == 0 ->
~ d * f == 0 ->
((a * f) / (b * e)) * ((c * e) / (d * f)) == (a * c) / (b * d).
assert (~ b == 0) by (contradict H; rewrite H; ring).
assert (~ e == 0) by (contradict H; rewrite H; ring).
assert (~ d == 0) by (contradict H0; rewrite H0; ring).
assert (~ f == 0) by (contradict H0; rewrite H0; ring).
assert (~ b*d == 0) by now apply field_is_integral_domain.
assert (~ e*f == 0) by now apply field_is_integral_domain.
transitivity ((e * f) * (a * c) / ((e * f) * (b * d))).
rewrite <- rdiv4, rdiv_r_r; trivial.
Theorem rdiv7 a b c d :
~ b == 0 ->
~ c == 0 ->
~ d == 0 ->
(a / b) / (c / d) == (a * d) / (b * c).
rewrite (rdiv_def (a / b)).
Theorem rdiv7b a b c d e f :
~ b * f == 0 ->
~ c * e == 0 ->
~ d * f == 0 ->
((a * e) / (b * f)) / ((c * e) / (d * f)) == (a * d) / (b * c).
assert (~ c==0) by (contradict Hce; rewrite Hce; ring).
assert (~ e==0) by (contradict Hce; rewrite Hce; ring).
assert (~ b==0) by (contradict Hbf; rewrite Hbf; ring).
assert (~ f==0) by (contradict Hbf; rewrite Hbf; ring).
assert (~ b*c==0) by now apply field_is_integral_domain.
assert (~ e*f==0) by now apply field_is_integral_domain.
transitivity ((e * f) * (a * d) / ((e * f) * (b * c))).
now rewrite <- rdiv4, rdiv_r_r.
Theorem rinv_nz a : ~ a == 0 -> ~ /a == 0.
rewrite <- (rdiv_r_r H), rdiv_def, H0.
Theorem rdiv8 a b : ~ b == 0 -> a == 0 -> a / b == 0.
now rewrite rdiv_def, H0, rmul_0_l.
Theorem cross_product_eq a b c d :
~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d.
transitivity (a / b * (d / d)).
now rewrite rdiv_r_r, rmul_1_r.
now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r.
(* Results about [pow_pos] and [pow_N] *)
Instance pow_ext : Proper (req ==> eq ==> req) (pow_pos rmul).
induction p as [p IH| p IH|];simpl; trivial; now rewrite !IH, ?H.
Instance pow_N_ext : Proper (req ==> eq ==> req) (pow_N rI rmul).
destruct n; simpl; trivial.
Lemma pow_pos_0 p : pow_pos rmul 0 p == 0.
induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !IHp.
Lemma pow_pos_1 p : pow_pos rmul 1 p == 1.
induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp].
Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p].
induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp.
Lemma pow_pos_mul_l x y p :
pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p.
induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp].
Lemma pow_pos_add_r x p1 p2 :
pow_pos rmul x (p1+p2) == pow_pos rmul x p1 * pow_pos rmul x p2.
exact (Ring_theory.pow_pos_add Rsth rmul_ext rmul_assoc x p1 p2).
Lemma pow_pos_mul_r x p1 p2 :
pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2.
induction p1 as [p1 IHp1|p1 IHp1|];simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r;
simpl; trivial; ring [IHp1].
Lemma pow_pos_nz x p : ~x==0 -> ~pow_pos rmul x p == 0.
induction p;simpl;trivial;
repeat (apply field_is_integral_domain; trivial).
Lemma pow_pos_div a b p : ~ b == 0 ->
pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p.
induction p as [p IHp|p IHp|]; simpl; trivial.
assert (nz := pow_pos_nz p H).
apply field_is_integral_domain; trivial.
assert (nz := pow_pos_nz p H).
Instance PEadd_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEadd C).
Instance PEsub_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEsub C).
Instance PEmul_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEmul C).
Instance PEopp_ext : Proper (NPEequiv ==> NPEequiv) (@PEopp C).
Instance PEpow_ext : Proper (NPEequiv ==> eq ==> NPEequiv) (@PEpow C).
apply pow_N_ext; trivial.
Lemma PE_1_l (e : PExpr C) : (1 * e === e)%poly.
Lemma PE_1_r (e : PExpr C) : (e * 1 === e)%poly.
Lemma PEpow_0_r (e : PExpr C) : (e ^ 0 === 1)%poly.
Lemma PEpow_1_r (e : PExpr C) : (e ^ 1 === e)%poly.
Lemma PEpow_1_l n : (1 ^ n === 1)%poly.
now rewrite phi_1, pow_pos_1.
Lemma PEpow_add_r (e : PExpr C) n n' :
(e ^ (n+n') === e ^ n * e ^ n')%poly.
Lemma PEpow_mul_l (e e' : PExpr C) n :
((e * e') ^ n === e ^ n * e' ^ n)%poly.
destruct n; simpl; trivial.
symmetry; apply rmul_1_l.
Lemma PEpow_mul_r (e : PExpr C) n n' :
(e ^ (n * n') === (e ^ n) ^ n')%poly.
destruct n, n'; simpl; trivial.
Lemma PEpow_nz l e n : ~ e @ l == 0 -> ~ (e^n) @ l == 0.
(***************************************************************************
Some equality test
***************************************************************************)
Local Notation "a &&& b" := (if a then b else false)
(at level 40, left associativity).
Fixpoint PExpr_eq (e e' : PExpr C) {struct e} : bool :=
match e, e' with
| PEc c, PEc c' => ceqb c c'
| PEX _ p, PEX _ p' => Pos.eqb p p'
| e1 + e2, e1' + e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
| e1 - e2, e1' - e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
| e1 * e2, e1' * e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
| - e, - e' => PExpr_eq e e'
| e ^ n, e' ^ n' => N.eqb n n' &&& PExpr_eq e e'
| _, _ => false
end%poly.
Lemma if_true (a b : bool) : a &&& b = true -> a = true /\ b = true.
destruct a, b; split; trivial.
Theorem PExpr_eq_semi_ok e e' :
PExpr_eq e e' = true -> (e === e')%poly.
revert e'; induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe ?];
intro e'; destruct e'; simpl; try discriminate.
now apply (morph_eq CRmorph).
case Pos.eqb_spec; intros; now subst.
intros H; destruct (if_true _ _ H).
intros H; destruct (if_true _ _ H).
intros H; destruct (if_true _ _ H).
destruct (if_true _ _ H) as [H0 H1].
Lemma PExpr_eq_spec e e' : BoolSpec (e === e')%poly True (PExpr_eq e e').
assert (H := PExpr_eq_semi_ok e e').
destruct PExpr_eq; constructor; intros; trivial.
(** Smart constructors for polynomial expression,
with reduction of constants *)
Definition NPEadd e1 e2 :=
match e1, e2 with
| PEc c1, PEc c2 => PEc (c1 + c2)
| PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2
| _, PEc c => if (c =? 0)%coef then e1 else e1 + e2
(* Peut t'on factoriser ici ??? *)
| _, _ => (e1 + e2)
end%poly.
Infix "++" := NPEadd (at level 60, right associativity).
Theorem NPEadd_ok e1 e2 : (e1 ++ e2 === e1 + e2)%poly.
destruct e1, e2; simpl; try reflexivity; try (case ceqb_spec);
try intro H; try rewrite H; simpl;
try apply eq_refl; try (ring [phi_0]).
apply (morph_add CRmorph).
Definition NPEsub e1 e2 :=
match e1, e2 with
| PEc c1, PEc c2 => PEc (c1 - c2)
| PEc c, _ => if (c =? 0)%coef then - e2 else e1 - e2
| _, PEc c => if (c =? 0)%coef then e1 else e1 - e2
(* Peut-on factoriser ici *)
| _, _ => e1 - e2
end%poly.
Infix "--" := NPEsub (at level 50, left associativity).
Theorem NPEsub_ok e1 e2: (e1 -- e2 === e1 - e2)%poly.
destruct e1, e2; simpl; try reflexivity; try case ceqb_spec;
try intro H; try rewrite H; simpl;
try rewrite phi_0; try reflexivity;
try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r).
apply (morph_sub CRmorph).
Definition NPEopp e1 :=
match e1 with PEc c1 => PEc (- c1) | _ => - e1 end%poly.
Theorem NPEopp_ok e : (NPEopp e === -e)%poly.
destruct e; simpl; trivial.
apply (morph_opp CRmorph).
Definition NPEpow x n :=
match n with
| N0 => 1
| Npos p =>
if (p =? 1)%positive then x else
match x with
| PEc c =>
if (c =? 1)%coef then 1
else if (c =? 0)%coef then 0
else PEc (pow_pos cmul c p)
| _ => x ^ n
end
end%poly.
Infix "^^" := NPEpow (at level 35, right associativity).
Theorem NPEpow_ok e n : (e ^^ n === e ^ n)%poly.
unfold NPEpow; destruct n.
simpl; now rewrite rpow_pow.
case Pos.eqb_spec; [intro; subst | intros _].
destruct e;simpl;trivial.
repeat case ceqb_spec; intros H **; rewrite ?rpow_pow, ?H; simpl.
now rewrite phi_1, pow_pos_1.
now rewrite phi_0, pow_pos_0.
Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C :=
match x, y with
| PEc c1, PEc c2 => PEc (c1 * c2)
| PEc c, _ => if (c =? 1)%coef then y else if (c =? 0)%coef then 0 else x * y
| _, PEc c => if (c =? 1)%coef then x else if (c =? 0)%coef then 0 else x * y
| e1 ^ n1, e2 ^ n2 => if (n1 =? n2)%N then (NPEmul e1 e2)^^n1 else x * y
| _, _ => x * y
end%poly.
Infix "**" := NPEmul (at level 40, left associativity).
Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly.
revert e2; induction e1 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1|? IHe1 n];
intro e2; destruct e2; simpl;try reflexivity;
repeat (case ceqb_spec; intro H; try rewrite H; clear H);
simpl; try reflexivity; try ring [phi_0 phi_1].
apply (morph_mul CRmorph).
case N.eqb_spec; [intros <- | reflexivity].
destruct n; simpl; [ ring | apply pow_pos_mul_l ].
Fixpoint PEsimp (e : PExpr C) : PExpr C :=
match e with
| e1 + e2 => (PEsimp e1) ++ (PEsimp e2)
| e1 * e2 => (PEsimp e1) ** (PEsimp e2)
| e1 - e2 => (PEsimp e1) -- (PEsimp e2)
| - e1 => NPEopp (PEsimp e1)
| e1 ^ n1 => (PEsimp e1) ^^ n1
| _ => e
end%poly.
Theorem PEsimp_ok e : (PEsimp e === e)%poly.
(****************************************************************************
Datastructure
***************************************************************************)
(* The input: syntax of a field expression *)
Inductive FExpr : Type :=
| FEO : FExpr
| FEI : FExpr
| FEc: C -> FExpr
| FEX: positive -> FExpr
| FEadd: FExpr -> FExpr -> FExpr
| FEsub: FExpr -> FExpr -> FExpr
| FEmul: FExpr -> FExpr -> FExpr
| FEopp: FExpr -> FExpr
| FEinv: FExpr -> FExpr
| FEdiv: FExpr -> FExpr -> FExpr
| FEpow: FExpr -> N -> FExpr .
Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
match pe with
| FEO => rO
| FEI => rI
| FEc c => phi c
| FEX x => BinList.nth 0 x l
| FEadd x y => FEeval l x + FEeval l y
| FEsub x y => FEeval l x - FEeval l y
| FEmul x y => FEeval l x * FEeval l y
| FEopp x => - FEeval l x
| FEinv x => / FEeval l x
| FEdiv x y => FEeval l x / FEeval l y
| FEpow x n => rpow (FEeval l x) (Cp_phi n)
end.
Strategy expand [FEeval].
(* The result of the normalisation *)
Record linear : Type := mk_linear {
num : PExpr C;
denum : PExpr C;
condition : list (PExpr C) }.
(***************************************************************************
Semantics and properties of side condition
***************************************************************************)
Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop :=
match le with
| nil => True
| e1 :: nil => ~ req (e1 @ l) rO
| e1 :: l1 => ~ req (e1 @ l) rO /\ PCond l l1
end.
Theorem PCond_cons l a l1 :
PCond l (a :: l1) <-> ~ a @ l == 0 /\ PCond l l1.
split; [split|destruct 1]; trivial.
Theorem PCond_cons_inv_l l a l1 : PCond l (a::l1) -> ~ a @ l == 0.
Theorem PCond_cons_inv_r l a l1 : PCond l (a :: l1) -> PCond l l1.
Theorem PCond_app l l1 l2 :
PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2.
induction l1 as [|a l1 IHl1].
split; [split|destruct 1]; trivial.
rewrite !PCond_cons, IHl1.
symmetry; apply and_assoc.
(* An unsatisfiable condition: issued when a division by zero is detected *)
Definition absurd_PCond := cons 0%poly nil.
Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond.
unfold absurd_PCond; simpl.
(***************************************************************************
Normalisation
***************************************************************************)
Definition default_isIn e1 p1 e2 p2 :=
if PExpr_eq e1 e2 then
match Z.pos_sub p1 p2 with
| Zpos p => Some (Npos p, 1%poly)
| Z0 => Some (N0, 1%poly)
| Zneg p => Some (N0, e2 ^^ Npos p)
end
else None.
Fixpoint isIn e1 p1 e2 p2 {struct e2}: option (N * PExpr C) :=
match e2 with
| e3 * e4 =>
match isIn e1 p1 e3 p2 with
| Some (N0, e5) => Some (N0, e5 ** (e4 ^^ Npos p2))
| Some (Npos p, e5) =>
match isIn e1 p e4 p2 with
| Some (n, e6) => Some (n, e5 ** e6)
| None => Some (Npos p, e5 ** (e4 ^^ Npos p2))
end
| None =>
match isIn e1 p1 e4 p2 with
| Some (n, e5) => Some (n, (e3 ^^ Npos p2) ** e5)
| None => None
end
end
| e3 ^ N0 => None
| e3 ^ Npos p3 => isIn e1 p1 e3 (Pos.mul p3 p2)
| _ => default_isIn e1 p1 e2 p2
end%poly.
Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end.
Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end.
Lemma Z_pos_sub_gt p q : (p > q)%positive ->
Z.pos_sub p q = Zpos (p - q).
intros; now apply Z.pos_sub_gt, Pos.gt_lt.
Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
Lemma default_isIn_ok e1 e2 p1 p2 :
match default_isIn e1 p1 e2 p2 with
| Some(n, e3) =>
let n' := ZtoN (Zpos p1 - NtoZ n) in
(e2 ^ N.pos p2 === e1 ^ n' * e3)%poly
/\ (Zpos p1 > NtoZ n)%Z
| _ => True
end.
case PExpr_eq_spec; trivial.
case Pos.compare_spec;intros H; split; try reflexivity.
now rewrite PE_1_r, H, EQ.
rewrite NPEpow_ok, EQ, <- PEpow_add_r.
now rewrite Pos.add_comm, Pos.sub_add.
rewrite Z.pos_sub_gt by now apply Pos.sub_decr.
rewrite Pos.sub_sub_distr, Pos.add_comm; trivial.
rewrite Pos.add_sub; trivial.
apply Pos.sub_decr; trivial.
now apply Z.lt_gt, Pos.sub_decr.
Ltac npe_simpl := rewrite ?NPEmul_ok, ?NPEpow_ok, ?PEpow_mul_l.
Ltac npe_ring := intro l; simpl; ring.
Theorem isIn_ok e1 p1 e2 p2 :
match isIn e1 p1 e2 p2 with
| Some(n, e3) =>
let n' := ZtoN (Zpos p1 - NtoZ n) in
(e2 ^ N.pos p2 === e1 ^ n' * e3)%poly
/\ (Zpos p1 > NtoZ n)%Z
| _ => True
end.
induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IHe2 n]; intros p1 p2;
try refine (default_isIn_ok e1 _ p1 p2); simpl isIn.
specialize (IHe2_1 p1 p2).
destruct isIn as [([|p],e)|].
destruct IHe2_1 as (IH,_).
specialize (IHe2_2 p p2).
destruct isIn as [([|p'],e')|].
destruct IHe2_1 as (IH1,GT1).
destruct IHe2_2 as (IH2,GT2).
split; [|simpl; apply Zgt_trans with (Z.pos p); trivial].
replace (N.pos p1) with (N.pos p + N.pos (p1 - p))%N.
rewrite PEpow_add_r; npe_ring.
rewrite Pos.add_comm, Pos.sub_add.
destruct IHe2_1 as (IH1,GT1).
destruct IHe2_2 as (IH2,GT2).
assert (Z.pos p1 > Z.pos p')%Z by (now apply Zgt_trans with (Zpos p)).
split; [|simpl; trivial].
replace (N.pos (p1 - p')) with (N.pos (p1 - p) + N.pos (p - p'))%N.
rewrite PEpow_add_r; npe_ring.
rewrite Pos.add_sub_assoc, Pos.sub_add; trivial.
destruct IHe2_1 as (IH,GT).
specialize (IHe2_2 p1 p2).
destruct isIn as [(n,e)|]; trivial.
destruct IHe2_2 as (IH,GT).
set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d.
destruct n as [|p]; trivial.
specialize (IHe2 p1 (p * p2)%positive).
destruct isIn as [(n,e)|]; trivial.
destruct IHe2 as (IH,GT).
set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d.
now rewrite <- PEpow_mul_r.
Record rsplit : Type := mk_rsplit {
rsplit_left : PExpr C;
rsplit_common : PExpr C;
rsplit_right : PExpr C}.
Notation left := rsplit_left.
Notation right := rsplit_right.
Notation common := rsplit_common.
Fixpoint split_aux e1 p e2 {struct e1}: rsplit :=
match e1 with
| e3 * e4 =>
let r1 := split_aux e3 p e2 in
let r2 := split_aux e4 p (right r1) in
mk_rsplit (left r1 ** left r2)
(common r1 ** common r2)
(right r2)
| e3 ^ N0 => mk_rsplit 1 1 e2
| e3 ^ Npos p3 => split_aux e3 (Pos.mul p3 p) e2
| _ =>
match isIn e1 p e2 1 with
| Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3
| Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3
| None => mk_rsplit (e1 ^^ Npos p) 1 e2
end
end%poly.
Lemma split_aux_ok1 e1 p e2 :
(let res := match isIn e1 p e2 1 with
| Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3
| Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3
| None => mk_rsplit (e1 ^^ Npos p) 1 e2
end
in
e1 ^ Npos p === left res * common res
/\ e2 === right res * common res)%poly.
unfold res;clear res; generalize (isIn_ok e1 p e2 xH).
destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl.
intros (H1,H2); split; npe_simpl.
intros (H1,H2); split; npe_simpl.
rewrite Pos.add_comm, Pos.sub_add; trivial.
intros _; split; npe_simpl; now rewrite PE_1_r.
Theorem split_aux_ok: forall e1 p e2,
(e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2)
/\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly.
intro e1;induction e1 as [| |?|?|? IHe1_1 ? IHe1_2|? IHe1_1 ? IHe1_2|e1_1 IHe1_1 ? IHe1_2|? IHe1|? IHe1 n];
intros k e2; try refine (split_aux_ok1 _ k e2);simpl.
destruct (IHe1_1 k e2) as (H1,H2).
destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4).
rewrite PEpow_0_r, PEpow_1_l, !PE_1_r.
Definition split e1 e2 := split_aux e1 xH e2.
Theorem split_ok_l e1 e2 :
(e1 === left (split e1 e2) * common (split e1 e2))%poly.
destruct (split_aux_ok e1 xH e2) as (H,_).
now rewrite <- H, PEpow_1_r.
Theorem split_ok_r e1 e2 :
(e2 === right (split e1 e2) * common (split e1 e2))%poly.
destruct (split_aux_ok e1 xH e2) as (_,H).
Lemma split_nz_l l e1 e2 :
~ e1 @ l == 0 -> ~ left (split e1 e2) @ l == 0.
rewrite (split_ok_l e1 e2); simpl.
Lemma split_nz_r l e1 e2 :
~ e2 @ l == 0 -> ~ right (split e1 e2) @ l == 0.
rewrite (split_ok_r e1 e2); simpl.
Fixpoint Fnorm (e : FExpr) : linear :=
match e with
| FEO => mk_linear 0 1 nil
| FEI => mk_linear 1 1 nil
| FEc c => mk_linear (PEc c) 1 nil
| FEX x => mk_linear (PEX C x) 1 nil
| FEadd e1 e2 =>
let x := Fnorm e1 in
let y := Fnorm e2 in
let s := split (denum x) (denum y) in
mk_linear
((num x ** right s) ++ (num y ** left s))
(left s ** (right s ** common s))
(condition x ++ condition y)%list
| FEsub e1 e2 =>
let x := Fnorm e1 in
let y := Fnorm e2 in
let s := split (denum x) (denum y) in
mk_linear
((num x ** right s) -- (num y ** left s))
(left s ** (right s ** common s))
(condition x ++ condition y)%list
| FEmul e1 e2 =>
let x := Fnorm e1 in
let y := Fnorm e2 in
let s1 := split (num x) (denum y) in
let s2 := split (num y) (denum x) in
mk_linear (left s1 ** left s2)
(right s2 ** right s1)
(condition x ++ condition y)%list
| FEopp e1 =>
let x := Fnorm e1 in
mk_linear (NPEopp (num x)) (denum x) (condition x)
| FEinv e1 =>
let x := Fnorm e1 in
mk_linear (denum x) (num x) (num x :: condition x)
| FEdiv e1 e2 =>
let x := Fnorm e1 in
let y := Fnorm e2 in
let s1 := split (num x) (num y) in
let s2 := split (denum x) (denum y) in
mk_linear (left s1 ** right s2)
(left s2 ** right s1)
(num y :: condition x ++ condition y)%list
| FEpow e1 n =>
let x := Fnorm e1 in
mk_linear ((num x)^^n) ((denum x)^^n) (condition x)
end.
(* Example *)
(*
Eval compute
in (Fnorm
(FEdiv
(FEc cI)
(FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))).
*)
Theorem Pcond_Fnorm l e :
PCond l (condition (Fnorm e)) -> ~ (denum (Fnorm e))@l == 0.
induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe|? IHe1 ? IHe2|? IHe n];
simpl condition; rewrite ?PCond_cons, ?PCond_app;
simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok.
rewrite phi_1; exact rI_neq_rO.
rewrite phi_1; exact rI_neq_rO.
rewrite phi_1; exact rI_neq_rO.
rewrite phi_1; exact rI_neq_rO.
apply field_is_integral_domain.
apply split_nz_l, IHe1, Hc1.
apply field_is_integral_domain.
apply split_nz_l, IHe1, Hc1.
apply field_is_integral_domain.
apply split_nz_r, IHe1, Hc1.
apply split_nz_r, IHe2, Hc2.
apply field_is_integral_domain.
apply split_nz_l, IHe1, Hc2.
(***************************************************************************
Main theorem
***************************************************************************)
Ltac uneval :=
repeat match goal with
| |- context [ ?x @ ?l * ?y @ ?l ] => change (x@l * y@l) with ((x*y)@l)
| |- context [ ?x @ ?l + ?y @ ?l ] => change (x@l + y@l) with ((x+y)@l)
end.
Theorem Fnorm_FEeval_PEeval l fe:
PCond l (condition (Fnorm fe)) ->
FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l.
induction fe as [| |?|?|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe IHfe|fe IHfe|fe1 IHfe1 fe2 IHfe2|fe IHfe n];
simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
intros (Hc1,Hc2) || intros Hc;
try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1);
try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2);
try set (F1 := Fnorm fe1) in *; try set (F2 := Fnorm fe2) in *.
now rewrite phi_1, phi_0, rdiv_def.
now rewrite phi_1; apply rdiv1.
rewrite phi_1; apply rdiv1.
rewrite phi_1; apply rdiv1.
rewrite NPEadd_ok, !NPEmul_ok.
rewrite <- rdiv2b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial.
rewrite NPEsub_ok, !NPEmul_ok.
rewrite <- rdiv3b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial.
rewrite (split_ok_l (num F1) (denum F2) l),
(split_ok_r (num F1) (denum F2) l),
(split_ok_l (num F2) (denum F1) l),
(split_ok_r (num F2) (denum F1) l) in *.
rewrite NPEopp_ok; simpl; rewrite (IHfe Hc); apply rdiv5.
rewrite (IHfe Hc2); apply rdiv6; trivial;
apply Pcond_Fnorm; trivial.
destruct Hc2 as (Hc2,Hc3).
assert (U1 := split_ok_l (num F1) (num F2) l).
assert (U2 := split_ok_r (num F1) (num F2) l).
assert (U3 := split_ok_l (denum F1) (denum F2) l).
assert (U4 := split_ok_r (denum F1) (denum F2) l).
rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4.
apply rdiv7b;
rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial.
rewrite !rpow_pow, (IHfe Hc).
apply Pcond_Fnorm; trivial.
Theorem Fnorm_crossproduct l fe1 fe2 :
let nfe1 := Fnorm fe1 in
let nfe2 := Fnorm fe2 in
(num nfe1 * denum nfe2) @ l == (num nfe2 * denum nfe1) @ l ->
PCond l (condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
intros Hcrossprod (Hc1,Hc2).
rewrite !Fnorm_FEeval_PEeval; trivial.
apply cross_product_eq; trivial;
apply Pcond_Fnorm; trivial.
(* Correctness lemmas of reflexive tactics *)
Notation Ninterp_PElist :=
(interp_PElist rO rI radd rmul rsub ropp req phi Cp_phi rpow).
Notation Nmk_monpol_list :=
(mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
Theorem Fnorm_ok:
forall n l lpe fe,
Ninterp_PElist l lpe ->
Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true ->
PCond l (condition (Fnorm fe)) -> FEeval l fe == 0.
intros n l lpe fe Hlpe H H1.
rewrite (Fnorm_FEeval_PEeval l fe H1).
apply Pcond_Fnorm; trivial.
transitivity (0@l); trivial.
rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe); trivial.
change (0 @ l) with (Pphi 0 radd rmul phi l (Pc cO)).
apply (Peq_ok Rsth Reqe CRmorph); trivial.
Notation ring_rw_correct :=
(ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
Notation ring_rw_pow_correct :=
(ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
Notation ring_correct :=
(ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th).
(* simplify a field expression into a fraction *)
Definition display_linear l num den :=
let lnum := NPphi_dev l num in
match den with
| Pc c => if ceqb c cI then lnum else lnum / NPphi_dev l den
| _ => lnum / NPphi_dev l den
end.
Definition display_pow_linear l num den :=
let lnum := NPphi_pow l num in
match den with
| Pc c => if ceqb c cI then lnum else lnum / NPphi_pow l den
| _ => lnum / NPphi_pow l den
end.
Theorem Field_rw_correct n lpe l :
Ninterp_PElist l lpe ->
forall lmp, Nmk_monpol_list lpe = lmp ->
forall fe nfe, Fnorm fe = nfe ->
PCond l (condition nfe) ->
FEeval l fe ==
display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
rewrite (Fnorm_FEeval_PEeval _ _ H).
destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
try ( apply rdiv_ext;
eapply ring_rw_correct; eauto).
destruct (ceqb_spec c cI) as [H0|].
set (nnum := NPphi_dev _ _).
apply eq_trans with (nnum / NPphi_dev l (Pc c)).
apply rdiv_ext;
eapply ring_rw_correct; eauto.
rewrite Pphi_dev_ok; try eassumption.
now simpl; rewrite H0, phi_1, <- rdiv1.
apply rdiv_ext;
eapply ring_rw_correct; eauto.
Theorem Field_rw_pow_correct n lpe l :
Ninterp_PElist l lpe ->
forall lmp, Nmk_monpol_list lpe = lmp ->
forall fe nfe, Fnorm fe = nfe ->
PCond l (condition nfe) ->
FEeval l fe ==
display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
rewrite (Fnorm_FEeval_PEeval _ _ H).
unfold display_pow_linear.
destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
try ( apply rdiv_ext;
eapply ring_rw_pow_correct; eauto).
destruct (ceqb_spec c cI) as [H0|].
set (nnum := NPphi_pow _ _).
apply eq_trans with (nnum / NPphi_pow l (Pc c)).
apply rdiv_ext;
eapply ring_rw_pow_correct; eauto.
rewrite Pphi_pow_ok; try eassumption.
now simpl; rewrite H0, phi_1, <- rdiv1.
apply rdiv_ext;
eapply ring_rw_pow_correct; eauto.
Theorem Field_correct n l lpe fe1 fe2 :
Ninterp_PElist l lpe ->
forall lmp, Nmk_monpol_list lpe = lmp ->
forall nfe1, Fnorm fe1 = nfe1 ->
forall nfe2, Fnorm fe2 = nfe2 ->
Peq ceqb (Nnorm n lmp (num nfe1 * denum nfe2))
(Nnorm n lmp (num nfe2 * denum nfe1)) = true ->
PCond l (condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
intros Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp.
apply Fnorm_crossproduct; trivial.
eapply ring_correct; eauto.
(* simplify a field equation : generate the crossproduct and simplify
polynomials *)
(** This allows rewriting modulo the simplification of PEeval on PMul *)
Declare Equivalent Keys PEeval rmul.
Theorem Field_simplify_eq_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp, Nmk_monpol_list lpe = lmp ->
forall nfe1, Fnorm fe1 = nfe1 ->
forall nfe2, Fnorm fe2 = nfe2 ->
forall den, split (denum nfe1) (denum nfe2) = den ->
NPphi_dev l (Nnorm n lmp (num nfe1 * right den)) ==
NPphi_dev l (Nnorm n lmp (num nfe2 * left den)) ->
PCond l (condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond.
apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial.
rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3.
rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
rewrite (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
(ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
Theorem Field_simplify_eq_pow_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp, Nmk_monpol_list lpe = lmp ->
forall nfe1, Fnorm fe1 = nfe1 ->
forall nfe2, Fnorm fe2 = nfe2 ->
forall den, split (denum nfe1) (denum nfe2) = den ->
NPphi_pow l (Nnorm n lmp (num nfe1 * right den)) ==
NPphi_pow l (Nnorm n lmp (num nfe2 * left den)) ->
PCond l (condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond.
apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial.
rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3.
rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
rewrite
(ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
(ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
Theorem Field_simplify_aux_ok l fe1 fe2 den :
FEeval l fe1 == FEeval l fe2 ->
split (denum (Fnorm fe1)) (denum (Fnorm fe2)) = den ->
PCond l (condition (Fnorm fe1) ++ condition (Fnorm fe2)) ->
(num (Fnorm fe1) * right den) @ l == (num (Fnorm fe2) * left den) @ l.
rewrite PCond_app; intros Hfe Hden (Hc1,Hc2); simpl.
assert (Hc1' := Pcond_Fnorm _ _ Hc1).
assert (Hc2' := Pcond_Fnorm _ _ Hc2).
set (N1 := num (Fnorm fe1)) in *.
set (N2 := num (Fnorm fe2)) in *.
set (D1 := denum (Fnorm fe1)) in *.
set (D2 := denum (Fnorm fe2)) in *.
assert (~ (common den) @ l == 0).
rewrite (split_ok_l D1 D2 l).
apply (@rmul_reg_l ((common den) @ l)); trivial.
rewrite !(rmul_comm ((common den) @ l)), <- !rmul_assoc.
change
(N1@l * (right den * common den) @ l ==
N2@l * (left den * common den) @ l).
rewrite <- Hden, <- split_ok_l, <- split_ok_r.
apply (@rmul_reg_l (/ D2@l)).
rewrite (rmul_comm (/ D2 @ l)), <- !rmul_assoc.
rewrite <- rdiv_def, rdiv_r_r, rmul_1_r by trivial.
apply (@rmul_reg_l (/ (D1@l))).
rewrite !(rmul_comm (/ D1@l)), <- !rmul_assoc.
rewrite <- !rdiv_def, rdiv_r_r, rmul_1_r by trivial.
rewrite (rmul_comm (/ D2@l)), <- rdiv_def.
unfold N1,N2,D1,D2; rewrite <- !Fnorm_FEeval_PEeval; trivial.
Theorem Field_simplify_eq_pow_in_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp, Nmk_monpol_list lpe = lmp ->
forall nfe1, Fnorm fe1 = nfe1 ->
forall nfe2, Fnorm fe2 = nfe2 ->
forall den, split (denum nfe1) (denum nfe2) = den ->
forall np1, Nnorm n lmp (num nfe1 * right den) = np1 ->
forall np2, Nnorm n lmp (num nfe2 * left den) = np2 ->
FEeval l fe1 == FEeval l fe2 ->
PCond l (condition nfe1 ++ condition nfe2) ->
NPphi_pow l np1 ==
NPphi_pow l np2.
intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?.
subst nfe1 nfe2 lmp np1 np2.
rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec).
repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial).
apply Field_simplify_aux_ok; trivial.
Theorem Field_simplify_eq_in_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp, Nmk_monpol_list lpe = lmp ->
forall nfe1, Fnorm fe1 = nfe1 ->
forall nfe2, Fnorm fe2 = nfe2 ->
forall den, split (denum nfe1) (denum nfe2) = den ->
forall np1, Nnorm n lmp (num nfe1 * right den) = np1 ->
forall np2, Nnorm n lmp (num nfe2 * left den) = np2 ->
FEeval l fe1 == FEeval l fe2 ->
PCond l (condition nfe1 ++ condition nfe2) ->
NPphi_dev l np1 == NPphi_dev l np2.
intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?.
subst nfe1 nfe2 lmp np1 np2.
rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec).
repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial).
apply Field_simplify_aux_ok; trivial.
Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C).
Hypothesis PCond_fcons_inv : forall l a l1,
PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1.
Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
match l with
| nil => m
| cons a l1 => Fcons a (Fapp l1 m)
end.
Lemma fcons_ok : forall l l1,
(forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
induction l1 as [|a l1 IHl1]; simpl; intros.
elim PCond_fcons_inv with (1 := H); intros.
(* Some general simpifications of the condition: eliminate duplicates,
split multiplications *)
Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
match l with
nil => cons e nil
| cons a l1 => if PExpr_eq e a then l else cons a (Fcons e l1)
end.
Theorem PFcons_fcons_inv:
forall l a l1, PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1.
intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons.
case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2);
repeat split; trivial.
(* equality of normal forms rather than syntactic equality *)
Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
match l with
nil => cons e nil
| cons a l1 =>
if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l
else cons a (Fcons0 e l1)
end.
Theorem PFcons0_fcons_inv:
forall l a l1, PCond l (Fcons0 a l1) -> ~ a @ l == 0 /\ PCond l l1.
intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons0.
generalize (ring_correct O l nil a e).
case Peq; intros H; rewrite !PCond_cons; intros (H1,H2);
repeat split; trivial.
(* split factorized denominators *)
Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
match e with
PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l)
| PEpow e1 _ => Fcons00 e1 l
| _ => Fcons0 e l
end.
Theorem PFcons00_fcons_inv:
forall l a l1, PCond l (Fcons00 a l1) -> ~ a @ l == 0 /\ PCond l l1.
intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
destruct (H _ H1) as (H2,H3).
destruct (H0 _ H3) as (H4,H5).
apply field_is_integral_domain; trivial.
Definition Pcond_simpl_gen :=
fcons_ok _ PFcons00_fcons_inv.
(* Specific case when the equality test of coefs is complete w.r.t. the
field equality: non-zero coefs can be eliminated, and opposite can
be simplified (if -1 <> 0) *)
Hypothesis ceqb_complete : forall c1 c2, [c1] == [c2] -> ceqb c1 c2 = true.
Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2).
assert (H := morph_eq CRmorph c1 c2).
assert (H' := @ceqb_complete c1 c2).
destruct (ceqb c1 c2); constructor.
Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
match e with
| PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l)
| PEpow e _ => Fcons1 e l
| PEopp e => if (-(1) =? 0)%coef then absurd_PCond else Fcons1 e l
| PEc c => if (c =? 0)%coef then absurd_PCond else l
| _ => Fcons0 e l
end.
Theorem PFcons1_fcons_inv:
forall l a l1, PCond l (Fcons1 a l1) -> ~ a @ l == 0 /\ PCond l l1.
intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
case ceqb_spec'; intros H H0.
elim (@absurd_PCond_bottom l H0).
rewrite <- phi_0; trivial.
destruct (H _ H1) as (H2,H3).
destruct (H0 _ H3) as (H4,H5).
apply field_is_integral_domain; trivial.
case ceqb_spec'; intros H0 H1.
elim (@absurd_PCond_bottom l H1).
apply ropp_neq_0; trivial.
rewrite (morph_opp CRmorph), phi_0, phi_1 in H0.
destruct (H _ H0);split;trivial.
Definition Fcons2 e l := Fcons1 (PEsimp e) l.
Theorem PFcons2_fcons_inv:
forall l a l1, PCond l (Fcons2 a l1) -> ~ a @ l == 0 /\ PCond l l1.
unfold Fcons2; intros l a l1 H; split;
case (PFcons1_fcons_inv l (PEsimp a) l1); trivial.
intros H1 H2 H3; case H1.
transitivity (a@l); trivial.
Definition Pcond_simpl_complete :=
fcons_ok _ PFcons2_fcons_inv.
Section FieldAndSemiField.
Record field_theory : Prop := mk_field {
F_R : ring_theory rO rI radd rmul rsub ropp req;
F_1_neq_0 : ~ 1 == 0;
Fdiv_def : forall p q, p / q == p * / q;
Finv_l : forall p, ~ p == 0 -> / p * p == 1
}.
Definition F2AF f :=
mk_afield
(Rth_ARth Rsth Reqe (F_R f)) (F_1_neq_0 f) (Fdiv_def f) (Finv_l f).
Record semi_field_theory : Prop := mk_sfield {
SF_SR : semi_ring_theory rO rI radd rmul req;
SF_1_neq_0 : ~ 1 == 0;
SFdiv_def : forall p q, p / q == p * / q;
SFinv_l : forall p, ~ p == 0 -> / p * p == 1
}.
Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth
(sf:semi_field_theory rO rI radd rmul rdiv rinv req) :=
mk_afield _ _
(SRth_ARth Rsth (SF_SR sf))
(SF_1_neq_0 sf)
(SFdiv_def sf)
(SFinv_l sf).
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable (rdiv : R -> R -> R) (rinv : R -> R).
Variable req : R -> R -> Prop.
Notation "x + y" := (radd x y).
Notation "x * y " := (rmul x y).
Notation "x - y " := (rsub x y).
Notation "- x" := (ropp x).
Notation "x / y " := (rdiv x y).
Notation "/ x" := (rinv x).
Notation "x == y" := (req x y) (at level 70, no associativity).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
transitivity proved by (@Equivalence_Transitive _ _ Rsth)
as R_setoid3.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
Add Morphism ropp with signature (req ==> req) as ropp_ext3.
Variable AFth : almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Let ARth := (AF_AR AFth).
Let rI_neq_rO := (AF_1_neq_0 AFth).
Let rdiv_def := (AFdiv_def AFth).
Let rinv_l := (AFinv_l AFth).
Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
Lemma add_inj_r p x y :
gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
elim p using Pos.peano_ind; simpl; [intros H|intros ? H ?].
rewrite !(ARadd_assoc ARth).
rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth); trivial.
Lemma gen_phiPOS_inj x y :
gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
x = y.
rewrite <- !(same_gen Rsth Reqe ARth).
case (Pos.compare_spec x y).
elim gen_phiPOS_not_0 with (y - x)%positive.
rewrite (ARadd_0_r Rsth ARth).
rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth).
now rewrite Pos.add_comm, Pos.sub_add.
elim gen_phiPOS_not_0 with (x - y)%positive.
rewrite (ARadd_0_r Rsth ARth).
rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth).
now rewrite Pos.add_comm, Pos.sub_add.
Lemma gen_phiN_inj x y :
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
x = y.
destruct x as [|p]; destruct y as [|p']; simpl; intros H; trivial.
elim gen_phiPOS_not_0 with p'.
rewrite (same_gen Rsth Reqe ARth); trivial.
elim gen_phiPOS_not_0 with p.
rewrite (same_gen Rsth Reqe ARth); trivial.
rewrite gen_phiPOS_inj with (1 := H); trivial.
Lemma gen_phiN_complete x y :
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
N.eqb x y = true.
now apply N.eqb_eq, gen_phiN_inj.
Variable Fth : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Let rI_neq_rO := (F_1_neq_0 Fth).
Let rdiv_def := (Fdiv_def Fth).
Let rinv_l := (Finv_l Fth).
Let AFth := F2AF Rsth Reqe Fth.
Let ARth := Rth_ARth Rsth Reqe Rth.
Lemma ring_S_inj x y : 1+x==1+y -> x==y.
rewrite <- (ARadd_0_l ARth x), <- (ARadd_0_l ARth y).
rewrite <- (Ropp_def Rth 1), (ARadd_comm ARth 1).
rewrite <- !(ARadd_assoc ARth).
now apply (Radd_ext Reqe).
Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
Let gen_phiPOS_inject :=
gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
Lemma gen_phiPOS_discr_sgn x y :
~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
apply gen_phiPOS_not_0 with (y + x)%positive.
rewrite (ARgen_phiPOS_add Rsth Reqe ARth).
transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y).
apply (Radd_ext Reqe); trivial.
rewrite (same_gen Rsth Reqe ARth).
rewrite (same_gen Rsth Reqe ARth).
Lemma gen_phiZ_inj x y :
gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
x = y.
destruct x as [|p|p]; destruct y as [|p'|p']; simpl; intros H.
elim gen_phiPOS_not_0 with p'.
rewrite (same_gen Rsth Reqe ARth).
elim gen_phiPOS_not_0 with p'.
rewrite (same_gen Rsth Reqe ARth).
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')).
apply (ARopp_zero Rsth Reqe ARth).
elim gen_phiPOS_not_0 with p.
rewrite (same_gen Rsth Reqe ARth).
rewrite gen_phiPOS_inject with (1 := H); trivial.
elim gen_phiPOS_discr_sgn with (1 := H).
elim gen_phiPOS_not_0 with p.
rewrite (same_gen Rsth Reqe ARth).
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
apply (ARopp_zero Rsth Reqe ARth).
elim gen_phiPOS_discr_sgn with p' p.
replace p' with p; trivial.
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')).
Lemma gen_phiZ_complete x y :
gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
Zeq_bool x y = true.
rewrite Z.compare_refl; trivial.
apply gen_phiZ_inj; trivial.