diff options
author | amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 15:34:09 +0000 |
---|---|---|
committer | amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 15:34:09 +0000 |
commit | 80f974b1cc399759c5e90a653bdccc3e1d508cbd (patch) | |
tree | 9cc175788e7f539fc8694e1c9bd812eebb98415d /plugins/setoid_ring/ZArithRing.v | |
parent | f6d8fc17dc9474e4d043cf709d672d9259599354 (diff) |
Fixing a significant efficiency leak in the code of the field tactic.
The field tactic post-processes the data generated during normalization
to ensure that vanished denominators do not cancel: essentially, this
step removes duplicates from a list of polynomials and uses the
clean list to generate the conjunction of associated non-zero conditions. This
conjunction is the proof obligation the user has to prove by hand after
a successful call to the field tactic.
The computation of the proof obligation statement
was performed using a fine-tuned reduction strategy, coded in
the newring.ml4 file (see the fv-protect tactic).
However, not only this strategy information was forgotten by the kernel,
but the strategy used at Qed time caused a real explosion (examples
normalized in 70s by the tactic have a one hour Qed). No idea why.
The fix consists in opacifying the part of the goal irrelevant to
computation and call the vm on the duplicate removal step. BTW this step
is programmed in a naive way and can probably be made more efficient.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16728 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring/ZArithRing.v')
0 files changed, 0 insertions, 0 deletions