blob: 5733d5ccabae7f9d403378b43a99fda04ae3d6ee (
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
|
Require Coq.setoid_ring.Integral_domain.
Require Crypto.Algebra.Nsatz.
Require Import Crypto.Util.Factorize.
Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring.
Require Import Crypto.Util.Tactics.RewriteHyp.
Require Import Crypto.Util.Tactics.BreakMatch.
Module IntegralDomain.
Section IntegralDomain.
Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}.
Lemma nonzero_product_iff_nonzero_factors :
forall x y : T, ~ eq (mul x y) zero <-> ~ eq x zero /\ ~ eq y zero.
Proof using Type*. setoid_rewrite Ring.zero_product_iff_zero_factor; intuition. Qed.
Global Instance Integral_domain :
@Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops
Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring.
Proof using Type. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed.
End IntegralDomain.
Module _LargeCharacteristicReflective.
Section ReflectiveNsatzSideConditionProver.
Import BinInt BinNat BinPos.
Context {R eq zero one opp add sub mul}
{ring:@Hierarchy.ring R eq zero one opp add sub mul}
{zpzf:@Hierarchy.is_zero_product_zero_factor R eq zero mul}.
Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul.
Inductive coef :=
| Coef_one
| Coef_opp (_:coef)
| Coef_add (_ _:coef)
| Coef_mul (_ _:coef).
Fixpoint denote (c:coef) : R :=
match c with
| Coef_one => one
| Coef_opp c => opp (denote c)
| Coef_add c1 c2 => add (denote c1) (denote c2)
| Coef_mul c1 c2 => mul (denote c1) (denote c2)
end.
Fixpoint CtoZ (c:coef) : Z :=
match c with
| Coef_one => Z.one
| Coef_opp c => Z.opp (CtoZ c)
| Coef_add c1 c2 => Z.add (CtoZ c1) (CtoZ c2)
| Coef_mul c1 c2 => Z.mul (CtoZ c1) (CtoZ c2)
end.
Let of_Z := (@Ring.of_Z R zero one opp add).
Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c.
Proof using ring.
induction c; simpl CtoZ; simpl denote;
repeat (rewrite_hyp ?* || Ring.push_homomorphism of_Z); reflexivity.
Qed.
(* TODO: move *)
Lemma nonzero_of_Z_abs z : of_Z (Z.abs z) <> zero <-> of_Z z <> zero.
Proof using ring.
destruct z; simpl Z.abs; [reflexivity..|].
simpl of_Z. setoid_rewrite opp_zero_iff. reflexivity.
Qed.
Section WithChar.
Context C (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C) (HC: Pos.lt xH C).
Definition is_factor_nonzero (n:N) : bool :=
match n with N0 => false | N.pos p => BinPos.Pos.ltb p C end.
Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true)
: of_Z (Z.of_N n) <> zero.
Proof using char_ge_C.
destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_ge_C, Pos.ltb_lt, refl.
Qed.
Lemma RZN_product_nonzero l (H : forall x : N, List.In x l -> of_Z (Z.of_N x) <> zero)
: of_Z (Z.of_N (List.fold_right N.mul 1%N l)) <> zero.
Proof using HC char_ge_C ring zpzf.
rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right.
{ eapply char_ge_C; assumption. }
{ rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism of_Z.
eapply Ring.nonzero_product_iff_nonzero_factor; eauto. }
Qed.
Definition is_constant_nonzero (z:Z) : bool :=
match factorize_or_fail (Z.abs_N z) with
| Some factors => List.forallb is_factor_nonzero factors
| None => false
end.
Lemma is_constant_nonzero_correct z (refl:Logic.eq (is_constant_nonzero z) true)
: of_Z z <> zero.
Proof using HC char_ge_C ring zpzf.
rewrite <-nonzero_of_Z_abs, <-Znat.N2Z.inj_abs_N.
repeat match goal with
| _ => progress cbv [is_constant_nonzero] in *
| _ => progress break_match_hyps; try congruence; []
| _ => progress rewrite ?List.forallb_forall in *
|H:_|-_ => apply product_factorize_or_fail in H; rewrite <- H in *
| _ => solve [eauto using RZN_product_nonzero, is_factor_nonzero_correct]
end.
Qed.
Fixpoint is_nonzero (c:coef) : bool :=
match c with
| Coef_one => true
| Coef_opp c => is_nonzero c
| Coef_mul c1 c2 => andb (is_nonzero c1) (is_nonzero c2)
| _ => is_constant_nonzero (CtoZ c)
end.
Lemma is_nonzero_correct' c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero.
Proof using HC char_ge_C ring zpzf.
induction c;
repeat match goal with
| H:_|-_ => progress rewrite Bool.andb_true_iff in H; destruct H
| H:_|-_ => progress apply is_constant_nonzero_correct in H
| _ => progress (unfold is_nonzero in *; fold is_nonzero in * )
| _ => progress (change (denote (Coef_one)) with (of_Z 1) in * )
| _ => progress (change (denote (Coef_opp c)) with (opp (denote c)) in * )
| _ => progress (change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * )
| |- (opp _ <> zero)%type => setoid_rewrite Ring.opp_zero_iff
| |- (mul _ _ <> zero)%type => eapply Ring.nonzero_product_iff_nonzero_factor
| _ => solve [eauto using is_constant_nonzero_correct, Pos.le_1_l]
| _ => progress rewrite <-CtoZ_correct
end.
Qed.
End WithChar.
Lemma is_nonzero_correct
C
(char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C)
c (refl:Logic.eq (andb (Pos.ltb xH C) (is_nonzero C c)) true)
: denote c <> zero.
Proof using ring zpzf.
rewrite Bool.andb_true_iff in refl; destruct refl.
eapply @is_nonzero_correct'; try apply Pos.ltb_lt; eauto.
Qed.
End ReflectiveNsatzSideConditionProver.
Ltac reify one opp add mul x :=
match x with
| one => constr:(Coef_one)
| opp ?a =>
let a := reify one opp add mul a in
constr:(Coef_opp a)
| add ?a ?b =>
let a := reify one opp add mul a in
let b := reify one opp add mul b in
constr:(Coef_add a b)
| mul ?a ?b =>
let a := reify one opp add mul a in
let b := reify one opp add mul b in
constr:(Coef_mul a b)
end.
End _LargeCharacteristicReflective.
Ltac solve_constant_nonzero :=
match goal with
| |- not (?eq ?x _) =>
let cg := constr:(_:Ring.char_ge (eq:=eq) _) in
match type of cg with
@Ring.char_ge ?R eq ?zero ?one ?opp ?add ?sub ?mul ?C =>
let x' := _LargeCharacteristicReflective.reify one opp add mul x in
let x' := constr:(@_LargeCharacteristicReflective.denote R one opp add mul x') in
change (not (eq x' zero));
apply (_LargeCharacteristicReflective.is_nonzero_correct(eq:=eq)(zero:=zero) C cg);
(vm_cast_no_check (eq_refl true))
end
end.
End IntegralDomain.
(** Tactics for polynomial equations over integral domains *)
Require Coq.nsatz.Nsatz.
Ltac dropAlgebraSyntax :=
cbv beta delta [
Algebra_syntax.zero
Algebra_syntax.one
Algebra_syntax.addition
Algebra_syntax.multiplication
Algebra_syntax.subtraction
Algebra_syntax.opposite
Algebra_syntax.equality
Algebra_syntax.bracket
Algebra_syntax.power
] in *.
Ltac dropRingSyntax :=
dropAlgebraSyntax;
cbv beta delta [
Ncring.zero_notation
Ncring.one_notation
Ncring.add_notation
Ncring.mul_notation
Ncring.sub_notation
Ncring.opp_notation
Ncring.eq_notation
] in *.
Ltac nsatz := Algebra.Nsatz.nsatz; dropRingSyntax.
|
