1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
10
Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List.
11
Require Import ZArith_base.
12
(*Require Import Omega.*)
13
Set Implicit Arguments.
19
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
20
Variable (rdiv : R -> R -> R) (rinv : R -> R).
21
Variable req : R -> R -> Prop.
23
Notation "0" := rO. Notation "1" := rI.
24
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
25
Notation "x - y " := (rsub x y). Notation "x / y" := (rdiv x y).
26
Notation "- x" := (ropp x). Notation "/ x" := (rinv x).
27
Notation "x == y" := (req x y) (at level 70, no associativity).
29
(* Equality properties *)
30
Variable Rsth : Setoid_Theory R req.
31
Variable Reqe : ring_eq_ext radd rmul ropp req.
32
Variable SRinv_ext : forall p q, p == q -> / p == / q.
34
(* Field properties *)
35
Record almost_field_theory : Prop := mk_afield {
36
AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req;
37
AF_1_neq_0 : ~ 1 == 0;
38
AFdiv_def : forall p q, p / q == p * / q;
39
AFinv_l : forall p, ~ p == 0 -> / p * p == 1
44
Variable AFth : almost_field_theory.
45
Let ARth := AFth.(AF_AR).
46
Let rI_neq_rO := AFth.(AF_1_neq_0).
47
Let rdiv_def := AFth.(AFdiv_def).
48
Let rinv_l := AFth.(AFinv_l).
52
Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
53
Variable ceqb : C->C->bool.
54
Variable phi : C -> R.
56
Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
57
cO cI cadd cmul csub copp ceqb phi.
59
Lemma ceqb_rect : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
60
(phi c1 == phi c2 -> P x) -> P y -> P (if ceqb c1 c2 then x else y).
63
generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
64
case (ceqb c1 c2); auto.
69
Notation "x +! y" := (cadd x y) (at level 50).
70
Notation "x *! y " := (cmul x y) (at level 40).
71
Notation "x -! y " := (csub x y) (at level 50).
72
Notation "-! x" := (copp x) (at level 35).
73
Notation " x ?=! y" := (ceqb x y) (at level 70, no associativity).
74
Notation "[ x ]" := (phi x) (at level 0).
78
Add Setoid R req Rsth as R_set1.
79
Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
80
Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
81
Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
82
Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
83
Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed.
85
Let eq_trans := Setoid.Seq_trans _ _ Rsth.
86
Let eq_sym := Setoid.Seq_sym _ _ Rsth.
87
Let eq_refl := Setoid.Seq_refl _ _ Rsth.
89
Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) .
90
Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe)
91
(ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext.
92
Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth)
93
(ARmul_1_l ARth) (ARmul_0_l ARth)
94
(ARmul_comm ARth) (ARmul_assoc ARth) (ARdistr_l ARth)
95
(ARopp_mul_l ARth) (ARopp_add ARth)
98
(* Power coefficients *)
100
Variable Cp_phi : N -> Cpow.
101
Variable rpow : R -> Cpow -> R.
102
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
104
Variable get_sign : C -> option C.
105
Variable get_sign_spec : sign_theory copp ceqb get_sign.
107
Variable cdiv:C -> C -> C*C.
108
Variable cdiv_th : div_theory req cadd cmul phi cdiv.
110
Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow).
111
Notation Nnorm:= (norm_subst cO cI cadd cmul csub copp ceqb cdiv).
113
Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign).
114
Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign).
116
(* add abstract semi-ring to help with some proofs *)
117
Add Ring Rring : (ARth_SRth ARth).
120
(* additional ring properties *)
122
Lemma rsub_0_l : forall r, 0 - r == - r.
123
intros; rewrite (ARsub_def ARth) in |- *;ring.
126
Lemma rsub_0_r : forall r, r - 0 == r.
127
intros; rewrite (ARsub_def ARth) in |- *.
128
rewrite (ARopp_zero Rsth Reqe ARth) in |- *; ring.
131
(***************************************************************************
133
Properties of division
135
***************************************************************************)
137
Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p.
139
rewrite rdiv_def in |- *.
140
transitivity (/ q * q * p); [ ring | idtac ].
141
rewrite rinv_l in |- *; auto.
143
Hint Resolve rdiv_simpl .
146
forall p1 p2, p1 == p2 -> forall q1 q2, q1 == q2 -> p1 / q1 == p2 / q2.
147
intros p1 p2 H q1 q2 H0.
148
transitivity (p1 * / q1); auto.
149
transitivity (p2 * / q2); auto.
151
Hint Resolve SRdiv_ext .
153
Add Morphism rdiv : rdiv_ext. exact SRdiv_ext. Qed.
155
Lemma rmul_reg_l : forall p q1 q2,
156
~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
158
rewrite <- (@rdiv_simpl q1 p) in |- *; trivial.
159
rewrite <- (@rdiv_simpl q2 p) in |- *; trivial.
160
repeat rewrite rdiv_def in |- *.
161
repeat rewrite (ARmul_assoc ARth) in |- *.
165
Theorem field_is_integral_domain : forall r1 r2,
166
~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0.
170
transitivity (1 * r2); auto.
171
transitivity (/ r1 * r1 * r2); auto.
172
rewrite <- (ARmul_assoc ARth) in |- *.
174
apply ARmul_0_r with (1 := Rsth) (2 := ARth).
177
Theorem ropp_neq_0 : forall r,
178
~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0.
180
setoid_replace (- r) with (- (1) * r).
181
apply field_is_integral_domain; trivial.
182
rewrite <- (ARopp_mul_l ARth) in |- *.
183
rewrite (ARmul_1_l ARth) in |- *.
187
Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1.
189
rewrite (AFdiv_def AFth) in |- *.
190
rewrite (ARmul_comm ARth) in |- *.
191
apply (AFinv_l AFth).
195
Theorem rdiv1: forall r, r == r / 1.
196
intros r; transitivity (1 * (r / 1)); auto.
203
r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4).
205
intros r1 r2 r3 r4 H H0.
206
assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
207
apply rmul_reg_l with (r2 * r4); trivial.
208
rewrite rdiv_simpl in |- *; trivial.
209
rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
210
apply (Radd_ext Reqe).
211
transitivity (r2 * (r1 / r2) * r4); [ ring | auto ].
212
transitivity (r2 * (r4 * (r3 / r4))); auto.
213
transitivity (r2 * r3); auto.
218
forall r1 r2 r3 r4 r5,
221
r1 / (r2*r5) + r3 / (r4*r5) == (r1 * r4 + r3 * r2) / (r2 * (r4 * r5)).
223
intros r1 r2 r3 r4 r5 H H0.
224
assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring).
225
assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring).
226
assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring).
227
assert (HH4: ~ r2 * (r4 * r5) == 0)
228
by complete (repeat apply field_is_integral_domain; trivial).
229
apply rmul_reg_l with (r2 * (r4 * r5)); trivial.
230
rewrite rdiv_simpl in |- *; trivial.
231
rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
232
apply (Radd_ext Reqe).
233
transitivity ((r2 * r5) * (r1 / (r2 * r5)) * r4); [ ring | auto ].
234
transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [ ring | auto ].
237
Theorem rdiv5: forall r1 r2, - (r1 / r2) == - r1 / r2.
239
transitivity (- (r1 * / r2)); auto.
240
transitivity (- r1 * / r2); auto.
248
r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4).
249
intros r1 r2 r3 r4 H H0.
250
assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
251
transitivity (r1 / r2 + - (r3 / r4)); auto.
252
transitivity (r1 / r2 + - r3 / r4); auto.
253
transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)); auto.
255
apply SRdiv_ext; auto.
256
transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
261
forall r1 r2 r3 r4 r5,
264
r1 / (r2*r5) - r3 / (r4*r5) == (r1 * r4 - r3 * r2) / (r2 * (r4 * r5)).
266
intros r1 r2 r3 r4 r5 H H0.
267
transitivity (r1 / (r2 * r5) + - (r3 / (r4 * r5))); auto.
268
transitivity (r1 / (r2 * r5) + - r3 / (r4 * r5)); auto.
269
transitivity ((r1 * r4 + - r3 * r2) / (r2 * (r4 * r5))).
270
apply rdiv2b; auto; try ring.
271
apply (SRdiv_ext); auto.
272
transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
277
~ r1 == 0 -> ~ r2 == 0 -> / (r1 / r2) == r2 / r1.
279
assert (~ r1 / r2 == 0) as Hk.
281
transitivity (r2 * (r1 / r2)); auto.
282
rewrite H1 in |- *; ring.
283
apply rmul_reg_l with (r1 / r2); auto.
284
transitivity (/ (r1 / r2) * (r1 / r2)); auto.
285
transitivity 1; auto.
286
repeat rewrite rdiv_def in |- *.
287
transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac | ring ].
288
repeat rewrite rinv_l in |- *; auto.
296
(r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4).
298
intros r1 r2 r3 r4 H H0.
299
assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
300
apply rmul_reg_l with (r2 * r4); trivial.
301
rewrite rdiv_simpl in |- *; trivial.
302
transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ].
303
repeat rewrite rdiv_simpl in |- *; trivial.
307
forall r1 r2 r3 r4 r5 r6,
310
((r1 * r6) / (r2 * r5)) * ((r3 * r5) / (r4 * r6)) == (r1 * r3) / (r2 * r4).
312
intros r1 r2 r3 r4 r5 r6 H H0.
314
transitivity ((r5 * r6) * (r1 * r3) / ((r5 * r6) * (r2 * r4))).
315
apply SRdiv_ext; ring.
316
assert (HH: ~ r5*r6 == 0).
317
apply field_is_integral_domain.
318
intros H1; case H; rewrite H1; ring.
319
intros H1; case H0; rewrite H1; ring.
320
rewrite <- rdiv4 ; auto.
321
rewrite rdiv_r_r; auto.
323
apply field_is_integral_domain.
324
intros H1; case H; rewrite H1; ring.
325
intros H1; case H0; rewrite H1; ring.
334
(r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3).
337
rewrite (rdiv_def (r1 / r2)) in |- *.
338
rewrite rdiv6 in |- *; trivial.
339
apply rdiv4; trivial.
343
forall r1 r2 r3 r4 r5 r6,
347
((r1 * r5) / (r2 * r6)) / ((r3 * r5) / (r4 * r6)) == (r1 * r4) / (r2 * r3).
351
transitivity ((r5 * r6) * (r1 * r4) / ((r5 * r6) * (r2 * r3))).
352
apply SRdiv_ext; ring.
353
assert (HH: ~ r5*r6 == 0).
354
apply field_is_integral_domain.
355
intros H2; case H0; rewrite H2; ring.
356
intros H2; case H1; rewrite H2; ring.
357
rewrite <- rdiv4 ; auto.
358
rewrite rdiv_r_r; auto.
359
apply field_is_integral_domain.
360
intros H2; case H; rewrite H2; ring.
361
intros H2; case H0; rewrite H2; ring.
365
Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 -> r1 / r2 == 0.
367
transitivity (r1 * / r2); auto.
368
transitivity (0 * / r2); auto.
372
Theorem cross_product_eq : forall r1 r2 r3 r4,
373
~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4.
375
transitivity (r1 / r2 * (r4 / r4)).
376
rewrite rdiv_r_r in |- *; trivial.
378
apply (ARmul_1_r Rsth ARth).
379
rewrite rdiv4 in |- *; trivial.
381
rewrite (ARmul_comm ARth r2 r4) in |- *.
382
rewrite <- rdiv4 in |- *; trivial.
383
rewrite rdiv_r_r in |- * by trivial.
384
apply (ARmul_1_r Rsth ARth).
387
(***************************************************************************
391
***************************************************************************)
393
Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool :=
396
| xO p3, xO p4 => positive_eq p3 p4
397
| xI p3, xI p4 => positive_eq p3 p4
401
Theorem positive_eq_correct:
402
forall p1 p2, if positive_eq p1 p2 then p1 = p2 else p1 <> p2.
404
(try (intros p2; case p2; simpl; auto; intros; discriminate)).
405
intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
406
generalize (rec p4); case (positive_eq p3 p4); auto.
407
intros H1; apply f_equal with ( f := xI ); auto.
408
intros H1 H2; case H1; injection H2; auto.
409
intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
410
generalize (rec p4); case (positive_eq p3 p4); auto.
411
intros H1; apply f_equal with ( f := xO ); auto.
412
intros H1 H2; case H1; injection H2; auto.
415
Definition N_eq n1 n2 :=
418
| Npos p1, Npos p2 => positive_eq p1 p2
422
Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2.
424
intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail).
425
assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2);
426
[rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial].
430
Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
432
PEc c1, PEc c2 => ceqb c1 c2
433
| PEX p1, PEX p2 => positive_eq p1 p2
434
| PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
435
| PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
436
| PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
437
| PEopp e3, PEopp e4 => PExpr_eq e3 e4
438
| PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false
442
Add Morphism (pow_pos rmul) : pow_morph.
443
intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH].
446
Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph.
447
intros x y H [|p];simpl;auto. apply pow_morph;trivial.
450
Lemma rpow_morph : forall x y n, x == y ->rpow x (Cp_phi n) == rpow y (Cp_phi n).
452
intros; repeat rewrite pow_th.(rpow_pow_N).
453
destruct n;simpl. apply eq_refl.
454
induction p;simpl;try rewrite IHp;try rewrite H; apply eq_refl.
457
Theorem PExpr_eq_semi_correct:
458
forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2.
459
intros l e1; elim e1.
460
intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)).
461
intros c2; apply (morph_eq CRmorph).
462
intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)).
463
intros p2; generalize (positive_eq_correct p1 p2); case (positive_eq p1 p2);
464
(try (intros; discriminate)); intros H; rewrite H; auto.
465
intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
466
intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
467
(try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
468
(try (intros; discriminate)); auto.
469
intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
470
intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
471
(try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
472
(try (intros; discriminate)); auto.
473
intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
474
intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
475
(try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
476
(try (intros; discriminate)); auto.
477
intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))).
478
intros e4; generalize (rec e4); case (PExpr_eq e3 e4);
479
(try (intros; discriminate)); auto.
480
intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))).
481
intros e4 n4;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4);
482
intros;try discriminate.
483
repeat rewrite pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto.
487
Definition NPEadd e1 e2 :=
489
PEc c1, PEc c2 => PEc (cadd c1 c2)
490
| PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2
491
| _, PEc c => if ceqb c cO then e1 else PEadd e1 e2
492
(* Peut t'on factoriser ici ??? *)
493
| _, _ => PEadd e1 e2
496
Theorem NPEadd_correct:
497
forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2).
500
destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
501
try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl;
502
try (ring [(morph0 CRmorph)]).
503
apply (morph_add CRmorph).
506
Definition NPEpow x n :=
510
if positive_eq p xH then x else
513
if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p)
518
Theorem NPEpow_correct : forall l e n,
519
NPEeval l (NPEpow e n) == NPEeval l (PEpow e n).
522
rewrite pow_th.(rpow_pow_N);simpl;auto.
523
generalize (positive_eq_correct p xH).
524
destruct (positive_eq p 1);intros.
525
rewrite H;rewrite pow_th.(rpow_pow_N). trivial.
526
clear H;destruct e;simpl;auto.
527
repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl.
528
symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)].
529
symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)].
530
induction p;simpl;auto;repeat rewrite CRmorph.(morph_mul);ring [IHp].
534
Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C :=
536
PEc c1, PEc c2 => PEc (cmul c1 c2)
538
if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y
540
if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y
541
| PEpow e1 n1, PEpow e2 n2 =>
542
if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
546
Lemma pow_pos_mul : forall x y p, pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p.
547
induction p;simpl;auto;try ring [IHp].
550
Theorem NPEmul_correct : forall l e1 e2,
551
NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2).
552
induction e1;destruct e2; simpl in |- *;try reflexivity;
553
repeat apply ceqb_rect;
554
try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity;
555
try ring [(morph0 CRmorph) (morph1 CRmorph)].
556
apply (morph_mul CRmorph).
557
assert (H:=N_eq_correct n n0);destruct (N_eq n n0).
558
rewrite NPEpow_correct. simpl.
559
repeat rewrite pow_th.(rpow_pow_N).
560
rewrite IHe1;rewrite <- H;destruct n;simpl;try ring.
566
Definition NPEsub e1 e2 :=
568
PEc c1, PEc c2 => PEc (csub c1 c2)
569
| PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2
570
| _, PEc c => if ceqb c cO then e1 else PEsub e1 e2
571
(* Peut-on factoriser ici *)
572
| _, _ => PEsub e1 e2
575
Theorem NPEsub_correct:
576
forall l e1 e2, NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2).
578
destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
579
try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;
580
try rewrite (morph0 CRmorph) in |- *; try reflexivity;
581
try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r).
582
apply (morph_sub CRmorph).
586
Definition NPEopp e1 :=
587
match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end.
589
Theorem NPEopp_correct:
590
forall l e1, NPEeval l (NPEopp e1) == NPEeval l (PEopp e1).
591
intros l e1; case e1; simpl; auto.
592
intros; apply (morph_opp CRmorph).
596
Fixpoint PExpr_simp (e : PExpr C) : PExpr C :=
598
PEadd e1 e2 => NPEadd (PExpr_simp e1) (PExpr_simp e2)
599
| PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2)
600
| PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2)
601
| PEopp e1 => NPEopp (PExpr_simp e1)
602
| PEpow e1 n1 => NPEpow (PExpr_simp e1) n1
606
Theorem PExpr_simp_correct:
607
forall l e, NPEeval l (PExpr_simp e) == NPEeval l e.
608
intros l e; elim e; simpl; auto.
609
intros e1 He1 e2 He2.
610
transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto.
611
apply NPEadd_correct.
613
intros e1 He1 e2 He2.
614
transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))); auto.
615
apply NPEsub_correct.
617
intros e1 He1 e2 He2.
618
transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto.
619
apply NPEmul_correct.
622
transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto.
623
apply NPEopp_correct.
625
intros e1 He1 n;simpl.
626
rewrite NPEpow_correct;simpl.
627
repeat rewrite pow_th.(rpow_pow_N).
632
(****************************************************************************
636
***************************************************************************)
638
(* The input: syntax of a field expression *)
640
Inductive FExpr : Type :=
642
| FEX: positive -> FExpr
643
| FEadd: FExpr -> FExpr -> FExpr
644
| FEsub: FExpr -> FExpr -> FExpr
645
| FEmul: FExpr -> FExpr -> FExpr
646
| FEopp: FExpr -> FExpr
647
| FEinv: FExpr -> FExpr
648
| FEdiv: FExpr -> FExpr -> FExpr
649
| FEpow: FExpr -> N -> FExpr .
651
Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
654
| FEX x => BinList.nth 0 x l
655
| FEadd x y => FEeval l x + FEeval l y
656
| FEsub x y => FEeval l x - FEeval l y
657
| FEmul x y => FEeval l x * FEeval l y
658
| FEopp x => - FEeval l x
659
| FEinv x => / FEeval l x
660
| FEdiv x y => FEeval l x / FEeval l y
661
| FEpow x n => rpow (FEeval l x) (Cp_phi n)
664
Strategy expand [FEeval].
666
(* The result of the normalisation *)
668
Record linear : Type := mk_linear {
671
condition : list (PExpr C) }.
673
(***************************************************************************
675
Semantics and properties of side condition
677
***************************************************************************)
679
Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop :=
682
| e1 :: nil => ~ req (NPEeval l e1) rO
683
| e1 :: l1 => ~ req (NPEeval l e1) rO /\ PCond l l1
686
Theorem PCond_cons_inv_l :
687
forall l a l1, PCond l (a::l1) -> ~ NPEeval l a == 0.
689
destruct l1; simpl in H |- *; trivial.
693
Theorem PCond_cons_inv_r : forall l a l1, PCond l (a :: l1) -> PCond l l1.
695
destruct l1; simpl in H |- *; trivial.
699
Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l1.
700
intros l l1 l2; elim l1; simpl app in |- *.
702
destruct l0; simpl in *.
703
destruct l2; firstorder.
707
Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l2.
708
intros l l1 l2; elim l1; simpl app; auto.
709
intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ).
712
(* An unsatisfiable condition: issued when a division by zero is detected *)
713
Definition absurd_PCond := cons (PEc cO) nil.
715
Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond.
716
unfold absurd_PCond in |- *; simpl in |- *.
719
apply (morph0 CRmorph).
722
(***************************************************************************
726
***************************************************************************)
728
Fixpoint isIn (e1:PExpr C) (p1:positive)
729
(e2:PExpr C) (p2:positive) {struct e2}: option (N * PExpr C) :=
732
match isIn e1 p1 e3 p2 with
733
| Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow e4 (Npos p2)))
734
| Some (Npos p, e5) =>
735
match isIn e1 p e4 p2 with
736
| Some (n, e6) => Some (n, NPEmul e5 e6)
737
| None => Some (Npos p, NPEmul e5 (NPEpow e4 (Npos p2)))
740
match isIn e1 p1 e4 p2 with
741
| Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5)
745
| PEpow e3 N0 => None
746
| PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pmult p3 p2)
748
if PExpr_eq e1 e2 then
749
match Zminus (Zpos p1) (Zpos p2) with
750
| Zpos p => Some (Npos p, PEc cI)
751
| Z0 => Some (N0, PEc cI)
752
| Zneg p => Some (N0, NPEpow e2 (Npos p))
757
Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end.
758
Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end.
760
Notation pow_pos_plus := (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext)
761
ARth.(ARmul_comm) ARth.(ARmul_assoc)).
763
Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
765
(if PExpr_eq e1 e2 then
766
match Zminus (Zpos p1) (Zpos p2) with
767
| Zpos p => Some (Npos p, PEc cI)
768
| Z0 => Some (N0, PEc cI)
769
| Zneg p => Some (N0, NPEpow e2 (Npos p))
774
NPEeval l (PEpow e2 (Npos p2)) ==
775
NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\
780
intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
781
case (PExpr_eq e1 e2); simpl; auto; intros H.
782
case_eq ((p1 ?= p2)%positive Eq);intros;simpl.
783
repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
784
rewrite (Pcompare_Eq_eq _ _ H0).
785
rewrite H by trivial. ring [ (morph1 CRmorph)].
786
fold (NPEpow e2 (Npos (p2 - p1))).
787
rewrite NPEpow_correct;simpl.
788
repeat rewrite pow_th.(rpow_pow_N);simpl.
789
rewrite H;trivial. split. 2:refine (refl_equal _).
790
rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial.
791
repeat rewrite pow_th.(rpow_pow_N);simpl.
794
match (p1 ?= p1 - p2)%positive Eq with
796
| Lt => Zneg (p1 - p2 - p1)
797
| Gt => Zpos (p1 - (p1 - p2))
798
end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))).
799
replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z.
801
repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth).
802
rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl.
803
ring [ (morph1 CRmorph)].
804
assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _).
805
apply Zplus_gt_reg_l with (Zpos p2).
806
rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z.
807
apply Zplus_gt_compat_r. refine (refl_equal _).
808
simpl;rewrite H0;trivial.
811
Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
812
induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_plus;simpl.
813
ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto.
817
Theorem isIn_correct: forall l e1 p1 e2 p2,
818
match isIn e1 p1 e2 p2 with
820
NPEeval l (PEpow e2 (Npos p2)) ==
821
NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\
827
intros l e1 p1 e2; generalize p1;clear p1;elim e2; intros;
828
try (refine (isIn_correct_aux l e1 _ p1 p2);fail);simpl isIn.
829
generalize (H p1 p2);clear H;destruct (isIn e1 p1 p p2). destruct p3.
831
simpl. rewrite NPEmul_correct. simpl; rewrite NPEpow_correct;simpl.
832
repeat rewrite pow_th.(rpow_pow_N);simpl.
833
rewrite pow_pos_mul;intros (H,H1);split;[ring[H]|trivial].
834
generalize (H0 p4 p2);clear H0;destruct (isIn e1 p4 p0 p2). destruct p5.
836
rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl.
837
intros (H1,H2) (H3,H4).
838
unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
839
rewrite pow_pos_mul. rewrite H1;rewrite H3.
840
assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
841
(pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
842
pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) *
843
NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H.
844
rewrite <- pow_pos_plus. rewrite Pplus_minus.
845
split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial.
846
repeat rewrite pow_th.(rpow_pow_N);simpl.
847
intros (H1,H2) (H3,H4).
848
unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
849
rewrite H2 in H1;simpl in H1.
850
assert (Zpos p1 > Zpos p6)%Z.
851
apply Zgt_trans with (Zpos p4). exact H4. exact H2.
852
unfold Zgt in H;simpl in H;rewrite H.
854
rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3.
855
assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
856
(pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) ==
857
pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) *
858
NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0.
859
rewrite <- pow_pos_plus.
860
replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive.
861
rewrite NPEmul_correct. simpl;ring.
863
(Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
864
change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
865
rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)).
866
simpl. rewrite Pcompare_refl. simpl. reflexivity.
867
unfold Zminus, Zopp in H0. simpl in H0.
868
rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
869
simpl. repeat rewrite pow_th.(rpow_pow_N).
870
intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3.
871
rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
872
simpl in H2. rewrite pow_th.(rpow_pow_N);simpl.
873
rewrite pow_pos_mul. split. ring [H2]. exact H3.
874
generalize (H0 p1 p2);clear H0;destruct (isIn e1 p1 p0 p2). destruct p3.
875
destruct n;simpl. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
876
repeat rewrite pow_th.(rpow_pow_N);simpl.
877
intros (H1,H2);split;trivial. rewrite pow_pos_mul;ring [H1].
878
rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
879
repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul.
880
intros (H1, H2);rewrite H1;split.
881
unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1.
882
simpl in H1;ring [H1]. trivial.
885
generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3.
886
destruct n;simpl. repeat rewrite pow_th.(rpow_pow_N). simpl.
887
intros (H1,H2);split. rewrite pow_pos_pow_pos. trivial. trivial.
888
repeat rewrite pow_th.(rpow_pow_N). simpl.
889
intros (H1,H2);split;trivial.
890
rewrite pow_pos_pow_pos;trivial.
894
Record rsplit : Type := mk_rsplit {
895
rsplit_left : PExpr C;
896
rsplit_common : PExpr C;
897
rsplit_right : PExpr C}.
899
(* Stupid name clash *)
900
Notation left := rsplit_left.
901
Notation right := rsplit_right.
902
Notation common := rsplit_common.
904
Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit :=
907
let r1 := split_aux e3 p e2 in
908
let r2 := split_aux e4 p (right r1) in
909
mk_rsplit (NPEmul (left r1) (left r2))
910
(NPEmul (common r1) (common r2))
912
| PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2
913
| PEpow e3 (Npos p3) => split_aux e3 (Pmult p3 p) e2
915
match isIn e1 p e2 xH with
916
| Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
917
| Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
918
| None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2
922
Lemma split_aux_correct_1 : forall l e1 p e2,
923
let res := match isIn e1 p e2 xH with
924
| Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
925
| Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
926
| None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2
928
NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res))
930
NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)).
932
intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH).
933
destruct (isIn e1 p e2 1). destruct p0.
934
Opaque NPEpow NPEmul.
936
(repeat rewrite NPEmul_correct;simpl;
937
repeat rewrite NPEpow_correct;simpl;
938
repeat rewrite pow_th.(rpow_pow_N);simpl).
939
intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
940
intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H.
941
simpl in H;split;try ring [H].
942
rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial.
943
simpl;intros. repeat rewrite NPEmul_correct;simpl.
944
rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
947
Theorem split_aux_correct: forall l e1 p e2,
948
NPEeval l (PEpow e1 (Npos p)) ==
949
NPEeval l (NPEmul (left (split_aux e1 p e2)) (common (split_aux e1 p e2)))
951
NPEeval l e2 == NPEeval l (NPEmul (right (split_aux e1 p e2))
952
(common (split_aux e1 p e2))).
954
intros l; induction e1;intros k e2; try refine (split_aux_correct_1 l _ k e2);simpl.
955
generalize (IHe1_1 k e2); clear IHe1_1.
956
generalize (IHe1_2 k (rsplit_right (split_aux e1_1 k e2))); clear IHe1_2.
957
simpl. repeat (rewrite NPEmul_correct;simpl).
958
repeat rewrite pow_th.(rpow_pow_N);simpl.
959
intros (H1,H2) (H3,H4);split.
960
rewrite pow_pos_mul. rewrite H1;rewrite H3. ring.
961
rewrite H4;rewrite H2;ring.
963
split. repeat rewrite pow_th.(rpow_pow_N);simpl.
964
rewrite NPEmul_correct. simpl.
965
induction k;simpl;try ring [CRmorph.(morph1)]; ring [IHk CRmorph.(morph1)].
966
rewrite NPEmul_correct;simpl. ring [CRmorph.(morph1)].
967
generalize (IHe1 (p*k)%positive e2);clear IHe1;simpl.
968
repeat rewrite NPEmul_correct;simpl.
969
repeat rewrite pow_th.(rpow_pow_N);simpl.
970
rewrite pow_pos_pow_pos. intros [H1 H2];split;ring [H1 H2].
973
Definition split e1 e2 := split_aux e1 xH e2.
975
Theorem split_correct_l: forall l e1 e2,
976
NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2))
977
(common (split e1 e2))).
979
intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl.
980
rewrite pow_th.(rpow_pow_N);simpl;auto.
983
Theorem split_correct_r: forall l e1 e2,
984
NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2))
985
(common (split e1 e2))).
987
intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto.
990
Fixpoint Fnorm (e : FExpr) : linear :=
992
| FEc c => mk_linear (PEc c) (PEc cI) nil
993
| FEX x => mk_linear (PEX C x) (PEc cI) nil
997
let s := split (denum x) (denum y) in
999
(NPEadd (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
1000
(NPEmul (left s) (NPEmul (right s) (common s)))
1001
(condition x ++ condition y)
1004
let x := Fnorm e1 in
1005
let y := Fnorm e2 in
1006
let s := split (denum x) (denum y) in
1008
(NPEsub (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
1009
(NPEmul (left s) (NPEmul (right s) (common s)))
1010
(condition x ++ condition y)
1012
let x := Fnorm e1 in
1013
let y := Fnorm e2 in
1014
let s1 := split (num x) (denum y) in
1015
let s2 := split (num y) (denum x) in
1016
mk_linear (NPEmul (left s1) (left s2))
1017
(NPEmul (right s2) (right s1))
1018
(condition x ++ condition y)
1020
let x := Fnorm e1 in
1021
mk_linear (NPEopp (num x)) (denum x) (condition x)
1023
let x := Fnorm e1 in
1024
mk_linear (denum x) (num x) (num x :: condition x)
1026
let x := Fnorm e1 in
1027
let y := Fnorm e2 in
1028
let s1 := split (num x) (num y) in
1029
let s2 := split (denum x) (denum y) in
1030
mk_linear (NPEmul (left s1) (right s2))
1031
(NPEmul (left s2) (right s1))
1032
(num y :: condition x ++ condition y)
1034
let x := Fnorm e1 in
1035
mk_linear (NPEpow (num x) n) (NPEpow (denum x) n) (condition x)
1045
(FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))).
1048
Lemma pow_pos_not_0 : forall x, ~x==0 -> forall p, ~pow_pos rmul x p == 0.
1051
intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
1053
rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp).
1055
rewrite H1. ring. rewrite Hp;ring.
1056
intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp).
1057
reflexivity. rewrite Hp;ring. trivial.
1060
Theorem Pcond_Fnorm:
1062
PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0.
1064
simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO.
1065
simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO.
1066
intros e1 Hrec1 e2 Hrec2 Hcond.
1067
simpl condition in Hcond.
1068
simpl denum in |- *.
1069
rewrite NPEmul_correct in |- *.
1071
apply field_is_integral_domain.
1072
intros HH; case Hrec1; auto.
1073
apply PCond_app_inv_l with (1 := Hcond).
1074
rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
1075
rewrite NPEmul_correct; simpl; rewrite HH; ring.
1076
intros HH; case Hrec2; auto.
1077
apply PCond_app_inv_r with (1 := Hcond).
1078
rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
1079
intros e1 Hrec1 e2 Hrec2 Hcond.
1080
simpl condition in Hcond.
1081
simpl denum in |- *.
1082
rewrite NPEmul_correct in |- *.
1084
apply field_is_integral_domain.
1085
intros HH; case Hrec1; auto.
1086
apply PCond_app_inv_l with (1 := Hcond).
1087
rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
1088
rewrite NPEmul_correct; simpl; rewrite HH; ring.
1089
intros HH; case Hrec2; auto.
1090
apply PCond_app_inv_r with (1 := Hcond).
1091
rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
1092
intros e1 Hrec1 e2 Hrec2 Hcond.
1093
simpl condition in Hcond.
1094
simpl denum in |- *.
1095
rewrite NPEmul_correct in |- *.
1097
apply field_is_integral_domain.
1098
intros HH; apply Hrec1.
1099
apply PCond_app_inv_l with (1 := Hcond).
1100
rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
1101
rewrite NPEmul_correct; simpl; rewrite HH; ring.
1102
intros HH; apply Hrec2.
1103
apply PCond_app_inv_r with (1 := Hcond).
1104
rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))).
1105
rewrite NPEmul_correct; simpl; rewrite HH; ring.
1106
intros e1 Hrec1 Hcond.
1107
simpl condition in Hcond.
1108
simpl denum in |- *.
1110
intros e1 Hrec1 Hcond.
1111
simpl condition in Hcond.
1112
simpl denum in |- *.
1113
apply PCond_cons_inv_l with (1:=Hcond).
1114
intros e1 Hrec1 e2 Hrec2 Hcond.
1115
simpl condition in Hcond.
1116
simpl denum in |- *.
1117
rewrite NPEmul_correct in |- *.
1119
apply field_is_integral_domain.
1120
intros HH; apply Hrec1.
1121
specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
1122
apply PCond_app_inv_l with (1 := Hcond1).
1123
rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
1124
rewrite NPEmul_correct; simpl; rewrite HH; ring.
1125
intros HH; apply PCond_cons_inv_l with (1:=Hcond).
1126
rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))).
1127
rewrite NPEmul_correct; simpl; rewrite HH; ring.
1128
simpl;intros e1 Hrec1 n Hcond.
1129
rewrite NPEpow_correct.
1130
simpl;rewrite pow_th.(rpow_pow_N).
1131
destruct n;simpl;intros.
1132
apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto.
1134
Hint Resolve Pcond_Fnorm.
1137
(***************************************************************************
1141
***************************************************************************)
1143
Theorem Fnorm_FEeval_PEeval:
1145
PCond l (condition (Fnorm fe)) ->
1146
FEeval l fe == NPEeval l (num (Fnorm fe)) / NPEeval l (denum (Fnorm fe)).
1148
intros l fe; elim fe; simpl.
1149
intros c H; rewrite CRmorph.(morph1); apply rdiv1.
1150
intros p H; rewrite CRmorph.(morph1); apply rdiv1.
1151
intros e1 He1 e2 He2 HH.
1152
assert (HH1: PCond l (condition (Fnorm e1))).
1153
apply PCond_app_inv_l with ( 1 := HH ).
1154
assert (HH2: PCond l (condition (Fnorm e2))).
1155
apply PCond_app_inv_r with ( 1 := HH ).
1156
rewrite (He1 HH1); rewrite (He2 HH2).
1157
rewrite NPEadd_correct; simpl.
1158
repeat rewrite NPEmul_correct; simpl.
1159
generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
1160
(split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
1161
repeat rewrite NPEmul_correct; simpl.
1162
intros U1 U2; rewrite U1; rewrite U2.
1164
rewrite <- U1; auto.
1165
rewrite <- U2; auto.
1167
intros e1 He1 e2 He2 HH.
1168
assert (HH1: PCond l (condition (Fnorm e1))).
1169
apply PCond_app_inv_l with ( 1 := HH ).
1170
assert (HH2: PCond l (condition (Fnorm e2))).
1171
apply PCond_app_inv_r with ( 1 := HH ).
1172
rewrite (He1 HH1); rewrite (He2 HH2).
1173
rewrite NPEsub_correct; simpl.
1174
repeat rewrite NPEmul_correct; simpl.
1175
generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
1176
(split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
1177
repeat rewrite NPEmul_correct; simpl.
1178
intros U1 U2; rewrite U1; rewrite U2.
1180
rewrite <- U1; auto.
1181
rewrite <- U2; auto.
1183
intros e1 He1 e2 He2 HH.
1184
assert (HH1: PCond l (condition (Fnorm e1))).
1185
apply PCond_app_inv_l with ( 1 := HH ).
1186
assert (HH2: PCond l (condition (Fnorm e2))).
1187
apply PCond_app_inv_r with ( 1 := HH ).
1188
rewrite (He1 HH1); rewrite (He2 HH2).
1189
repeat rewrite NPEmul_correct; simpl.
1190
generalize (split_correct_l l (num (Fnorm e1)) (denum (Fnorm e2)))
1191
(split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2)))
1192
(split_correct_l l (num (Fnorm e2)) (denum (Fnorm e1)))
1193
(split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
1194
repeat rewrite NPEmul_correct; simpl.
1195
intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
1198
rewrite <- U4; auto.
1199
rewrite <- U2; auto.
1202
rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto.
1205
assert (HH1: PCond l (condition (Fnorm e1))).
1206
apply PCond_cons_inv_r with ( 1 := HH ).
1207
rewrite (He1 HH1); apply rdiv6; auto.
1208
apply PCond_cons_inv_l with ( 1 := HH ).
1210
intros e1 He1 e2 He2 HH.
1211
assert (HH1: PCond l (condition (Fnorm e1))).
1212
apply PCond_app_inv_l with (condition (Fnorm e2)).
1213
apply PCond_cons_inv_r with ( 1 := HH ).
1214
assert (HH2: PCond l (condition (Fnorm e2))).
1215
apply PCond_app_inv_r with (condition (Fnorm e1)).
1216
apply PCond_cons_inv_r with ( 1 := HH ).
1217
rewrite (He1 HH1); rewrite (He2 HH2).
1218
repeat rewrite NPEmul_correct;simpl.
1219
generalize (split_correct_l l (num (Fnorm e1)) (num (Fnorm e2)))
1220
(split_correct_r l (num (Fnorm e1)) (num (Fnorm e2)))
1221
(split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
1222
(split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
1223
repeat rewrite NPEmul_correct; simpl.
1224
intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
1227
rewrite <- U3; auto.
1228
rewrite <- U2; auto.
1229
apply PCond_cons_inv_l with ( 1 := HH ).
1230
rewrite <- U4; auto.
1232
intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1.
1233
repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N).
1234
rewrite He1';clear He1'.
1235
destruct n;simpl. apply rdiv1.
1236
generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1)))
1237
(Pcond_Fnorm _ _ Hcond).
1238
intros r r0 Hdiff;induction p;simpl.
1239
repeat (rewrite <- rdiv4;trivial).
1240
rewrite IHp. reflexivity.
1241
apply pow_pos_not_0;trivial.
1242
apply pow_pos_not_0;trivial.
1243
intro Hp. apply (pow_pos_not_0 Hdiff p).
1244
rewrite (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p) 0).
1245
reflexivity. apply pow_pos_not_0;trivial. ring [Hp].
1246
rewrite <- rdiv4;trivial.
1247
rewrite IHp;reflexivity.
1248
apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
1252
Theorem Fnorm_crossproduct:
1254
let nfe1 := Fnorm fe1 in
1255
let nfe2 := Fnorm fe2 in
1256
NPEeval l (PEmul (num nfe1) (denum nfe2)) ==
1257
NPEeval l (PEmul (num nfe2) (denum nfe1)) ->
1258
PCond l (condition nfe1 ++ condition nfe2) ->
1259
FEeval l fe1 == FEeval l fe2.
1260
intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
1261
rewrite Fnorm_FEeval_PEeval in |- * by
1262
apply PCond_app_inv_l with (1 := Hcond).
1263
rewrite Fnorm_FEeval_PEeval in |- * by
1264
apply PCond_app_inv_r with (1 := Hcond).
1265
apply cross_product_eq; trivial.
1267
apply PCond_app_inv_l with (1 := Hcond).
1269
apply PCond_app_inv_r with (1 := Hcond).
1272
(* Correctness lemmas of reflexive tactics *)
1273
Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow).
1274
Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
1276
Theorem Fnorm_correct:
1278
Ninterp_PElist l lpe ->
1279
Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true ->
1280
PCond l (condition (Fnorm fe)) -> FEeval l fe == 0.
1281
intros n l lpe fe Hlpe H H1;
1282
apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1).
1284
transitivity (NPEeval l (PEc cO)); auto.
1285
rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe);auto.
1286
change (NPEeval l (PEc cO)) with (Pphi 0 radd rmul phi l (Pc cO)).
1287
apply (Peq_ok Rsth Reqe CRmorph);auto.
1288
simpl. apply (morph0 CRmorph); auto.
1291
(* simplify a field expression into a fraction *)
1292
(* TODO: simplify when den is constant... *)
1293
Definition display_linear l num den :=
1294
NPphi_dev l num / NPphi_dev l den.
1296
Definition display_pow_linear l num den :=
1297
NPphi_pow l num / NPphi_pow l den.
1299
Theorem Field_rw_correct :
1301
Ninterp_PElist l lpe ->
1302
forall lmp, Nmk_monpol_list lpe = lmp ->
1303
forall fe nfe, Fnorm fe = nfe ->
1304
PCond l (condition nfe) ->
1305
FEeval l fe == display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
1307
intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
1308
apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
1309
unfold display_linear; apply SRdiv_ext;
1310
eapply (ring_rw_correct Rsth Reqe ARth CRmorph);eauto.
1313
Theorem Field_rw_pow_correct :
1315
Ninterp_PElist l lpe ->
1316
forall lmp, Nmk_monpol_list lpe = lmp ->
1317
forall fe nfe, Fnorm fe = nfe ->
1318
PCond l (condition nfe) ->
1319
FEeval l fe == display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
1321
intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
1322
apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
1323
unfold display_pow_linear; apply SRdiv_ext;
1324
eapply (ring_rw_pow_correct Rsth Reqe ARth CRmorph);eauto.
1327
Theorem Field_correct :
1328
forall n l lpe fe1 fe2, Ninterp_PElist l lpe ->
1329
forall lmp, Nmk_monpol_list lpe = lmp ->
1330
forall nfe1, Fnorm fe1 = nfe1 ->
1331
forall nfe2, Fnorm fe2 = nfe2 ->
1332
Peq ceqb (Nnorm n lmp (PEmul (num nfe1) (denum nfe2)))
1333
(Nnorm n lmp (PEmul (num nfe2) (denum nfe1))) = true ->
1334
PCond l (condition nfe1 ++ condition nfe2) ->
1335
FEeval l fe1 == FEeval l fe2.
1337
intros n l lpe fe1 fe2 Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp.
1338
apply Fnorm_crossproduct; trivial.
1339
eapply (ring_correct Rsth Reqe ARth CRmorph); eauto.
1342
(* simplify a field equation : generate the crossproduct and simplify
1344
Theorem Field_simplify_eq_old_correct :
1345
forall l fe1 fe2 nfe1 nfe2,
1348
NPphi_dev l (Nnorm O nil (PEmul (num nfe1) (denum nfe2))) ==
1349
NPphi_dev l (Nnorm O nil (PEmul (num nfe2) (denum nfe1))) ->
1350
PCond l (condition nfe1 ++ condition nfe2) ->
1351
FEeval l fe1 == FEeval l fe2.
1353
intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2.
1354
apply Fnorm_crossproduct; trivial.
1356
[ |- NPEeval l ?x == NPEeval l ?y] =>
1357
rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
1358
O nil l I (refl_equal nil) x (refl_equal (Nnorm O nil x)));
1359
rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
1360
O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y)))
1365
Theorem Field_simplify_eq_correct :
1366
forall n l lpe fe1 fe2,
1367
Ninterp_PElist l lpe ->
1368
forall lmp, Nmk_monpol_list lpe = lmp ->
1369
forall nfe1, Fnorm fe1 = nfe1 ->
1370
forall nfe2, Fnorm fe2 = nfe2 ->
1371
forall den, split (denum nfe1) (denum nfe2) = den ->
1372
NPphi_dev l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
1373
NPphi_dev l (Nnorm n lmp (PEmul (num nfe2) (left den))) ->
1374
PCond l (condition nfe1 ++ condition nfe2) ->
1375
FEeval l fe1 == FEeval l fe2.
1377
intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
1378
subst nfe1 nfe2 den lmp.
1379
apply Fnorm_crossproduct; trivial.
1381
rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
1382
rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
1383
rewrite NPEmul_correct in |- *.
1384
rewrite NPEmul_correct in |- *.
1386
repeat rewrite (ARmul_assoc ARth) in |- *.
1388
let x := PEmul (num (Fnorm fe1))
1389
(rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
1390
ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
1391
Hlpe (refl_equal (Nmk_monpol_list lpe))
1392
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
1394
let x := (PEmul (num (Fnorm fe2))
1396
(split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
1397
ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
1398
Hlpe (refl_equal (Nmk_monpol_list lpe))
1399
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
1400
simpl in Hcrossprod.
1401
rewrite Hcrossprod in |- *.
1405
Theorem Field_simplify_eq_pow_correct :
1406
forall n l lpe fe1 fe2,
1407
Ninterp_PElist l lpe ->
1408
forall lmp, Nmk_monpol_list lpe = lmp ->
1409
forall nfe1, Fnorm fe1 = nfe1 ->
1410
forall nfe2, Fnorm fe2 = nfe2 ->
1411
forall den, split (denum nfe1) (denum nfe2) = den ->
1412
NPphi_pow l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
1413
NPphi_pow l (Nnorm n lmp (PEmul (num nfe2) (left den))) ->
1414
PCond l (condition nfe1 ++ condition nfe2) ->
1415
FEeval l fe1 == FEeval l fe2.
1417
intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
1418
subst nfe1 nfe2 den lmp.
1419
apply Fnorm_crossproduct; trivial.
1421
rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
1422
rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
1423
rewrite NPEmul_correct in |- *.
1424
rewrite NPEmul_correct in |- *.
1426
repeat rewrite (ARmul_assoc ARth) in |- *.
1428
let x := PEmul (num (Fnorm fe1))
1429
(rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
1430
ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
1431
Hlpe (refl_equal (Nmk_monpol_list lpe))
1432
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
1434
let x := (PEmul (num (Fnorm fe2))
1436
(split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
1437
ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
1438
Hlpe (refl_equal (Nmk_monpol_list lpe))
1439
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
1440
simpl in Hcrossprod.
1441
rewrite Hcrossprod in |- *.
1445
Theorem Field_simplify_eq_pow_in_correct :
1446
forall n l lpe fe1 fe2,
1447
Ninterp_PElist l lpe ->
1448
forall lmp, Nmk_monpol_list lpe = lmp ->
1449
forall nfe1, Fnorm fe1 = nfe1 ->
1450
forall nfe2, Fnorm fe2 = nfe2 ->
1451
forall den, split (denum nfe1) (denum nfe2) = den ->
1452
forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 ->
1453
forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 ->
1454
FEeval l fe1 == FEeval l fe2 ->
1455
PCond l (condition nfe1 ++ condition nfe2) ->
1459
intros. subst nfe1 nfe2 lmp np1 np2.
1460
repeat rewrite (Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec).
1461
repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl.
1462
assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)).
1463
assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)).
1464
apply (@rmul_reg_l (NPEeval l (rsplit_common den))).
1466
rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
1467
rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq].
1468
repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))).
1469
repeat rewrite <- ARth.(ARmul_assoc).
1470
change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with
1471
(NPEeval l (PEmul (rsplit_right den) (rsplit_common den))).
1472
change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with
1473
(NPEeval l (PEmul (rsplit_left den) (rsplit_common den))).
1474
repeat rewrite <- NPEmul_correct. rewrite <- H3. rewrite <- split_correct_l.
1475
rewrite <- split_correct_r.
1476
apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))).
1477
intro Heq; apply AFth.(AF_1_neq_0).
1478
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
1479
ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
1480
repeat rewrite <- (ARth.(ARmul_assoc)).
1481
rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
1482
apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
1483
intro Heq; apply AFth.(AF_1_neq_0).
1484
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
1485
ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))).
1486
repeat rewrite <- (ARth.(ARmul_assoc)).
1487
repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
1488
rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
1489
rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
1490
repeat rewrite <- (AFth.(AFdiv_def)).
1491
repeat rewrite <- Fnorm_FEeval_PEeval ; trivial.
1492
apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
1495
Theorem Field_simplify_eq_in_correct :
1496
forall n l lpe fe1 fe2,
1497
Ninterp_PElist l lpe ->
1498
forall lmp, Nmk_monpol_list lpe = lmp ->
1499
forall nfe1, Fnorm fe1 = nfe1 ->
1500
forall nfe2, Fnorm fe2 = nfe2 ->
1501
forall den, split (denum nfe1) (denum nfe2) = den ->
1502
forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 ->
1503
forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 ->
1504
FEeval l fe1 == FEeval l fe2 ->
1505
PCond l (condition nfe1 ++ condition nfe2) ->
1509
intros. subst nfe1 nfe2 lmp np1 np2.
1510
repeat rewrite (Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec).
1511
repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl.
1512
assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)).
1513
assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)).
1514
apply (@rmul_reg_l (NPEeval l (rsplit_common den))).
1516
rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
1517
rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq].
1518
repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))).
1519
repeat rewrite <- ARth.(ARmul_assoc).
1520
change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with
1521
(NPEeval l (PEmul (rsplit_right den) (rsplit_common den))).
1522
change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with
1523
(NPEeval l (PEmul (rsplit_left den) (rsplit_common den))).
1524
repeat rewrite <- NPEmul_correct;rewrite <- H3. rewrite <- split_correct_l.
1525
rewrite <- split_correct_r.
1526
apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))).
1527
intro Heq; apply AFth.(AF_1_neq_0).
1528
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
1529
ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
1530
repeat rewrite <- (ARth.(ARmul_assoc)).
1531
rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
1532
apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
1533
intro Heq; apply AFth.(AF_1_neq_0).
1534
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
1535
ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))).
1536
repeat rewrite <- (ARth.(ARmul_assoc)).
1537
repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
1538
rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
1539
rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
1540
repeat rewrite <- (AFth.(AFdiv_def)).
1541
repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
1542
apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
1548
Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C).
1550
Hypothesis PCond_fcons_inv : forall l a l1,
1551
PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
1553
Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
1556
| cons a l1 => Fcons a (Fapp l1 m)
1559
Lemma fcons_correct : forall l l1,
1560
PCond l (Fapp l1 nil) -> PCond l l1.
1561
induction l1; simpl in |- *; intros.
1563
elim PCond_fcons_inv with (1 := H); intros.
1569
Section Fcons_simpl.
1571
(* Some general simpifications of the condition: eliminate duplicates,
1572
split multiplications *)
1574
Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
1577
| cons a l1 => if PExpr_eq e a then l else cons a (Fcons e l1)
1580
Theorem PFcons_fcons_inv:
1581
forall l a l1, PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
1582
intros l a l1; elim l1; simpl Fcons; auto.
1585
generalize (PExpr_eq_semi_correct l a a0); case (PExpr_eq a a0).
1586
intros H H0 H1; split; auto.
1588
generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
1590
assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
1592
generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
1594
generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
1595
generalize Hp; case l0; simpl; intuition.
1598
(* equality of normal forms rather than syntactic equality *)
1599
Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
1603
if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l else cons a (Fcons0 e l1)
1606
Theorem PFcons0_fcons_inv:
1607
forall l a l1, PCond l (Fcons0 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
1608
intros l a l1; elim l1; simpl Fcons0; auto.
1611
generalize (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th O l nil a a0). simpl.
1612
case (Peq ceqb (Nnorm O nil a) (Nnorm O nil a0)).
1613
intros H H0 H1; split; auto.
1615
generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
1617
assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
1619
generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
1621
generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
1622
clear get_sign get_sign_spec.
1623
generalize Hp; case l0; simpl; intuition.
1626
Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
1628
PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l)
1629
| PEpow e1 _ => Fcons00 e1 l
1633
Theorem PFcons00_fcons_inv:
1634
forall l a l1, PCond l (Fcons00 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
1635
intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
1636
intros p H p0 H0 l1 H1.
1638
case (H _ H1); intros H2 H3.
1639
case (H0 _ H3); intros H4 H5; split; auto.
1641
apply field_is_integral_domain; trivial.
1642
simpl;intros. rewrite pow_th.(rpow_pow_N).
1643
destruct (H _ H0);split;auto.
1644
destruct n;simpl. apply AFth.(AF_1_neq_0).
1645
apply pow_pos_not_0;trivial.
1648
Definition Pcond_simpl_gen :=
1649
fcons_correct _ PFcons00_fcons_inv.
1652
(* Specific case when the equality test of coefs is complete w.r.t. the
1653
field equality: non-zero coefs can be eliminated, and opposite can
1654
be simplified (if -1 <> 0) *)
1656
Hypothesis ceqb_complete : forall c1 c2, phi c1 == phi c2 -> ceqb c1 c2 = true.
1658
Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
1659
(phi c1 == phi c2 -> P x) ->
1660
(~ phi c1 == phi c2 -> P y) ->
1661
P (if ceqb c1 c2 then x else y).
1664
generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
1665
generalize (@ceqb_complete c1 c2).
1666
case (c1 ?=! c2); auto; intros.
1669
absurd (false = true); auto; discriminate.
1672
Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
1674
PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l)
1675
| PEpow e _ => Fcons1 e l
1676
| PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l
1677
| PEc c => if ceqb c cO then absurd_PCond else l
1681
Theorem PFcons1_fcons_inv:
1682
forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
1683
intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
1684
simpl in |- *; intros c l1.
1685
apply ceqb_rect_complete; intros.
1686
elim (@absurd_PCond_bottom l H0).
1688
rewrite <- (morph0 CRmorph) in |- *; trivial.
1689
intros p H p0 H0 l1 H1.
1691
case (H _ H1); intros H2 H3.
1692
case (H0 _ H3); intros H4 H5; split; auto.
1694
apply field_is_integral_domain; trivial.
1695
simpl in |- *; intros p H l1.
1696
apply ceqb_rect_complete; intros.
1697
elim (@absurd_PCond_bottom l H1).
1700
apply ropp_neq_0; trivial.
1701
rewrite (morph_opp CRmorph) in H0.
1702
rewrite (morph1 CRmorph) in H0.
1703
rewrite (morph0 CRmorph) in H0.
1705
intros;simpl. destruct (H _ H0);split;trivial.
1706
rewrite pow_th.(rpow_pow_N). destruct n;simpl.
1707
apply AFth.(AF_1_neq_0). apply pow_pos_not_0;trivial.
1710
Definition Fcons2 e l := Fcons1 (PExpr_simp e) l.
1712
Theorem PFcons2_fcons_inv:
1713
forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
1714
unfold Fcons2 in |- *; intros l a l1 H; split;
1715
case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto.
1716
intros H1 H2 H3; case H1.
1717
transitivity (NPEeval l a); trivial.
1718
apply PExpr_simp_correct.
1721
Definition Pcond_simpl_complete :=
1722
fcons_correct _ PFcons2_fcons_inv.
1728
Section FieldAndSemiField.
1730
Record field_theory : Prop := mk_field {
1731
F_R : ring_theory rO rI radd rmul rsub ropp req;
1732
F_1_neq_0 : ~ 1 == 0;
1733
Fdiv_def : forall p q, p / q == p * / q;
1734
Finv_l : forall p, ~ p == 0 -> / p * p == 1
1737
Definition F2AF f :=
1739
(Rth_ARth Rsth Reqe f.(F_R)) f.(F_1_neq_0) f.(Fdiv_def) f.(Finv_l).
1741
Record semi_field_theory : Prop := mk_sfield {
1742
SF_SR : semi_ring_theory rO rI radd rmul req;
1743
SF_1_neq_0 : ~ 1 == 0;
1744
SFdiv_def : forall p q, p / q == p * / q;
1745
SFinv_l : forall p, ~ p == 0 -> / p * p == 1
1748
End FieldAndSemiField.
1752
Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth
1753
(sf:semi_field_theory rO rI radd rmul rdiv rinv req) :=
1755
(SRth_ARth Rsth sf.(SF_SR))
1763
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
1764
Variable (rdiv : R -> R -> R) (rinv : R -> R).
1765
Variable req : R -> R -> Prop.
1766
Notation "0" := rO. Notation "1" := rI.
1767
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
1768
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
1769
Notation "x / y " := (rdiv x y). Notation "/ x" := (rinv x).
1770
Notation "x == y" := (req x y) (at level 70, no associativity).
1771
Variable Rsth : Setoid_Theory R req.
1772
Add Setoid R req Rsth as R_setoid3.
1773
Variable Reqe : ring_eq_ext radd rmul ropp req.
1774
Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed.
1775
Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed.
1776
Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed.
1778
Section AlmostField.
1780
Variable AFth : almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req.
1781
Let ARth := AFth.(AF_AR).
1782
Let rI_neq_rO := AFth.(AF_1_neq_0).
1783
Let rdiv_def := AFth.(AFdiv_def).
1784
Let rinv_l := AFth.(AFinv_l).
1786
Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
1788
Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
1790
Lemma add_inj_r : forall p x y,
1791
gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
1793
elim p using Pind; simpl in |- *; intros.
1794
apply S_inj; trivial.
1797
repeat rewrite (ARadd_assoc ARth) in |- *.
1798
rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial.
1801
Lemma gen_phiPOS_inj : forall x y,
1802
gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
1805
repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *.
1806
ElimPcompare x y; intro.
1808
apply Pcompare_Eq_eq; trivial.
1810
elim gen_phiPOS_not_0 with (y - x)%positive.
1811
apply add_inj_r with x.
1813
rewrite (ARadd_0_r Rsth ARth) in |- *.
1814
rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
1815
rewrite Pplus_minus in |- *; trivial.
1816
change Eq with (CompOpp Eq) in |- *.
1817
rewrite <- Pcompare_antisym in |- *; trivial.
1818
rewrite H in |- *; trivial.
1820
elim gen_phiPOS_not_0 with (x - y)%positive.
1821
apply add_inj_r with y.
1822
rewrite (ARadd_0_r Rsth ARth) in |- *.
1823
rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
1824
rewrite Pplus_minus in |- *; trivial.
1828
Lemma gen_phiN_inj : forall x y,
1829
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
1831
destruct x; destruct y; simpl in |- *; intros; trivial.
1832
elim gen_phiPOS_not_0 with p.
1834
rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
1835
elim gen_phiPOS_not_0 with p.
1836
rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
1837
rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial.
1840
Lemma gen_phiN_complete : forall x y,
1841
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
1842
Neq_bool x y = true.
1845
unfold Neq_bool in |- *.
1846
rewrite Ncompare_refl in |- *; trivial.
1847
apply gen_phiN_inj; trivial.
1854
Variable Fth : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
1855
Let Rth := Fth.(F_R).
1856
Let rI_neq_rO := Fth.(F_1_neq_0).
1857
Let rdiv_def := Fth.(Fdiv_def).
1858
Let rinv_l := Fth.(Finv_l).
1859
Let AFth := F2AF Rsth Reqe Fth.
1860
Let ARth := Rth_ARth Rsth Reqe Rth.
1862
Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y.
1864
transitivity (x + (1 + - (1))).
1865
rewrite (Ropp_def Rth) in |- *.
1867
apply (ARadd_0_r Rsth ARth).
1868
transitivity (y + (1 + - (1))).
1869
repeat rewrite <- (ARplus_assoc ARth) in |- *.
1870
repeat rewrite (ARadd_assoc ARth) in |- *.
1871
apply (Radd_ext Reqe).
1872
repeat rewrite <- (ARadd_comm ARth 1) in |- *.
1875
rewrite (Ropp_def Rth) in |- *.
1876
apply (ARadd_0_r Rsth ARth).
1880
Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
1882
Let gen_phiPOS_inject :=
1883
gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
1885
Lemma gen_phiPOS_discr_sgn : forall x y,
1886
~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
1887
red in |- *; intros.
1888
apply gen_phiPOS_not_0 with (y + x)%positive.
1889
rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
1890
transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y).
1891
apply (Radd_ext Reqe); trivial.
1893
rewrite (same_gen Rsth Reqe ARth) in |- *.
1894
rewrite (same_gen Rsth Reqe ARth) in |- *.
1896
apply (Ropp_def Rth).
1899
Lemma gen_phiZ_inj : forall x y,
1900
gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
1902
destruct x; destruct y; simpl in |- *; intros.
1904
elim gen_phiPOS_not_0 with p.
1905
rewrite (same_gen Rsth Reqe ARth) in |- *.
1906
symmetry in |- *; trivial.
1907
elim gen_phiPOS_not_0 with p.
1908
rewrite (same_gen Rsth Reqe ARth) in |- *.
1909
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
1910
rewrite <- H in |- *.
1911
apply (ARopp_zero Rsth Reqe ARth).
1912
elim gen_phiPOS_not_0 with p.
1913
rewrite (same_gen Rsth Reqe ARth) in |- *.
1915
rewrite gen_phiPOS_inject with (1 := H) in |- *; trivial.
1916
elim gen_phiPOS_discr_sgn with (1 := H).
1917
elim gen_phiPOS_not_0 with p.
1918
rewrite (same_gen Rsth Reqe ARth) in |- *.
1919
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
1921
apply (ARopp_zero Rsth Reqe ARth).
1922
elim gen_phiPOS_discr_sgn with p0 p.
1923
symmetry in |- *; trivial.
1924
replace p0 with p; trivial.
1925
apply gen_phiPOS_inject.
1926
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
1927
rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *.
1928
rewrite H in |- *; trivial.
1932
Lemma gen_phiZ_complete : forall x y,
1933
gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
1934
Zeq_bool x y = true.
1937
unfold Zeq_bool in |- *.
1938
rewrite Zcompare_refl in |- *; trivial.
1939
apply gen_phiZ_inj; trivial.
added
removed
contrib/setoid_ring/Field_theory.v
