← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/field/LegacyField_Theory.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/field/LegacyField_Theory.v
 
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
(************************************************************************)
 
8
 
 
9
(* $Id: LegacyField_Theory.v 9288 2006-10-26 18:25:06Z herbelin $ *)
 
10
 
 
11
Require Import List.
 
12
Require Import Peano_dec.
 
13
Require Import LegacyRing.
 
14
Require Import LegacyField_Compl.
 
15
 
 
16
Record Field_Theory : Type := 
 
17
  {A : Type;
 
18
   Aplus : A -> A -> A;
 
19
   Amult : A -> A -> A;
 
20
   Aone : A;
 
21
   Azero : A;
 
22
   Aopp : A -> A;
 
23
   Aeq : A -> A -> bool;
 
24
   Ainv : A -> A;
 
25
   Aminus : option (A -> A -> A);
 
26
   Adiv : option (A -> A -> A);
 
27
   RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq;
 
28
   Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}.
 
29
 
 
30
(* The reflexion structure *)
 
31
Inductive ExprA : Set :=
 
32
  | EAzero : ExprA
 
33
  | EAone : ExprA
 
34
  | EAplus : ExprA -> ExprA -> ExprA
 
35
  | EAmult : ExprA -> ExprA -> ExprA
 
36
  | EAopp : ExprA -> ExprA
 
37
  | EAinv : ExprA -> ExprA
 
38
  | EAvar : nat -> ExprA.
 
39
 
 
40
(**** Decidability of equality ****)
 
41
 
 
42
Lemma eqExprA_O : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}.
 
43
Proof.
 
44
  double induction e1 e2; try intros;
 
45
   try (left; reflexivity) || (try (right; discriminate)).
 
46
  elim (H1 e0); intro y; elim (H2 e); intro y0;
 
47
   try
 
48
    (left; rewrite y; rewrite y0; auto) ||
 
49
      (right; red in |- *; intro; inversion H3; auto).
 
50
  elim (H1 e0); intro y; elim (H2 e); intro y0;
 
51
   try
 
52
    (left; rewrite y; rewrite y0; auto) ||
 
53
      (right; red in |- *; intro; inversion H3; auto).
 
54
  elim (H0 e); intro y.
 
55
  left; rewrite y; auto.
 
56
  right; red in |- *; intro; inversion H1; auto.
 
57
  elim (H0 e); intro y.
 
58
  left; rewrite y; auto.
 
59
  right; red in |- *; intro; inversion H1; auto.
 
60
  elim (eq_nat_dec n n0); intro y.
 
61
  left; rewrite y; auto.
 
62
  right; red in |- *; intro; inversion H; auto. 
 
63
Defined.
 
64
 
 
65
Definition eq_nat_dec := Eval compute in eq_nat_dec.
 
66
Definition eqExprA := Eval compute in eqExprA_O.
 
67
 
 
68
(**** Generation of the multiplier ****)
 
69
 
 
70
Fixpoint mult_of_list (e:list ExprA) : ExprA :=
 
71
  match e with
 
72
  | nil => EAone
 
73
  | e1 :: l1 => EAmult e1 (mult_of_list l1)
 
74
  end.
 
75
 
 
76
Section Theory_of_fields.
 
77
 
 
78
Variable T : Field_Theory.
 
79
 
 
80
Let AT := A T.
 
81
Let AplusT := Aplus T.
 
82
Let AmultT := Amult T.
 
83
Let AoneT := Aone T.
 
84
Let AzeroT := Azero T.
 
85
Let AoppT := Aopp T.
 
86
Let AeqT := Aeq T.
 
87
Let AinvT := Ainv T.
 
88
Let RTT := RT T.
 
89
Let Th_inv_defT := Th_inv_def T.
 
90
 
 
91
Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (
 
92
 Azero T) (Aopp T) (Aeq T) (RT T).
 
93
 
 
94
Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
 
95
 
 
96
(***************************)
 
97
(*    Lemmas to be used    *)
 
98
(***************************)
 
99
 
 
100
Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.
 
101
Proof.
 
102
  intros; legacy ring.
 
103
Qed.
 
104
 
 
105
Lemma AplusT_assoc :
 
106
 forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).
 
107
Proof.
 
108
  intros; legacy ring.
 
109
Qed.
 
110
 
 
111
Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
 
112
Proof.
 
113
  intros; legacy ring.
 
114
Qed.
 
115
 
 
116
Lemma AmultT_assoc :
 
117
 forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).
 
118
Proof.
 
119
  intros; legacy ring.
 
120
Qed.
 
121
 
 
122
Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.
 
123
Proof.
 
124
  intros; legacy ring.
 
125
Qed.
 
126
 
 
127
Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.
 
128
Proof.
 
129
  intros; legacy ring.
 
130
Qed.
 
131
 
 
132
Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.
 
133
Proof.
 
134
  intros; legacy ring.
 
135
Qed.
 
136
 
 
137
Lemma AmultT_AplusT_distr :
 
138
 forall r1 r2 r3:AT,
 
139
   AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3).
 
140
Proof.
 
141
  intros; legacy ring.
 
142
Qed.
 
143
 
 
144
Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2.
 
145
Proof.
 
146
  intros; transitivity (AplusT (AplusT (AoppT r) r) r1).
 
147
  legacy ring.
 
148
  transitivity (AplusT (AplusT (AoppT r) r) r2).
 
149
  repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
 
150
  legacy ring.
 
151
Qed.
 
152
 
 
153
Lemma r_AmultT_mult :
 
154
 forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2.
 
155
Proof.
 
156
  intros; transitivity (AmultT (AmultT (AinvT r) r) r1).
 
157
  rewrite Th_inv_defT; [ symmetry  in |- *; apply AmultT_1l; auto | auto ].
 
158
  transitivity (AmultT (AmultT (AinvT r) r) r2).
 
159
  repeat rewrite AmultT_assoc; rewrite H; trivial.
 
160
  rewrite Th_inv_defT; [ apply AmultT_1l; auto | auto ].
 
161
Qed.
 
162
 
 
163
Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
 
164
Proof.
 
165
  intro; legacy ring.
 
166
Qed.
 
167
 
 
168
Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
 
169
Proof.
 
170
  intro; legacy ring.
 
171
Qed.
 
172
 
 
173
Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
 
174
Proof.
 
175
  intro; legacy ring.
 
176
Qed.
 
177
 
 
178
Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.
 
179
Proof.
 
180
  intros; rewrite AmultT_comm; apply Th_inv_defT; auto.
 
181
Qed.
 
182
 
 
183
Lemma Rmult_neq_0_reg :
 
184
 forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT.
 
185
Proof.
 
186
  intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; legacy ring.
 
187
Qed.
 
188
 
 
189
(************************)
 
190
(*    Interpretation    *)
 
191
(************************)
 
192
 
 
193
(**** ExprA --> A ****)
 
194
 
 
195
Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
 
196
 AT :=
 
197
  match e with
 
198
  | EAzero => AzeroT
 
199
  | EAone => AoneT
 
200
  | EAplus e1 e2 => AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
 
201
  | EAmult e1 e2 => AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
 
202
  | EAopp e => Aopp T (interp_ExprA lvar e)
 
203
  | EAinv e => Ainv T (interp_ExprA lvar e)
 
204
  | EAvar n => assoc_2nd AT nat eq_nat_dec lvar n AzeroT
 
205
  end.
 
206
 
 
207
(************************)
 
208
(*    Simplification    *)
 
209
(************************)
 
210
 
 
211
(**** Associativity ****)
 
212
 
 
213
Definition merge_mult :=
 
214
  (fix merge_mult (e1:ExprA) : ExprA -> ExprA :=
 
215
     fun e2:ExprA =>
 
216
       match e1 with
 
217
       | EAmult t1 t2 =>
 
218
           match t2 with
 
219
           | EAmult t2 t3 => EAmult t1 (EAmult t2 (merge_mult t3 e2))
 
220
           | _ => EAmult t1 (EAmult t2 e2)
 
221
           end
 
222
       | _ => EAmult e1 e2
 
223
       end).
 
224
 
 
225
Fixpoint assoc_mult (e:ExprA) : ExprA :=
 
226
  match e with
 
227
  | EAmult e1 e3 =>
 
228
      match e1 with
 
229
      | EAmult e1 e2 =>
 
230
          merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2))
 
231
            (assoc_mult e3)
 
232
      | _ => EAmult e1 (assoc_mult e3)
 
233
      end
 
234
  | _ => e
 
235
  end.
 
236
 
 
237
Definition merge_plus :=
 
238
  (fix merge_plus (e1:ExprA) : ExprA -> ExprA :=
 
239
     fun e2:ExprA =>
 
240
       match e1 with
 
241
       | EAplus t1 t2 =>
 
242
           match t2 with
 
243
           | EAplus t2 t3 => EAplus t1 (EAplus t2 (merge_plus t3 e2))
 
244
           | _ => EAplus t1 (EAplus t2 e2)
 
245
           end
 
246
       | _ => EAplus e1 e2
 
247
       end).
 
248
 
 
249
Fixpoint assoc (e:ExprA) : ExprA :=
 
250
  match e with
 
251
  | EAplus e1 e3 =>
 
252
      match e1 with
 
253
      | EAplus e1 e2 =>
 
254
          merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3)
 
255
      | _ => EAplus (assoc_mult e1) (assoc e3)
 
256
      end
 
257
  | _ => assoc_mult e
 
258
  end.
 
259
 
 
260
Lemma merge_mult_correct1 :
 
261
 forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
 
262
   interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) =
 
263
   interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)).
 
264
Proof.
 
265
intros e1 e2; generalize e1; generalize e2; clear e1 e2.
 
266
simple induction e2; auto; intros.
 
267
unfold merge_mult at 1 in |- *; fold merge_mult in |- *;
 
268
 unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *;
 
269
 rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *;
 
270
 fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *;
 
271
 fold interp_ExprA in |- *; auto.
 
272
Qed.
 
273
 
 
274
Lemma merge_mult_correct :
 
275
 forall (e1 e2:ExprA) (lvar:list (AT * nat)),
 
276
   interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).
 
277
Proof.
 
278
simple induction e1; auto; intros.
 
279
elim e0; try (intros; simpl in |- *; legacy ring).
 
280
unfold interp_ExprA in H2; fold interp_ExprA in H2;
 
281
 cut
 
282
  (AmultT (interp_ExprA lvar e2)
 
283
     (AmultT (interp_ExprA lvar e4)
 
284
        (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))) =
 
285
   AmultT
 
286
     (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4))
 
287
        (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
 
288
intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1;
 
289
 simpl in |- *; legacy ring.
 
290
legacy ring.
 
291
Qed.
 
292
 
 
293
Lemma assoc_mult_correct1 :
 
294
 forall (e1 e2:ExprA) (lvar:list (AT * nat)),
 
295
   AmultT (interp_ExprA lvar (assoc_mult e1))
 
296
     (interp_ExprA lvar (assoc_mult e2)) =
 
297
   interp_ExprA lvar (assoc_mult (EAmult e1 e2)).
 
298
Proof.
 
299
simple induction e1; auto; intros.
 
300
rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct;
 
301
 simpl in |- *; rewrite merge_mult_correct; simpl in |- *; 
 
302
 auto.
 
303
Qed.
 
304
 
 
305
Lemma assoc_mult_correct :
 
306
 forall (e:ExprA) (lvar:list (AT * nat)),
 
307
   interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
 
308
Proof.
 
309
simple induction e; auto; intros.
 
310
elim e0; intros.
 
311
intros; simpl in |- *; legacy ring.
 
312
simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1)));
 
313
 rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0.
 
314
simpl in |- *; rewrite (H0 lvar); auto.
 
315
simpl in |- *; rewrite merge_mult_correct; simpl in |- *;
 
316
 rewrite merge_mult_correct; simpl in |- *; rewrite AmultT_assoc;
 
317
 rewrite assoc_mult_correct1; rewrite H2; simpl in |- *;
 
318
 rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1;
 
319
 fold interp_ExprA in H1; rewrite (H0 lvar) in H1;
 
320
 rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1));
 
321
 rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; 
 
322
 legacy ring.
 
323
simpl in |- *; rewrite (H0 lvar); auto.
 
324
simpl in |- *; rewrite (H0 lvar); auto.
 
325
simpl in |- *; rewrite (H0 lvar); auto.
 
326
Qed.
 
327
 
 
328
Lemma merge_plus_correct1 :
 
329
 forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
 
330
   interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) =
 
331
   interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)).
 
332
Proof.
 
333
intros e1 e2; generalize e1; generalize e2; clear e1 e2.
 
334
simple induction e2; auto; intros.
 
335
unfold merge_plus at 1 in |- *; fold merge_plus in |- *;
 
336
 unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *;
 
337
 rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *;
 
338
 fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *;
 
339
 fold interp_ExprA in |- *; auto.
 
340
Qed.
 
341
 
 
342
Lemma merge_plus_correct :
 
343
 forall (e1 e2:ExprA) (lvar:list (AT * nat)),
 
344
   interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).
 
345
Proof.
 
346
simple induction e1; auto; intros.
 
347
elim e0; try intros; try (simpl in |- *; legacy ring).
 
348
unfold interp_ExprA in H2; fold interp_ExprA in H2;
 
349
 cut
 
350
  (AplusT (interp_ExprA lvar e2)
 
351
     (AplusT (interp_ExprA lvar e4)
 
352
        (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))) =
 
353
   AplusT
 
354
     (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4))
 
355
        (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
 
356
intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1;
 
357
 simpl in |- *; legacy ring.
 
358
legacy ring.
 
359
Qed.
 
360
 
 
361
Lemma assoc_plus_correct :
 
362
 forall (e1 e2:ExprA) (lvar:list (AT * nat)),
 
363
   AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) =
 
364
   interp_ExprA lvar (assoc (EAplus e1 e2)).
 
365
Proof.
 
366
simple induction e1; auto; intros.
 
367
rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct;
 
368
 simpl in |- *; rewrite merge_plus_correct; simpl in |- *; 
 
369
 auto.
 
370
Qed.
 
371
 
 
372
Lemma assoc_correct :
 
373
 forall (e:ExprA) (lvar:list (AT * nat)),
 
374
   interp_ExprA lvar (assoc e) = interp_ExprA lvar e.
 
375
Proof.
 
376
simple induction e; auto; intros.
 
377
elim e0; intros.
 
378
simpl in |- *; rewrite (H0 lvar); auto.
 
379
simpl in |- *; rewrite (H0 lvar); auto.
 
380
simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
 
381
 rewrite merge_plus_correct; simpl in |- *; rewrite AplusT_assoc;
 
382
 rewrite assoc_plus_correct; rewrite H2; simpl in |- *;
 
383
 apply
 
384
  (r_AplusT_plus (interp_ExprA lvar (assoc e1))
 
385
     (AplusT (interp_ExprA lvar (assoc e2))
 
386
        (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1)))
 
387
     (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3))
 
388
        (interp_ExprA lvar e1))); rewrite <- AplusT_assoc;
 
389
 rewrite
 
390
  (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))
 
391
  ; rewrite assoc_plus_correct; rewrite H1; simpl in |- *; 
 
392
 rewrite (H0 lvar);
 
393
 rewrite <-
 
394
  (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1))
 
395
     (interp_ExprA lvar e3) (interp_ExprA lvar e1))
 
396
  ;
 
397
 rewrite
 
398
  (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1)
 
399
     (interp_ExprA lvar e3));
 
400
 rewrite (AplusT_comm (interp_ExprA lvar e1) (interp_ExprA lvar e3));
 
401
 rewrite <-
 
402
  (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3)
 
403
     (interp_ExprA lvar e1)); apply AplusT_comm.
 
404
unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *;
 
405
 fold interp_ExprA in |- *; rewrite assoc_mult_correct; 
 
406
 rewrite (H0 lvar); simpl in |- *; auto.
 
407
simpl in |- *; rewrite (H0 lvar); auto.
 
408
simpl in |- *; rewrite (H0 lvar); auto.
 
409
simpl in |- *; rewrite (H0 lvar); auto.
 
410
unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *;
 
411
 fold interp_ExprA in |- *; rewrite assoc_mult_correct; 
 
412
 simpl in |- *; auto.
 
413
Qed.
 
414
 
 
415
(**** Distribution *****)
 
416
 
 
417
Fixpoint distrib_EAopp (e:ExprA) : ExprA :=
 
418
  match e with
 
419
  | EAplus e1 e2 => EAplus (distrib_EAopp e1) (distrib_EAopp e2)
 
420
  | EAmult e1 e2 => EAmult (distrib_EAopp e1) (distrib_EAopp e2)
 
421
  | EAopp e => EAmult (EAopp EAone) (distrib_EAopp e)
 
422
  | e => e
 
423
  end.
 
424
 
 
425
Definition distrib_mult_right :=
 
426
  (fix distrib_mult_right (e1:ExprA) : ExprA -> ExprA :=
 
427
     fun e2:ExprA =>
 
428
       match e1 with
 
429
       | EAplus t1 t2 =>
 
430
           EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2)
 
431
       | _ => EAmult e1 e2
 
432
       end).
 
433
 
 
434
Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA :=
 
435
  match e1 with
 
436
  | EAplus t1 t2 =>
 
437
      EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2)
 
438
  | _ => distrib_mult_right e2 e1
 
439
  end.
 
440
 
 
441
Fixpoint distrib_main (e:ExprA) : ExprA :=
 
442
  match e with
 
443
  | EAmult e1 e2 => distrib_mult_left (distrib_main e1) (distrib_main e2)
 
444
  | EAplus e1 e2 => EAplus (distrib_main e1) (distrib_main e2)
 
445
  | EAopp e => EAopp (distrib_main e)
 
446
  | _ => e
 
447
  end.
 
448
 
 
449
Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).
 
450
 
 
451
Lemma distrib_mult_right_correct :
 
452
 forall (e1 e2:ExprA) (lvar:list (AT * nat)),
 
453
   interp_ExprA lvar (distrib_mult_right e1 e2) =
 
454
   AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
 
455
Proof.
 
456
simple induction e1; try intros; simpl in |- *; auto.
 
457
rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
 
458
 rewrite (H0 e2 lvar); legacy ring.
 
459
Qed.
 
460
 
 
461
Lemma distrib_mult_left_correct :
 
462
 forall (e1 e2:ExprA) (lvar:list (AT * nat)),
 
463
   interp_ExprA lvar (distrib_mult_left e1 e2) =
 
464
   AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
 
465
Proof.
 
466
simple induction e1; try intros; simpl in |- *.
 
467
rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl in |- *;
 
468
 apply AmultT_Or.
 
469
rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. 
 
470
rewrite AmultT_comm;
 
471
 rewrite
 
472
  (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e)
 
473
     (interp_ExprA lvar e0));
 
474
 rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e));
 
475
 rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0));
 
476
 rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto.
 
477
rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
 
478
rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
 
479
rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
 
480
rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
 
481
Qed.
 
482
 
 
483
Lemma distrib_correct :
 
484
 forall (e:ExprA) (lvar:list (AT * nat)),
 
485
   interp_ExprA lvar (distrib e) = interp_ExprA lvar e.
 
486
Proof.
 
487
simple induction e; intros; auto.
 
488
simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar);
 
489
 unfold distrib in |- *; simpl in |- *; auto.
 
490
simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar);
 
491
 unfold distrib in |- *; simpl in |- *; apply distrib_mult_left_correct.
 
492
simpl in |- *; fold AoppT in |- *; rewrite <- (H lvar);
 
493
 unfold distrib in |- *; simpl in |- *; rewrite distrib_mult_right_correct;
 
494
 simpl in |- *; fold AoppT in |- *; legacy ring.
 
495
Qed.
 
496
 
 
497
(**** Multiplication by the inverse product ****)
 
498
 
 
499
Lemma mult_eq :
 
500
 forall (e1 e2 a:ExprA) (lvar:list (AT * nat)),
 
501
   interp_ExprA lvar a <> AzeroT ->
 
502
   interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) ->
 
503
   interp_ExprA lvar e1 = interp_ExprA lvar e2.
 
504
Proof.
 
505
  simpl in |- *; intros;
 
506
   apply
 
507
    (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1)
 
508
       (interp_ExprA lvar e2)); assumption.
 
509
Qed.
 
510
 
 
511
Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA :=
 
512
  match e with
 
513
  | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2)
 
514
  | _ => EAmult a e
 
515
  end.
 
516
 
 
517
Definition multiply (e:ExprA) : ExprA :=
 
518
  match e with
 
519
  | EAmult a e1 => multiply_aux a e1
 
520
  | _ => e
 
521
  end.
 
522
 
 
523
Lemma multiply_aux_correct :
 
524
 forall (a e:ExprA) (lvar:list (AT * nat)),
 
525
   interp_ExprA lvar (multiply_aux a e) =
 
526
   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
 
527
Proof.
 
528
simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
 
529
 auto.
 
530
  simpl in |- *; rewrite (H0 lvar); legacy ring.
 
531
Qed.
 
532
 
 
533
Lemma multiply_correct :
 
534
 forall (e:ExprA) (lvar:list (AT * nat)),
 
535
   interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
 
536
Proof.
 
537
  simple induction e; simpl in |- *; auto.
 
538
  intros; apply multiply_aux_correct.
 
539
Qed.
 
540
 
 
541
(**** Permutations and simplification ****)
 
542
 
 
543
Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA :=
 
544
  match m with
 
545
  | EAmult m0 m1 =>
 
546
      match eqExprA m0 (EAinv a) with
 
547
      | left _ => m1
 
548
      | right _ => EAmult m0 (monom_remove a m1)
 
549
      end
 
550
  | _ =>
 
551
      match eqExprA m (EAinv a) with
 
552
      | left _ => EAone
 
553
      | right _ => EAmult a m
 
554
      end
 
555
  end.
 
556
 
 
557
Definition monom_simplif_rem :=
 
558
  (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA :=
 
559
     fun m:ExprA =>
 
560
       match a with
 
561
       | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m)
 
562
       | _ => monom_remove a m
 
563
       end).
 
564
 
 
565
Definition monom_simplif (a m:ExprA) : ExprA :=
 
566
  match m with
 
567
  | EAmult a' m' =>
 
568
      match eqExprA a a' with
 
569
      | left _ => monom_simplif_rem a m'
 
570
      | right _ => m
 
571
      end
 
572
  | _ => m
 
573
  end.
 
574
 
 
575
Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
 
576
  match e with
 
577
  | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2)
 
578
  | _ => monom_simplif a e
 
579
  end.
 
580
 
 
581
Lemma monom_remove_correct :
 
582
 forall (e a:ExprA) (lvar:list (AT * nat)),
 
583
   interp_ExprA lvar a <> AzeroT ->
 
584
   interp_ExprA lvar (monom_remove a e) =
 
585
   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
 
586
Proof.
 
587
simple induction e; intros.
 
588
simpl in |- *; case (eqExprA EAzero (EAinv a)); intros;
 
589
 [ inversion e0 | simpl in |- *; trivial ].
 
590
simpl in |- *; case (eqExprA EAone (EAinv a)); intros;
 
591
 [ inversion e0 | simpl in |- *; trivial ].
 
592
simpl in |- *; case (eqExprA (EAplus e0 e1) (EAinv a)); intros;
 
593
 [ inversion e2 | simpl in |- *; trivial ].
 
594
simpl in |- *; case (eqExprA e0 (EAinv a)); intros.
 
595
rewrite e2; simpl in |- *; fold AinvT in |- *.
 
596
rewrite <-
 
597
 (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a))
 
598
    (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ].
 
599
simpl in |- *; rewrite H0; auto; legacy ring.
 
600
simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a));
 
601
 intros; [ inversion e1 | simpl in |- *; trivial ].
 
602
unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros.
 
603
case (eqExprA e0 a); intros.
 
604
rewrite e2; simpl in |- *; fold AinvT in |- *; rewrite AinvT_r; auto.
 
605
inversion e1; simpl in |- *; elimtype False; auto.
 
606
simpl in |- *; trivial.
 
607
unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros;
 
608
 [ inversion e0 | simpl in |- *; trivial ].
 
609
Qed.
 
610
 
 
611
Lemma monom_simplif_rem_correct :
 
612
 forall (a e:ExprA) (lvar:list (AT * nat)),
 
613
   interp_ExprA lvar a <> AzeroT ->
 
614
   interp_ExprA lvar (monom_simplif_rem a e) =
 
615
   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
 
616
Proof.
 
617
simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct;
 
618
 auto.
 
619
elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1);
 
620
 intros.
 
621
rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto.
 
622
legacy ring.
 
623
Qed.
 
624
 
 
625
Lemma monom_simplif_correct :
 
626
 forall (e a:ExprA) (lvar:list (AT * nat)),
 
627
   interp_ExprA lvar a <> AzeroT ->
 
628
   interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e.
 
629
Proof.
 
630
simple induction e; intros; auto.
 
631
simpl in |- *; case (eqExprA a e0); intros.
 
632
rewrite <- e2; apply monom_simplif_rem_correct; auto. 
 
633
simpl in |- *; trivial.
 
634
Qed.
 
635
 
 
636
Lemma inverse_correct :
 
637
 forall (e a:ExprA) (lvar:list (AT * nat)),
 
638
   interp_ExprA lvar a <> AzeroT ->
 
639
   interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e.
 
640
Proof.
 
641
simple induction e; intros; auto.
 
642
simpl in |- *; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto.
 
643
unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto.
 
644
Qed.
 
645
 
 
646
End Theory_of_fields.
 
647
 
 
648
(* Compatibility *)
 
649
Notation AplusT_sym := AplusT_comm (only parsing).
 
650
Notation AmultT_sym := AmultT_comm (only parsing).