Build Why3 with Coq support

[suhr]

Right now creusot-install builds Why3 without Coq support, even if Coq is installed in the system.

[Lysxia]

You can install Coq in Creusot's switch and it will stay there:

opam install --switch ~/.local/share/creusot coq

That said our current stance is to encourage making proofs automatable with why3find. I'd be interested in hearing about cases where that is difficult, and see if we can handle them in other ways than supporting Why3 transformations or Coq proofs.

[suhr]

Why3 documentation says that Coq must be installed before building Why3:

If you want to use the Coq realizations (Section 10.2), then Coq has to be installed before Why3. Look at the summary printed at the end of the configuration script to check if Coq has been detected properly. Similarly, in order to use PVS (Section 10.5) or Isabelle (Section 10.4) to discharge proofs, PVS and Isabelle must be installed before Why3. You should check that those proof assistants are correctly detected by the configure script.

(https://www.why3.org/doc/install.html)

I'd be interested in hearing about cases where that is difficult, and see if we can handle them in other ways than supporting Why3 transformations or Coq proofs.

To investigate why a particular invariant does not work. In Why3, the only way to debug an invariant is to read a rather unreadable goal. While in a proof assistant, I could simplify the goal and try to prove it yourself to figure out why it's not provable.

[Lysxia]

That's a quote from the instructions for installing from source. On opam you can install why3-coq independently.

(I previously thought installing Coq would rebuild Why3 for Coq support, but instead installing why3-coq seems to be the way to go.)

[suhr]

I see, thanks. Though opam install --switch ~/.local/share/creusot why3-coq does not work, because it requires why3 <= 1.8.0.

[Lysxia]

Run opam update to refresh opam's package database. nevermind

[Lysxia]

Now that I think about it, you may want manage the installation of Why3 and Coq manually with a global opam switch instead, because it will make it less of a hassle to work with Coq (notably for editor extensions to find it):

opam install why3 why3find why3-ide why3-coq
./INSTALL --external why3-and-why3find

[suhr]

I guess I need to patch creusot-deps.opam, so it does not use git versions of packages for which there's no why3-coq version.

[claudemarche]

I'd be interested in hearing about cases where that is difficult, and see if we can handle them in other ways than supporting Why3 transformations or Coq proofs.

To investigate why a particular invariant does not work. In Why3, the only way to debug an invariant is to read a rather unreadable goal. While in a proof assistant, I could simplify the goal and try to prove it yourself to figure out why it's not provable.

Notice that in Why3 IDE, you can also manually apply some transformations and simplifications to do what what you want, that is to figure out why an invariant is not provable.

That being said, I would certainly agree that when you have the knowledge of a proof assistant, like Coq, you would prefer to do that with that particular assistant.

And a final remark: it is true that Why3 currently does not offer Lean as a back-end, but we would certainly be happy to accept patches to make it work!

[suhr]

And a final remark: it is true that Why3 currently does not offer Lean as a back-end, but we would certainly be happy to accept patches to make it work!

I'm familiar with Lean but I'm not familiar with Why3 codebase. So I don't know where to start.

[ia0]

To investigate why a particular invariant does not work. In Why3, the only way to debug an invariant is to read a rather unreadable goal. While in a proof assistant, I could simplify the goal and try to prove it yourself to figure out why it's not provable.

Notice that in Why3 IDE, you can also manually apply some transformations and simplifications to do what what you want, that is to figure out why an invariant is not provable.

I don't see any transformation to evaluate the goal and context as seen in the "Task" tab, which is what I understand by "simplify the goal" as stated above, and which is what I would like to have (and do have in Coq).

To take a concrete example, I have a VC that doesn't verify, so I look at the Task tab to figure out if I can prove the goal from the hypotheses or if a necessary hypothesis is missing. In this tab, I can see hypotheses like:

Assert6 :
  exists g:closure13'1.
   postcondition_mut'0
   (closure13'1'mk input field_0 (t'mk (output.current) fin id)) () g () /\
   resolve'5 g

I would like to unfold postcondition_mut'0 definition and simplify this proposition through evaluation of that predicate. Currently I have to do it in my head, which requires a bit of gymnastic and effort. In Coq it's just a matter of unfold postcondition_mut'0 in Assert6.

Is it possible to do such simplifications in the Task tab and figure out if the provers have enough hypotheses to prove the goal? Otherwise what's the recommended approach for such cases? Currently I just add a proof_assert!() for each hypothesis I can think of that is necessary. This helps discriminate between:

• All hypotheses are verified but the goal still doesn't, then the provers need some help (maybe a trigger annotation).
• The goal and all hypotheses are verified, then one or more of those proof_assert!() is helpful to the provers.
• The goal is verified but one or more hypotheses don't (the most common case), then I'm progressing toward the root cause and can recurse the process on that failed hypothesis. Usually some loop invariant or postcondition is missing.

[claudemarche]

To take a concrete example, I have a VC that doesn't verify, so I look at the Task tab to figure out if I can prove the goal from the hypotheses or if a necessary hypothesis is missing. In this tab, I can see hypotheses like:

Assert6 :
  exists g:closure13'1.
   postcondition_mut'0
   (closure13'1'mk input field_0 (t'mk (output.current) fin id)) () g () /\
   resolve'5 g

I would like to unfold postcondition_mut'0 definition and simplify this proposition through evaluation of that predicate. Currently I have to do it in my head, which requires a bit of gymnastic and effort. In Coq it's just a matter of unfold postcondition_mut'0 in Assert6.

I would certainly admit that the set of available transformations in Why3 is not as rich as the set of tactics of Coq, but that case is not a good example at all : just go into the "command line" in the IDE and type exactly unfold postcondition_mut'0 in Assert6 and it will do what you expect

In this short command line style input there is a completion facility, so if you type a few characters it will list you the set of transformations that starts with them.

The list of all Why3 transformations is documented here.

[ia0]

just go into the "command line" in the IDE

Thanks! That's what I was missing. I've only read the doc of the IDE here which doesn't mention the "command line in the IDE", and I didn't notice it either.

I'll have to test it when I'm on my computer but that should solve my problem, which I assume is the same as #1393 (comment), namely being able to read a VC to figure out if it's at all provable or if Creusot did not add a hypothesis that should be there, either because of a limitation in Creusot or because I actually forgot a non-trivial invariant. The goal is not to transform the VC to prove it in Why3 (or Coq), only to understand it.

[xldenis]

Another tactic I like is compute_specified which produces results a lot like simp. Generally it makes goals a lot more readable.