3 The Proof Modes
3.1 The Interactive Mode
This is the usual way to use Coq. To access the proof obligation, in Jack's
Case Viewer click with the right button on the goal you want to prove; and
there you are, the plugin launches the Coq Ide you have chosen.
After you have edited the proof obligation it is checked with coqc and
saved inside the Jack's Jpo. If the checking succeeds; the goal is considered
solved.
An interactive poof always begins with 'Proof with autoJack.'
followed by the tactic startJack.
When you are satisfied with your proof, you have to press
the button Evaluate (E), in order to update the case explorer.
3.2 The Automatic Modes
Strangely in this plugin you can try to prove several goals automatically using
some tactics written in Ltac, namely lightAutoJack and toughAutoJack.
It uses coqtop to check the different goals.
To prove automatically there is two buttons with a coq.
3.2.1 Light Mode
To prove automatically with the light mode (this means using the tactic
lightAutoJack) you must first select a file and the
press the button which has a yellow coq over it.
3.2.2 Tough Mode
To prove automatically with the tough mode (this means using the tactic
toughAutoJack) you must first select a file and the
press the button which has a yellow coq over it.
If some proofs take too much time (indeed more seconds than the number
allowed by the grace time); coqtop is restarted.
3.3 The Semi-Automatic Mode
When you select several goals in the case viewer, and you click with the
right button you have a pop up dialog that opens with the option
'Prove automatically with > Coq (Light Mode)', in fact it is not done through
the light mode but through the Semi-Auto Mode tm.
A dialog box will appear asking you to choose a tactic to apply to the goals
you have chosen to solve automatically. You can add your own fave tactics with
the buttons add and remove.
Then press the Ok, or Cancel button (cancel solves
using the lightAutoTactic). It will try to solve the goals with the chosen
tactic.
The tactic list is stored in the file chosen in
Window > Preference > Jack > provers > Coq Prover > Location of the tactics for
the semi auto mode; one tactic per line.