Subject: Tactics

Keywords: ::tactic

Title: Basic tactics

--------------------------------------------------
This page contains a rough comparison between Nuprl's and Coq's
basic tactics.  In Nuprl, hypotheses are numbered in addition
to having names, so one can refer to an hypothesis by its name or
by its number.  We use number 0 to refer to the conclusion.
If a sequent has 10 hypotheses, they would be numbered 1 to 10
starting from the top.  Hypothesis 10 can also be refered to as
hypothesis (-1), hypothesis 9 as (-2), ...

Nuprl's basic tactics refer to hypotheses by their numbers.

(In the following table, n is a Nuprl hypothesis number,
h a Coq hypothesis name, and t is a Nuprl or Coq term.)

              Nuprl            |             Coq
----------------------------------------------------------------
Auto                           | auto (with lots of builtin hints)
Auto'                          | omega followed by auto
D n                            | destruct h
InstConcl [t1;...;tn]          | exists t1 ... tn
Intro/D 0                      | intro
Intros/UnivCD                  | intros
RenameVar `v' n                | rename h into v
InstLemma `name' [t1;...;tn]   | pose proof (name t1 ... tn)
FLemma `name' [n1;...;nn]      | eapply name in hi
BLemma `name'                  | apply name
OrLeft                         | left
OrRight                        | right
Assert t                       | assert t
RWO "name" n                   | rewrite name in h
RWO "name<" n                  | rewrite <- name in h
RWW "name" n                   | repeat (rewrite name in h)
HypSubst n1 n2                 | rewrite h1 in h2
Subst ⌜t1 = t2⌝ n              | assert (t1 = t2) as e;[|rewrite e in h]
Reduce n                       | simpl in n
Repeat tac                     | repeat tac
tac1 THEN tac2                 | tac1; tac2
tac THENL [tac1;...;tacn]      | tac1; [ tac1 | ... | tacn ]
EqCD                           | f_equal
EqHD n                         | inversion h
ExRepD                         | Repeat of destruct ands and exists
D 0                            | split
NatInd n                       | induction h
InductionOnNat                 | induction k, where k is the first quantified nat


Nuprl tactics tag certain subgoals as auxiliary.  Examples of auxiliary
"tags" are "wf", "aux", and "antecedent".  Well-formedness subgoals are
typically tagged with "wf".
For example, when instantiating a lemma of the form ⌜∀n:ℕ. (P[n] ⇒ Q[n])⌝
with term ⌜t⌝, one has to prove the well-formedness subgoal ⌜t ∈ ℕ⌝ and
the auxiliary subgoal ⌜P[t]⌝.  These subgoals are labelled "wf" and
"antecedent" respectively.
Therefore, a useful tactic in Nuprl is

    tac THENA Auto

(Auto could be any tactic), which applies the Auto tactics to all auxiliary
subgoals.
⋅
--------------------------------------------------

Authors: 

Contributors: VINCENT:t

⋅

Home