18.2 Using Program

18.2 Using Program

The user has to give two things: the specification (given as usual by a goal) and the program (see section 18.3). Then, this program is associated to the current goal (to know which specification it corresponds to) and the user can use different tactics to develop an automatic proof.

18.2.1 Realizer term.

This command attaches a program term to the current goal. This is a necessary step before applying the first time the tactic Program. The syntax of programs is given in section 18.3. If a program is already attached to the current subgoal, Realizer can be also used to change it.

18.2.2 Show Program.

The command Show Program shows the program associated to the current goal. The variant Show Program n shows the program associated to the nth subgoal.

18.2.3 Program.

This tactics tries to build a proof of the current subgoal from the program associated to the current goal. This tactic performs Intros then either one Apply or one Elim depending on the syntax of the program. The Program tactic generates a list of subgoals which can be either logical or informative. Subprograms are automatically attached to the informative subgoals.

When attached program are not automatically generated, an initial program has to be given by Realizer.


Error messages:
  1. No program associated to this subgoal
    You need to attach a program to the current goal by using Realizer. Perhaps, you already attached a program but a Restart or an Undo has removed it.
  2. Type of program and informative extraction of goal do not coincide
  3. Cannot attach a realizer to a logical goal
    The current goal is non informative (it lives in the world Prop of propositions or Type of abstract sets) while it should lives in the world Set of computational objects.
  4. Perhaps a term of the Realizer is not an FW term and you then have
    to replace it by its extraction
    Your program contains non informative subterms.



Variants:
  1. Program_all.
    This tactic is equivalent to the composed tactic Repeat (Program OrElse Auto). It repeats the Program tactic on every informative subgoal and tries the Auto tactic on the logical subgoals. Note that the work of the Program tactic is considered to be finished when all the informative subgoals have been solved. This implies that logical lemmas can stay at the end of the automatic proof which have to be solved by the user.
  2. Program_Expand
    The Program_Expand tactic transforms the current program into the same program with the head constant expanded. This tactic particularly allows the user to force a program to be reduced before each application of the Program tactic.
    Error messages:
    1. Not reducible
      The head of the program is not a constant or is an opaque constant. need to attach a program to the current goal by using Realizer. Perhaps, you already attached a program but a Restart or an Undo has removed it.


18.2.4 Hints for Program

Mutual inductive types
The Program tactic can deal with mutual inductive types. But, this needs the use of annotations. Indeed, when associating a mutual fixpoint program to a specification, the specification is associated to the first (the outermost) function defined by the fixpoint. But, the specifications to be associated to the other functions cannot be automatically derived. They have to be explicitly given by the user as annotations. See section 18.4.5 for an example.
Constants
The Program tactic is very sensitive to the status of constants. Constants can be either opaque (their body cannot be viewed) or transparent. The best of way of doing is to leave constants opaque (this is the default). If it is needed after, it is best to use the Transparent command after having used the Program tactic.


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.7.1.html at 8/10/98