PSPEC_TAC

PairRules.PSPEC_TAC : term * term -> tactic

Generalizes a goal.

When applied to a pair of terms (q,p), where p is a paired structure of variables and a goal A ?- t, the tactic PSPEC_TAC generalizes the goal to A ?- !p. t[p/q], that is, all components of q are turned into the corresponding components of p.

        A ?- t
   =================  PSPEC_TAC (q,p)
    A ?- !x. t[p/q]

Failure

Fails unless p is a paired structure of variables with the same type as q.

Example

> g `1 + 2 = 2 + 1`;
val it =
   Proof manager status: 2 proofs.
   2. Incomplete goalstack:
        Initial goal:
        ∃R. WF R ∧ (∀rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)) ∧
            ∀rst x ord. R (ord,FILTER ($¬ ∘ ord x) rst) (ord,x::rst)
   
   1. Incomplete goalstack:
        Initial goal:
        1 + 2 = 2 + 1

> e (PairRules.PSPEC_TAC (Term`(1,2)`, Term`(x:num,y:num)`));
OK..
1 subgoal:
val it =
   
   ∀(x,y). x + y = y + x

Removing unnecessary speciality in a goal, particularly as a prelude to an inductive proof.

See also

PairRules.PGEN, PairRules.PGENL, PairRules.PGEN_TAC, PairRules.PSPEC, PairRules.PSPECL, PairRules.PSPEC_ALL, PairRules.PSTRIP_TAC