quantHeuristicsLib.QUANT

STRUCTURE

SYNOPSIS

A tactic to instantiate quantifiers in a term using an explitly given list of (partial) instantiations.

DESCRIPTION

This tactic can be seen as a generalisation of Q.EXISTS_TAC. When applied to a term fragment u and a goal ?x. t, the tactic EXISTS_TAC reduces the goal to t[u/x]. QUANT_TAC allows to perform similar instantiations of quantifiers at subpositions, provided the subposition occurs in a formula composed of standard operators that the tactic can handle. It can - depending on negation level - instantiate both existential and universal quantifiers. Moreover, it allows partial instantiations and instantiating multiple variables at the same time.

QUANT_TAC gets a list of triples (var_name, instantiation, free_vars) as an argument. var_name is the name of the variable to be instantiated; instantiation is the term this variable should be instantiated with. Finally, free_vars is a list of free variables in instantiation that should remain quantified.

As this tactic adresses variables by their name, resulting proofs might not be robust. Therefore, this tactic should be used carefully.

EXAMPLE

Given the goal

   !x. (!z. P x z) ==> ?a b.    Q a        b z

where z and a are natural numbers, the call QUANT_TAC [("z", `0`, []), ("a", `SUC a'`, [`a'`])] instantiates z with 0 and a with SUC a', where a' is free. The variable z is universally quantified, but in the antecedent of the implication. Therefore, it can be safely instantiated. a is existentially quantified. In this example we just want to say that a is not 0, therefore a' is considered as a free variable and thus remains existentially quantified. The call results in the goal

   !x. (    P x 0) ==> ?  b a'. Q (SUC a') b z

SEEALSO

EXISTS_TAC