diff options
author | 2014-01-10 17:22:55 +0100 | |
---|---|---|
committer | 2014-01-10 18:19:51 +0100 | |
commit | 033ffae9beb88e8b9c509cf151331f5855165f2f (patch) | |
tree | 7d58bef787a654b59a6c5000d2bc07f5a9a09461 /plugins/pluginsopt.itarget | |
parent | 6058cdf5e70822e4501c61dfd969e4746c01145b (diff) |
Omega: avoiding distinct proof-terms on repeated identical runs
Omega now reuse the same inner variable names (Zvar0, Zvar1, ...)
at each run. This way, the obtained proof-terms on
two identical omega runs should be the same.
This wasn't always the case earlier:
- the two proofs were almost always convertible, but with distinct
variable names.
- in very rare situations, the two proofs could even be non-convertible.
Indeed, the omega engine use hash-tables which may be sensible to
the names in the (in)equality system and hence lead to different
solutions. Example of this behavior (with ocaml 4, whose default hash
function is different from ocaml 3.12, leading to a different behavior
here !) :
--------------------------------------------------------------------
Require Import Omega.
Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Check (eq_refl : test1 = test2). (* OK *)
Check (eq_refl : test1 = test3). (* OK *)
Check (eq_refl : test1 = test4). (* KO, test4 is different !! *)
--------------------------------------------------------------------
The old behavior could be restored with "Unset Stable Omega".
Thanks to Frédéric Loulergue for spotting this sensibility to
the underlying ocaml versions...
Diffstat (limited to 'plugins/pluginsopt.itarget')
0 files changed, 0 insertions, 0 deletions