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
|
(* This is a rewrite of the Ltac parts of standard library nsatz. We should
periodically check whether we still need it -- once enough bugs get fixed
in mailine, we hope to drop this implementation *)
Require Coq.nsatz.Nsatz.
Require Import Coq.Lists.List.
Generalizable All Variables.
Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
: forall x y, eq (sub x y) zero <-> eq x y.
Proof.
split;intros Hx.
{ eapply Nsatz.psos_r1b. eapply Hx. }
{ eapply Nsatz.psos_r1. eapply Hx. }
Qed.
Ltac get_goal := lazymatch goal with |- ?g => g end.
Ltac nsatz_equation_implications_to_list eq zero g :=
lazymatch g with
| eq ?p zero => constr:(p::nil)
| eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l)
end.
Ltac nsatz_reify_equations eq zero :=
let g := get_goal in
let lb := nsatz_equation_implications_to_list eq zero g in
lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with
(?variables, ?le) =>
lazymatch (eval compute in (List.rev le)) with
| ?reified_goal::?reified_givens => constr:((variables, reified_givens, reified_goal))
end
end.
Ltac nsatz_get_free_variables reified_package :=
lazymatch reified_package with (?fv, _, _) => fv end.
Ltac nsatz_get_reified_givens reified_package :=
lazymatch reified_package with (_, ?givens, _) => givens end.
Ltac nsatz_get_reified_goal reified_package :=
lazymatch reified_package with (_, _, ?goal) => goal end.
Require Import Coq.setoid_ring.Ring_polynom.
(* Kludge for 8.4/8.5 compatibility *)
Module Import mynsatz_compute.
Import Nsatz.
Global Ltac mynsatz_compute x := nsatz_compute x.
End mynsatz_compute.
Ltac nsatz_compute x := mynsatz_compute x.
Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens :=
nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
Ltac nsatz_compute_get_leading_coefficient :=
lazymatch goal with
|- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a
end.
Ltac nsatz_compute_get_certificate :=
lazymatch goal with
|- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:((c,b))
end.
Ltac nsatz_rewrite_and_revert domain :=
lazymatch type of domain with
| @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
lazymatch goal with
| |- eq _ zero => idtac
| |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring))
end;
repeat match goal with
| [H : eq _ zero |- _ ] => revert H
| [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H
end
end.
(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz]
cannot handle duplicate hypotheses. So we clear them. *)
Ltac nsatz_clear_duplicates_for_bug_4851 domain :=
lazymatch type of domain with
| @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ =>
repeat match goal with
| [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H'
end
end.
Ltac nsatz_nonzero :=
try solve [apply Integral_domain.integral_domain_one_zero
|apply Integral_domain.integral_domain_minus_one_zero
|trivial
|assumption].
Ltac nsatz_domain_sugar_power domain sugar power :=
let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *)
lazymatch type of domain with
| @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
nsatz_clear_duplicates_for_bug_4851 domain;
nsatz_rewrite_and_revert domain;
let reified_package := nsatz_reify_equations eq zero in
let fv := nsatz_get_free_variables reified_package in
let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
let reified_givens := nsatz_get_reified_givens reified_package in
let reified_goal := nsatz_get_reified_goal reified_package in
nsatz_compute_to_goal sugar nparams reified_goal power reified_givens;
let a := nsatz_compute_get_leading_coefficient in
let crt := nsatz_compute_get_certificate in
intros _ (* discard [nsatz_compute] output *); intros;
apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
[ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
| solve [vm_cast_no_check (eq_refl true)] (* if this fails, the prover returned a bad certificate *)
| solve [repeat (split; [assumption|]); exact I] ]
end.
Ltac nsatz_guess_domain :=
match goal with
| |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
| |- not (?eq _ _) => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
| [H: ?eq _ _ |- _ ] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
| [H: not (?eq _ _) |- _] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
end.
Ltac nsatz_sugar_power sugar power :=
let domain := nsatz_guess_domain in
nsatz_domain_sugar_power domain sugar power.
Ltac nsatz_power power :=
let power_N := (eval compute in (BinNat.N.of_nat power)) in
nsatz_sugar_power BinInt.Z0 power_N.
Ltac nsatz := nsatz_power 1%nat.
Tactic Notation "nsatz" := nsatz.
Tactic Notation "nsatz" constr(n) := nsatz_power n.
(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y]
contradicts any hypothesis of the form [?x' <> ?y'], we turn this
problem about inequalities into one about equalities and give it
to [nsatz]. *)
Ltac nsatz_contradict_single_hypothesis domain :=
lazymatch type of domain with
| @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
unfold not in *;
match goal with
| [ H : eq _ _ -> False |- eq _ _ -> False ]
=> intro; apply H; nsatz
| [ H : eq _ _ -> False |- False ]
=> apply H; nsatz
end
end.
Ltac nsatz_contradict :=
let domain := nsatz_guess_domain in
nsatz_contradict_single_hypothesis domain
|| (unfold not;
intros;
lazymatch type of domain with
| @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
assert (eq one zero) as Hbad;
[nsatz; nsatz_nonzero
|destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
end).
|
