blob: 1f7915eebfd8efc7ee53f63c9c86519f52132e8e (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Export Morphisms Setoid Bool.
Require Import ZArith.
Require Export Algebra_syntax.
Require Export Ring2.
Require Export Ring2_initial.
Require Export Ring2_tac.
Class Cring {R:Type}`{Rr:Ring R} :=
cring_mul_comm: forall x y:R, x * y == y * x.
Ltac reify_goal lvar lexpr lterm:=
(*idtac lvar; idtac lexpr; idtac lterm;*)
match lexpr with
nil => idtac
| ?e1::?e2::_ =>
match goal with
|- (?op ?u1 ?u2) =>
change (op
(@Ring_polynom.PEeval
_ zero _+_ _*_ _-_ -_ Z gen_phiZ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication) lvar e1)
(@Ring_polynom.PEeval
_ zero _+_ _*_ _-_ -_ Z gen_phiZ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication) lvar e2))
end
end.
Section cring.
Context {R:Type}`{Rr:Cring R}.
Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.
intros. apply mk_reqe;intros.
rewrite H. rewrite H0. reflexivity.
rewrite H. rewrite H0. reflexivity.
rewrite H. reflexivity. Defined.
Lemma cring_almost_ring_theory:
almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.
intros. apply mk_art ;intros.
rewrite ring_add_0_l; reflexivity.
rewrite ring_add_comm; reflexivity.
rewrite ring_add_assoc; reflexivity.
rewrite ring_mul_1_l; reflexivity.
apply ring_mul_0_l.
rewrite cring_mul_comm; reflexivity.
rewrite ring_mul_assoc; reflexivity.
rewrite ring_distr_l; reflexivity.
rewrite ring_opp_mul_l; reflexivity.
apply ring_opp_add.
rewrite ring_sub_def ; reflexivity. Defined.
Lemma cring_morph:
ring_morph zero one _+_ _*_ _-_ -_ _==_
0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
gen_phiZ.
intros. apply mkmorph ; intros; simpl; try reflexivity.
rewrite gen_phiZ_add; reflexivity.
rewrite ring_sub_def. unfold Zminus. rewrite gen_phiZ_add.
rewrite gen_phiZ_opp; reflexivity.
rewrite gen_phiZ_mul; reflexivity.
rewrite gen_phiZ_opp; reflexivity.
rewrite (Zeqb_ok x y H). reflexivity. Defined.
Lemma cring_power_theory :
@Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication).
intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
Lemma cring_div_theory:
div_theory _==_ Zplus Zmult gen_phiZ Z.quotrem.
intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
simpl. apply ring_setoid. Defined.
End cring.
Ltac cring_gen :=
match goal with
|- ?g => let lterm := lterm_goal g in (* les variables *)
match eval red in (list_reifyl (lterm:=lterm)) with
| (?fv, ?lexpr) =>
(*idtac "variables:";idtac fv;
idtac "terms:"; idtac lterm;
idtac "reifications:"; idtac lexpr; *)
reify_goal fv lexpr lterm;
match goal with
|- ?g =>
generalize
(@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_
ring_setoid
cring_eq_ext
cring_almost_ring_theory
Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
gen_phiZ
cring_morph
N
(fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication)
cring_power_theory
Z.quotrem
cring_div_theory
O fv nil);
let rc := fresh "rc"in
intro rc; apply rc
end
end
end.
Ltac cring_compute:= vm_compute; reflexivity.
Ltac cring:=
intros;
cring_gen;
cring_compute.
|
