10.4 Some Useful Tools for Writing Tactics
When the implementation of a tactic is not a straightforward combination of tactics and tacticals, the module Tacmach provides several useful functions for handling goals, calling the type-checker, parsing terms, etc. This module is intended to be the interface of the proof engine for the user.- val Tacmach.pf_hyps : goal sigma -> constr signature.
Projects the local typing context G from a given goal G |- ?:G. - val pf_concl : goal sigma -> constr.
Projects the conclusion G from a given goal G |- ?:G. - val Tacmach.pf_nth_hyp : goal sigma -> int -> identifier *
constr.
Projects the ith typing constraint xi:Ai from the local context of the given goal. - val Tacmach.pf_fexecute : goal sigma -> constr -> judgement.
Given a goal whose local context is G and a term a, this function infers a type A and a kind K such that the judgement a:A:K is valid under G, or raises an exception if there is no such judgement. A judgement is just a record type containing the three terms a, A and K. - val Tacmach.pf_infexecute :
goal sigma -> constr -> judgement * information.
In addition to the typing judgement, this function also extracts the Fw program underlying the term. - val Tacmach.pf_type_of : goal sigma -> constr -> constr.
Infers a term A such that G |- a:A for a given term a, where G is the local typing context of the goal. - val Tacmach.pf_check_type : goal sigma -> constr -> constr -> bool.
This function yields a type A if the two given terms a and A verify G |- a:A in the local typing context G of the goal. Otherwise, it raises an exception. - val Tacmach.pf_constr_of_com : goal sigma -> CoqAst.t -> constr.
Transforms an abstract syntax tree into a well-typed term of the language of constructions. Raises an exception if the term cannot be typed. - val Tacmach.pf_constr_of_com_sort : goal sigma -> CoqAst.t -> constr.
Transforms an abstract syntax tree representing a type into a well-typed term of the language of constructions. Raises an exception if the term cannot be typed. - val Tacmach.pf_parse_const : goal sigma -> string -> constr.
Constructs the constant whose name is the given string. - val
Tacmach.pf_reduction_of_redexp :
goal sigma -> red_expr -> constr -> constr.
Applies a certain kind of reduction function, specified by an element of the type red_expr. - val Tacmach.pf_conv_x : goal sigma -> constr -> constr -> bool.
Test whether two given terms are definitionally equal.
10.4.1 Patterns
The Ocmal file Pattern provides a quick way for describing a term pattern and performing second-order, binding-preserving, matching on it. Patterns are described using an extension of Coq's concrete syntax, where the second-order meta-variables of the pattern are denoted by indexed question marks.Patterns may depend on constants, and therefore only to make have sense when certain theories have been loaded. For this reason, they are stored with a module-marker, telling us which modules have to be open in order to use the pattern. The following functions can be used to store and retrieve patterns form the pattern table:
- val Pattern.make_module_marker : string list -> module_mark.
Constructs a module marker from a list of module names. - val Pattern.put_pat : module_mark -> string -> marked_term.
Constructs a pattern from a parseable string containing holes and a module marker. - val Pattern.somatches : constr -> marked_term-> bool.
Tests if a term matches a pattern. - val dest_somatch : constr -> marked_term -> constr list.
If the term matches the pattern, yields the list of sub-terms matching the occurrences of the pattern variables (ordered from left to right). Raises a UserError exception if the term does not match the pattern. - val Pattern.soinstance : marked_term -> constr list -> constr.
Substitutes each hole in the pattern by the corresponding term of the given the list.
Warning:
Sometimes, a Coq term may have invisible sub-terms that the matching functions are nevertheless sensible to. For example, the Coq term (?1,?2) is actually a shorthand for the expression ( pair ? ? ?1 ?2). Hence, matching this term pattern with the term ( true, O) actually yields the list [?;?; true; O] as result (and not [ true; O], as could be expected).10.4.2 Patterns on Inductive Definitions
The module Pattern also includes some functions for testing if the definition of an inductive type satisfies certain properties. Such functions may be used to perform pattern matching independently from the name given to the inductive type and the universe it inhabits. They yield the value ( Some r::l) if the input term reduces into an application of an inductive type r to a list of terms l, and the definition of r satisfies certain conditions. Otherwise, they yield the value None.- val Pattern.match_with_non_recursive_type : constr list option.
Tests if the inductive type r has no recursive constructors - val Pattern.match_with_disjunction : constr list option.
Tests if the inductive type r is a non-recursive type such that all its constructors have a single argument. - val Pattern.match_with_conjunction : constr list option.
Tests if the inductive type r is a non-recursive type with a unique constructor. - val Pattern.match_with_empty_type : constr list option.
Tests if the inductive type r has no constructors at all - val Pattern.match_with_equation : constr list option.
Tests if the inductive type r has a single constructor expressing the property of reflexivity for some type. For example, the types a=b, A==B and A===B satisfy this predicate.
10.4.3 Elimination Tacticals
It is frequently the case that the subgoals generated by an elimination can all be solved in a similar way, possibly parametrized on some information about each case, like for example:- the inductive type of the object being eliminated;
- its arguments (if it is an inductive predicate);
- the branch number;
- the predicate to be proven;
- the number of assumptions to be introduced by the case
- the signature of the branch, i.e., for each argument of the branch whether it is recursive or not.
The following tacticals can be useful to deal with such situations. They
- val Elim.simple_elimination_then :
(branch_args -> tactic) -> constr -> tactic.
Performs the default elimination on the last argument, and then tries to solve the generated subgoals using a given parametrized tactic. The type branch_args is a record type containing all information mentioned above. - val Elim.simple_case_then :
(branch_args -> tactic) -> constr -> tactic.
Similarly, but it performs case analysis instead of induction.