Subject: Tactics

Keywords: ::tactic

Title: Basic tactics

--------------------------------------------------
This page contains 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 to refer to the conclusion.
If sequent has 10 hypotheses, they would be numbered to 10
starting from the top.  Hypothesis 10 can also be refered to as
hypothesis (-1), hypothesis as (-2), ...

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

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

              Nuprl            |             Coq
----------------------------------------------------------------
Auto                           auto (with lots of builtin hints)
Auto'                          omega followed by auto
n                            destruct h
InstConcl [t1;...;tn]          exists t1 ... tn
Intro/D 0                      intro
Intros/UnivCD                  intros
RenameVar `v' n                rename 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 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
0                            split
NatInd n                       induction h
InductionOnNat                 induction k, where 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 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, 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