aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/InitialRing.v
blob: f5db275465b18708330538875ff13435b2f9f2e9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

Require Import Zbool.
Require Import BinInt.
Require Import BinNat.
Require Import Setoid.
Require Import Ring_theory.
Require Import Ring_polynom.
Import List.

Set Implicit Arguments.
(* Set Universe Polymorphism. *)

Import RingSyntax.

(* An object to return when an expression is not recognized as a constant *)
Definition NotConstant := false.

(** Z is a ring and a setoid*)

Lemma Zsth : Setoid_Theory Z (@eq Z).
Proof (Eqsth Z).

Lemma Zeqe : ring_eq_ext Z.add Z.mul Z.opp (@eq Z).
Proof (Eq_ext Z.add Z.mul Z.opp).

Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).
Proof.
 constructor. exact Z.add_0_l. exact Z.add_comm. exact Z.add_assoc.
 exact Z.mul_1_l. exact Z.mul_comm. exact Z.mul_assoc.
 exact Z.mul_add_distr_r. trivial. exact Z.sub_diag.
Qed.

(** Two generic morphisms from Z to (abrbitrary) rings, *)
(**second one is more convenient for proofs but they are ext. equal*)
Section ZMORPHISM.
 Variable R : Type.
 Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
 Variable req : R -> R -> Prop.
  Notation "0" := rO.  Notation "1" := rI.
  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" := (req x y).
  Variable Rsth : Setoid_Theory R req.
     Add Parametric Relation : R req
       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
      as R_setoid3.
     Ltac rrefl := gen_reflexivity Rsth.
 Variable Reqe : ring_eq_ext radd rmul ropp req.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
   Proof. exact (Radd_ext Reqe). Qed.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
   Proof. exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp with signature (req ==> req) as ropp_ext3.
   Proof. exact (Ropp_ext Reqe). Qed.

 Fixpoint gen_phiPOS1 (p:positive) : R :=
  match p with
  | xH => 1
  | xO p => (1 + 1) * (gen_phiPOS1 p)
  | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
  end.

 Fixpoint gen_phiPOS (p:positive) : R :=
  match p with
  | xH => 1
  | xO xH => (1 + 1)
  | xO p => (1 + 1) * (gen_phiPOS p)
  | xI xH => 1 + (1 +1)
  | xI p => 1 + ((1 + 1) * (gen_phiPOS p))
  end.

 Definition gen_phiZ1 z :=
  match z with
  | Zpos p => gen_phiPOS1 p
  | Z0 => 0
  | Zneg p => -(gen_phiPOS1 p)
  end.

 Definition gen_phiZ z :=
  match z with
  | Zpos p => gen_phiPOS p
  | Z0 => 0
  | Zneg p => -(gen_phiPOS p)
  end.
 Notation "[ x ]" := (gen_phiZ x).

 Definition get_signZ z :=
  match z with
  | Zneg p => Some (Zpos p)
  | _ => None
  end.

 Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ.
 Proof.
  constructor.
  destruct c;intros;try discriminate.
  injection H as <-.
  simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
 Qed.


 Section ALMOST_RING.
 Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3.
   Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
   Ltac norm := gen_srewrite Rsth Reqe ARth.
   Ltac add_push := gen_add_push radd Rsth Reqe ARth.

 Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
 Proof.
  induction x;simpl.
  rewrite IHx;destruct x;simpl;norm.
  rewrite IHx;destruct x;simpl;norm.
  rrefl.
 Qed.

 Lemma ARgen_phiPOS_Psucc : forall x,
   gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).
 Proof.
  induction x;simpl;norm.
  rewrite IHx;norm.
  add_push 1;rrefl.
 Qed.

 Lemma ARgen_phiPOS_add : forall x y,
   gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
 Proof.
  induction x;destruct y;simpl;norm.
  rewrite Pos.add_carry_spec.
  rewrite ARgen_phiPOS_Psucc.
  rewrite IHx;norm.
  add_push (gen_phiPOS1 y);add_push 1;rrefl.
  rewrite IHx;norm;add_push (gen_phiPOS1 y);rrefl.
  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
  rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;rrefl.
  rewrite IHx;norm;add_push(gen_phiPOS1 y);rrefl.
  add_push 1;rrefl.
  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
 Qed.

 Lemma ARgen_phiPOS_mult :
   forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
 Proof.
  induction x;intros;simpl;norm.
  rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
  rewrite IHx;rrefl.
 Qed.

 End ALMOST_RING.

 Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
 Let ARth := Rth_ARth Rsth Reqe Rth.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4.
   Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
   Ltac norm := gen_srewrite Rsth Reqe ARth.
   Ltac add_push := gen_add_push radd Rsth Reqe ARth.

(*morphisms are extensionally equal*)
 Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
 Proof.
  destruct x;simpl; try rewrite (same_gen ARth);rrefl.
 Qed.

 Lemma gen_Zeqb_ok : forall x y,
   Zeq_bool x y = true -> [x] == [y].
 Proof.
  intros x y H.
  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
  rewrite H1;rrefl.
 Qed.

 Lemma gen_phiZ1_pos_sub : forall x y,
 gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
 Proof.
  intros x y.
  rewrite Z.pos_sub_spec.
  case Pos.compare_spec; intros H; simpl.
  rewrite H. rewrite (Ropp_def Rth);rrefl.
  rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
  rewrite (ARgen_phiPOS_add ARth);simpl;norm.
  rewrite (Ropp_def Rth);norm.
  rewrite <- (Pos.sub_add x y H) at 2.
  rewrite (ARgen_phiPOS_add ARth);simpl;norm.
  add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
 Qed.

 Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
 Proof.
  intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
  destruct x, y; simpl; norm.
  apply (ARgen_phiPOS_add ARth).
  apply gen_phiZ1_pos_sub.
  rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
  rewrite (ARgen_phiPOS_add ARth); norm.
 Qed.

 Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
 Proof.
  intros x y;repeat rewrite same_genZ.
  destruct x;destruct y;simpl;norm;
  rewrite  (ARgen_phiPOS_mult ARth);try (norm;fail).
  rewrite (Ropp_opp Rsth Reqe Rth);rrefl.
 Qed.

 Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
 Proof. intros;subst;rrefl. Qed.

(*proof that [.] satisfies morphism specifications*)
 Lemma gen_phiZ_morph :
  ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH)
   Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ.
 Proof.
  assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH)
                  Z.add Z.mul Zeq_bool gen_phiZ).
   apply mkRmorph;simpl;try rrefl.
   apply gen_phiZ_add.  apply gen_phiZ_mul. apply gen_Zeqb_ok.
  apply  (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
 Qed.

End ZMORPHISM.

(** N is a semi-ring and a setoid*)
Lemma Nsth : Setoid_Theory N (@eq N).
Proof (Eqsth N).

Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N).
Proof (Eq_s_ext N.add N.mul).

Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).
Proof.
 constructor. exact N.add_0_l. exact N.add_comm. exact N.add_assoc.
 exact N.mul_1_l. exact N.mul_0_l. exact N.mul_comm. exact N.mul_assoc.
 exact N.mul_add_distr_r.
Qed.

Definition Nsub := SRsub N.add.
Definition Nopp := (@SRopp N).

Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
Proof (SReqe_Reqe Nseqe).

Lemma Nath :
 almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).
Proof (SRth_ARth Nsth Nth).

Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.

(**Same as above : definition of two, extensionally equal, generic morphisms *)
(**from N to any semi-ring*)
Section NMORPHISM.
 Variable R : Type.
 Variable  (rO rI : R) (radd rmul: R->R->R).
 Variable req : R -> R -> Prop.
  Notation "0" := rO.  Notation "1" := rI.
  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
 Variable Rsth : Setoid_Theory R req.
     Add Parametric Relation : R req
       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
       as R_setoid4.
     Ltac rrefl := gen_reflexivity Rsth.
 Variable SReqe : sring_eq_ext radd rmul req.
 Variable SRth : semi_ring_theory 0 1 radd rmul req.
 Let ARth := SRth_ARth Rsth SRth.
 Let Reqe := SReqe_Reqe SReqe.
 Let ropp := (@SRopp R).
 Let rsub := (@SRsub R radd).
  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
  Notation "x == y" := (req x y).
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext4.
   Proof. exact (Radd_ext Reqe). Qed.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4.
   Proof. exact (Rmul_ext Reqe). Qed.
   Ltac norm := gen_srewrite_sr Rsth Reqe ARth.

 Definition gen_phiN1 x :=
  match x with
  | N0 => 0
  | Npos x => gen_phiPOS1 1 radd rmul x
  end.

 Definition gen_phiN x :=
  match x with
  | N0 => 0
  | Npos x => gen_phiPOS 1 radd rmul x
  end.
 Notation "[ x ]" := (gen_phiN x).

 Lemma same_genN : forall x, [x] == gen_phiN1 x.
 Proof.
  destruct x;simpl. reflexivity.
  now rewrite (same_gen Rsth Reqe ARth).
 Qed.

 Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y].
 Proof.
  intros x y;repeat rewrite same_genN.
  destruct x;destruct y;simpl;norm.
  apply (ARgen_phiPOS_add Rsth Reqe ARth).
 Qed.

 Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y].
 Proof.
  intros x y;repeat rewrite same_genN.
  destruct x;destruct y;simpl;norm.
  apply (ARgen_phiPOS_mult Rsth Reqe ARth).
 Qed.

 Lemma gen_phiN_sub : forall x y, [Nsub x y] == [x] - [y].
 Proof. exact gen_phiN_add. Qed.

(*gen_phiN satisfies morphism specifications*)
 Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req
                           0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
 Proof.
  constructor; simpl; try reflexivity.
  apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
  intros x y EQ. apply N.eqb_eq in EQ. now subst.
 Qed.

End NMORPHISM.

(* Words on N : initial structure for almost-rings. *)
Definition Nword := list N.
Definition NwO : Nword := nil.
Definition NwI : Nword := 1%N :: nil.

Definition Nwcons n (w : Nword) : Nword :=
  match w, n with
  | nil, 0%N => nil
  | _, _ => n :: w
  end.

Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword :=
  match w1, w2 with
  | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2'
  | nil, _ => w2
  | _, nil => w1
  end.

Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w.

Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2).

Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword :=
  match w with
  | m :: w' => (n*m)%N :: Nwscal n w'
  | nil => nil
  end.

Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword :=
  match w1 with
  | 0%N::w1' => Nwopp (Nwmul w1' w2)
  | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2)
  | nil => nil
  end.
Fixpoint Nw_is0 (w : Nword) : bool :=
  match w with
  | nil => true
  | 0%N :: w' => Nw_is0 w'
  | _ => false
  end.

Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
  match w1, w2 with
  | n1::w1', n2::w2' =>
     if N.eqb n1 n2 then Nweq_bool w1' w2' else false
  | nil, _ => Nw_is0 w2
  | _, nil => Nw_is0 w1
  end.

Section NWORDMORPHISM.
 Variable R : Type.
 Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
 Variable req : R -> R -> Prop.
  Notation "0" := rO.  Notation "1" := rI.
  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" := (req x y).
  Variable Rsth : Setoid_Theory R req.
     Add Parametric Relation : R req
       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
      as R_setoid5.
     Ltac rrefl := gen_reflexivity Rsth.
 Variable Reqe : ring_eq_ext radd rmul ropp req.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
   Proof. exact (Radd_ext Reqe). Qed.
   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5.
   Proof. exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp with signature (req ==> req) as ropp_ext5.
   Proof. exact (Ropp_ext Reqe). Qed.

 Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7.
   Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
   Ltac norm := gen_srewrite Rsth Reqe ARth.
   Ltac add_push := gen_add_push radd Rsth Reqe ARth.

 Fixpoint gen_phiNword (w : Nword) : R :=
  match w with
  | nil => 0
  | n :: nil => gen_phiN rO rI radd rmul n
  | N0 :: w' => - gen_phiNword w'
  | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w'
  end.

 Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
Proof.
induction w; simpl; intros; auto.
 reflexivity.

 destruct a.
  destruct w.
   reflexivity.

   rewrite IHw; trivial.
   apply (ARopp_zero Rsth Reqe ARth).

   discriminate.
Qed.

  Lemma gen_phiNword_cons : forall w n,
    gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
induction w.
 destruct n; simpl; norm.

 intros.
 destruct n; norm.
Qed.

  Lemma gen_phiNword_Nwcons : forall w n,
    gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
destruct w; intros.
 destruct n; norm.

 unfold Nwcons.
 rewrite gen_phiNword_cons.
 reflexivity.
Qed.

 Lemma gen_phiNword_ok : forall w1 w2,
   Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
induction w1; intros.
 simpl.
 rewrite (gen_phiNword0_ok _ H).
 reflexivity.

 rewrite gen_phiNword_cons.
 destruct w2.
  simpl in H.
  destruct a; try  discriminate.
  rewrite (gen_phiNword0_ok _ H).
  norm.

  simpl in H.
  rewrite gen_phiNword_cons.
  case_eq (N.eqb a n); intros H0.
   rewrite H0 in H.
   apply N.eqb_eq in H0. rewrite <- H0.
   rewrite (IHw1 _ H).
   reflexivity.

   rewrite H0 in H;  discriminate H.
Qed.


Lemma Nwadd_ok : forall x y,
   gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.
induction x; intros.
 simpl.
 norm.

 destruct y.
  simpl Nwadd; norm.

  simpl Nwadd.
  repeat rewrite gen_phiNword_cons.
  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) by
    (destruct Reqe; constructor; trivial).

  rewrite IHx.
  norm.
  add_push (- gen_phiNword x); reflexivity.
Qed.

Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
simpl.
unfold Nwopp; simpl.
intros.
rewrite gen_phiNword_Nwcons; norm.
Qed.

Lemma Nwscal_ok : forall n x,
  gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.
induction x; intros.
 norm.

 simpl Nwscal.
 repeat rewrite gen_phiNword_cons.
 rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth))
   by (destruct Reqe; constructor; trivial).

  rewrite IHx.
  norm.
Qed.

Lemma Nwmul_ok : forall x y,
   gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.
induction x; intros.
 norm.

 destruct a.
  simpl Nwmul.
  rewrite Nwopp_ok.
  rewrite IHx.
  rewrite gen_phiNword_cons.
  norm.

  simpl Nwmul.
  unfold Nwsub.
  rewrite Nwadd_ok.
  rewrite Nwscal_ok.
  rewrite Nwopp_ok.
  rewrite IHx.
  rewrite gen_phiNword_cons.
  norm.
Qed.

(* Proof that [.] satisfies morphism specifications *)
 Lemma gen_phiNword_morph :
  ring_morph 0 1 radd rmul rsub ropp req
   NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.
constructor.
 reflexivity.

 reflexivity.

 exact Nwadd_ok.

 intros.
 unfold Nwsub.
 rewrite Nwadd_ok.
 rewrite Nwopp_ok.
 norm.

 exact Nwmul_ok.

 exact Nwopp_ok.

 exact gen_phiNword_ok.
Qed.

End NWORDMORPHISM.

Section GEN_DIV.

  Variables  (R : Type) (rO : R) (rI : R) (radd : R -> R -> R)
              (rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R)
              (req : R -> R -> Prop) (C : Type) (cO : C) (cI : C)
              (cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C)
              (copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R).
 Variable Rsth : Setoid_Theory R req.
 Variable Reqe : ring_eq_ext radd rmul ropp req.
 Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
 Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.

  (* Useful tactics *)
  Add Parametric Relation : R req
    reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
    symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
    transitivity proved by Rsth.(@Equivalence_Transitive _ _)
   as R_set1.
 Ltac rrefl := gen_reflexivity Rsth.
  Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
  Proof. exact (Radd_ext Reqe). Qed.
  Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
  Proof. exact (Rmul_ext Reqe). Qed.
  Add Morphism ropp with signature (req ==> req) as ropp_ext.
  Proof. exact (Ropp_ext Reqe). Qed.
  Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
  Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
 Ltac rsimpl := gen_srewrite Rsth Reqe ARth.

 Definition triv_div x y :=
   if ceqb x y then (cI, cO)
   else (cO, x).

 Ltac Esimpl :=repeat (progress (
   match goal with
   | |- context [phi cO] => rewrite (morph0 morph)
   | |- context [phi cI] => rewrite (morph1 morph)
   | |- context [phi (cadd ?x  ?y)] => rewrite ((morph_add morph) x y)
   | |- context [phi (cmul ?x  ?y)] => rewrite ((morph_mul morph) x y)
   | |- context [phi (csub ?x  ?y)] => rewrite ((morph_sub morph) x y)
   | |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x)
   end)).

 Lemma triv_div_th : Ring_theory.div_theory  req cadd cmul phi triv_div.
 Proof.
  constructor.
  intros a b;unfold triv_div.
  assert (X:= morph.(morph_eq) a b);destruct (ceqb a b).
  Esimpl.
  rewrite X; trivial.
  rsimpl.
  Esimpl;  rsimpl.
Qed.

 Variable zphi : Z -> R.

 Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.
 Proof.
  constructor.
  intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
  rewrite Z.mul_comm; rsimpl.
 Qed.

 Variable nphi : N -> R.

 Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
  constructor.
  intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst.
  rewrite N.mul_comm; rsimpl.
 Qed.

End GEN_DIV.

 (* syntaxification of constants in an abstract ring:
    the inverse of gen_phiPOS *)
 Ltac inv_gen_phi_pos rI add mul t :=
   let rec inv_cst t :=
   match t with
     rI => constr:(1%positive)
   | (add rI rI) => constr:(2%positive)
   | (add rI (add rI rI)) => constr:(3%positive)
   | (mul (add rI rI) ?p) => (* 2p *)
       match inv_cst p with
         NotConstant => constr:(NotConstant)
       | 1%positive => constr:(NotConstant) (* 2*1 is not convertible to 2 *)
       | ?p => constr:(xO p)
       end
   | (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
       match inv_cst p with
         NotConstant => constr:(NotConstant)
       | 1%positive => constr:(NotConstant)
       | ?p => constr:(xI p)
       end
   | _ => constr:(NotConstant)
   end in
   inv_cst t.

(* The (partial) inverse of gen_phiNword *)
 Ltac inv_gen_phiNword rO rI add mul opp t :=
   match t with
     rO => constr:(NwO)
   | _ =>
     match inv_gen_phi_pos rI add mul t with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Npos p::nil)
     end
   end.


(* The inverse of gen_phiN *)
 Ltac inv_gen_phiN rO rI add mul t :=
   match t with
     rO => constr:(0%N)
   | _ =>
     match inv_gen_phi_pos rI add mul t with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Npos p)
     end
   end.

(* The inverse of gen_phiZ *)
 Ltac inv_gen_phiZ rO rI add mul opp t :=
   match t with
     rO => constr:(0%Z)
   | (opp ?p) =>
     match inv_gen_phi_pos rI add mul p with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Zneg p)
     end
   | _ =>
     match inv_gen_phi_pos rI add mul t with
       NotConstant => constr:(NotConstant)
     | ?p => constr:(Zpos p)
     end
   end.

(* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above
   are only optimisations that directly returns the reified constant
   instead of resorting to the constant propagation of the simplification
   algorithm. *)
Ltac inv_gen_phi rO rI cO cI t :=
  match t with
  | rO => cO
  | rI => cI
  end.

(* A simple tactic recognizing no constant *)
 Ltac inv_morph_nothing t := constr:(NotConstant).

Ltac coerce_to_almost_ring set ext rspec :=
  match type of rspec with
  | ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec)
  | semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec)
  | almost_ring_theory _ _ _ _ _ _ _ => rspec
  | _ => fail 1 "not a valid ring theory"
  end.

Ltac coerce_to_ring_ext ext :=
  match type of ext with
  | ring_eq_ext _ _ _ _ => ext
  | sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext)
  | _ => fail 1 "not a valid ring_eq_ext theory"
  end.

Ltac abstract_ring_morphism set ext rspec :=
  match type of rspec with
  | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
  | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
  | almost_ring_theory _ _ _ _ _ _ _ =>
      constr:(gen_phiNword_morph set ext rspec)
  | _ => fail 1 "bad ring structure"
  end.

Record hypo : Type := mkhypo {
   hypo_type : Type;
   hypo_proof : hypo_type
 }.

Ltac gen_ring_pow set arth pspec :=
 match pspec with
 | None =>
   match type of arth with
   | @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
     constr:(mkhypo (@pow_N_th R rI rmul req set))
   | _ => fail 1 "gen_ring_pow"
   end
 | Some ?t => constr:(t)
 end.

Ltac gen_ring_sign morph sspec :=
  match sspec with
  | None =>
    match type of morph with
    | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
       constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th)
    | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               ?C  ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
        constr:(mkhypo (@get_sign_None_th C copp ceqb))
    | _ => fail 2 "ring anomaly : default_sign_spec"
    end
 | Some ?t => constr:(t)
 end.

Ltac default_div_spec set reqe arth morph :=
 match type of morph with
 | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               Z ?c0 ?c1 Z.add Z.mul ?csub ?copp ?ceq_b ?phi =>
      constr:(mkhypo (Ztriv_div_th set phi))
 | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               N ?c0 ?c1 N.add N.mul ?csub ?copp ?ceq_b ?phi =>
      constr:(mkhypo (Ntriv_div_th set phi))
 | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
      constr:(mkhypo (triv_div_th set reqe arth morph))
 | _ => fail 1 "ring anomaly : default_sign_spec"
 end.

Ltac gen_ring_div set reqe arth morph dspec  :=
 match dspec with
 | None => default_div_spec set reqe arth morph
 | Some ?t => constr:(t)
 end.

Ltac ring_elements set ext rspec pspec sspec dspec rk :=
  let arth := coerce_to_almost_ring set ext rspec in
  let ext_r := coerce_to_ring_ext ext in
  let morph :=
    match rk with
    | Abstract => abstract_ring_morphism set ext rspec
    | @Computational ?reqb_ok =>
        match type of arth with
        | almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ =>
            constr:(IDmorph rO rI add mul sub opp set _ reqb_ok)
        | _ => fail 2 "ring anomaly"
        end
    | @Morphism ?m =>
       match type of m with
       | ring_morph _ _ _ _ _ _ _  _ _ _ _ _ _  _ _ => m
       | @semi_morph _ _ _ _ _ _  _ _ _ _ _  _ _   =>
           constr:(SRmorph_Rmorph set m)
       | _ => fail 2 "ring anomaly"
       end
    | _ => fail 1 "ill-formed ring kind"
    end in
  let p_spec := gen_ring_pow set arth pspec in
  let s_spec := gen_ring_sign morph sspec in
  let d_spec := gen_ring_div set ext_r arth morph dspec in
  fun f => f arth ext_r morph p_spec s_spec d_spec.

(* Given a ring structure and the kind of morphism,
   returns 2 lemmas (one for ring, and one for ring_simplify). *)

 Ltac ring_lemmas set ext rspec pspec sspec dspec rk :=
  let gen_lemma2 :=
    match pspec with
    | None => constr:(ring_rw_correct)
    | Some _ => constr:(ring_rw_pow_correct)
    end in
  ring_elements set ext rspec pspec sspec dspec rk
    ltac:(fun arth ext_r morph p_spec s_spec d_spec =>
       match type of morph with
       | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
          let gen_lemma2_0 :=
              constr:(gen_lemma2 R  r0 rI  radd rmul rsub ropp req set ext_r arth
                                C  c0 c1 cadd cmul csub copp ceq_b phi morph) in
          match p_spec with
          | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec =>
             let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in
             match d_spec with
             | @mkhypo (div_theory _ _ _ _  ?cdiv) ?dd_spec =>
                let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in
                match s_spec with
                | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec =>
                  let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in
                  let lemma1 :=
                    constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in
                  fun f => f arth ext_r morph lemma1 lemma2
                | _ => fail 4 "ring: bad sign specification"
                end
             | _ => fail 3 "ring: bad coefficient division specification"
             end
          | _ => fail 2 "ring: bad power specification"
          end
       | _ => fail 1 "ring internal error: ring_lemmas, please report"
       end).

(* Tactic for constant *)
Ltac isnatcst t :=
  match t with
    O => constr:(true)
  | S ?p => isnatcst p
  | _ => constr:(false)
  end.

Ltac isPcst t :=
  match t with
  | xI ?p => isPcst p
  | xO ?p => isPcst p
  | xH => constr:(true)
  (* nat -> positive *)
  | Pos.of_succ_nat ?n => isnatcst n
  | _ => constr:(false)
  end.

Ltac isNcst t :=
  match t with
    N0 => constr:(true)
  | Npos ?p => isPcst p
  | _ => constr:(false)
  end.

Ltac isZcst t :=
  match t with
    Z0 => constr:(true)
  | Zpos ?p => isPcst p
  | Zneg ?p => isPcst p
  (* injection nat -> Z *)
  | Z.of_nat ?n => isnatcst n
  (* injection N -> Z *)
  | Z.of_N ?n => isNcst n
  (* *)
  | _ => constr:(false)
  end.