Le 16/05/2019 à 13:38, Jean-Jacques Levy a écrit :
1- assertions around ‘if-statement’ keep the conditional in the logic. In previous 0.88.3, they were splitted around the two branches of the if-statement. Now the provers have to go through the predicate of the if-statement. In command-line, I tried to use a ‘case’ command, but did not seem to help the provers. Same with various ‘split’.. I miss a ‘simplify’ command which would normalize (ie erase) the condition in the two branches?
I cannot think of a good solution. I would have thought that "eliminate_if" would do the trick, but the formula it produces is not suitable for splitting. (It is basically the same formula as the one obtained by "split_all_full".)
2- for records with 0.88.3, there was an automatic inversion (in Coq sense) which could help the provers. No longer inversion in 1.2.0. I think that’s also making impossible automatic proofs.
Do you have a testcase?
Here are few minor extra-points: - is there an intuition between the suffixes ‘.._spec’ or ‘.._def’ in names for the Why3-Coq ?
When doing a standard proof, "_def" is used when translating a partial function whose body can be translated into the logic. The axiom is of the form "forall x. requires x -> foo x = ...". If the function is not partial, there is just a definition and no axiom.
As for "_spec", it is used when translating a function with a postcondition. The axiom is of the form "forall x. requires x -> ensures (foo x)".
When doing a realization, "_def" is used when proving the extensional equality between a function defined in Why3 and the corresponding notation written in the driver file.
- ‘mem-empty’ lemma seems also hard to use in Coq. It took me long time to redefine it.
What is the issue? (Note that it won't exist anymore in the next version of Why3.)
- where is documentation for ‘why_decidable_eq' in Coq? maybe it also blocks the automatic provers.
It can be found in lib/coq/BuiltIn.v. It just characterizes that equality on any Why3 type is strongly decidable. It should have absolutely no impact on automatic provers.
Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
