18.3 Syntax for programs
18.3.1 Pure programs
The language to express programs is called Real(It corresponds to Fw plus inductive definitions). Programs are explicitly typed(This information is not strictly needed but was useful for type checking in a first experiment.) like terms extracted from proofs. Some extra expressions have been added to have a simpler syntax.This is the raw form of what we call pure programs. But, in fact, it appeared that this simple type of programs is not sufficient. Indeed, all the logical part useful for the proof is not contained in these programs. That is why annotated programs are introduced.
18.3.2 Annotated programs
The notion of annotation introduces in a program a logical assertion that will be used for the proof. The aim of theProgram tactic
is to start from a specification and a program and to generate
subgoals either logical or associated with programs. However, to find
the good specification for subprograms is not at all trivial in
general. For instance, if we have to find an invariant for a loop, or
a well founded order in a recursive call.So, annotations add in a program the logical part which is needed for the proof and which cannot be automatically retrieved. This allows the system to do proofs it could not do otherwise.
For this, a particular syntax is needed which is the following: since they are specifications, annotations follow the same internal syntax as Coq terms. We indicate they are annotations by putting them between
{ and } and preceding them with :: ::.
Since annotations are Coq terms, they can involve abstractions over
logical propositions that have to be declared. Annotated-l
have to be written between [{ and }].
Annotated-l can be seen like usual l-bindings but
concerning just annotations and not Coq programs.18.3.3 Recursive Programs
Programs can be recursively defined using the following syntax:<type-of-the-result> rec name-of-the-induction-hypothesis :: :: { well-founded-order-of-the-recursion } and then the body of
the program (see section 18.4) which must always begin with
an abstraction [x:A] where A is the type of the arguments of the
function (also on which the ordering relation acts).18.3.4 Implicit arguments
A synthesis of implicit arguments has been added in order to allow the user to write a minimum of types in a program. Then, it is possible not to write a type inside a program term. This type has then to be automatically synthesized. For this, it is necessary to indicate where the implicit type to be synthesized appears. The syntax is the current one of implicit arguments in Coq: the question mark?. This synthesis of implicit arguments is not possible everywhere in a program. In fact, the synthesis is only available inside a
Match, a Cases or a Fix construction (where
Fix is a syntax for defining fixpoints).18.3.5 Grammar
The grammar for programs is described in figure 18.1.
pgm ::= ident | ? | [ ident : pgm ] pgm | [ ident ] pgm | ( ident : pgm ) pgm | ( pgms ) | Match pgm with pgms end | <pgm>Match pgm with pgms end| Cases pgm of [equation | ... | equation] end | <pgm>Cases pgm of [equation | ... | equation] end| Fix ident {fix_pgm with ... with fix_pgm}| Cofix ident {ident : pgm := pgm with ... with ident : pgm := pgm} | pgm :: :: {term } | [{ ident : term }] pgm | let ( ident , ... , ident , ... , ident ) = pgm in pgm | <pgm>let ( ident , ... , ... , ident ) = pgm in pgm| if pgm then pgm else pgm | <pgm>if pgm then pgm else pgm| <pgm>rec ident :: :: {term}[ ident : pgm ] pgmpgms ::= pgm | pgm pgms fix_pgm ::= ident [ typed_idents ; ... ; typed_idents ] : pgm := pgm | ident / num : pgm := pgm :: :: {term } simple_pattern ::= ident | (ident ... ident)equation ::= simple_pattern =>pgm
Figure 18.1:Syntax of annotated programs
As for Coq terms (see section 1.2), (pgms) associates to the left. The syntax of term is the one in section. The infix annotation operator
:: :: binds more than the
abstraction and product constructions.
1.2.The reference to an identifier of the Coq context (in particular a constant) inside a program of the language Real is a reference to its extracted contents.