Notación:    E(G) |-  t:T significa que el término t está bien tipado y tiene tipo T en el
entorno E y contexto G.
WF(E) [G] significa que el entorno E está bien formado y que el contexto G es válido
en este entorno.


 
Ejemplo: táctica Assumption:
Mira en el contexto local si hay una hipótesis con tipo igual que el objetivo:

Coq < Variable A:Prop.
A is assumed
Coq < Lemma var: A->A.
1 subgoal

  ============================
   A->A
var < Intro.
1 subgoal
  H : A
  ============================
   A
var < Assumption.
Subtree proved!
 



 
Ejemplo: táctica Intro:

Variable P,Q:nat->Prop.
P is assumed
Q is assumed
Variable R:nat->nat->Prop.
R is assumed
Lemma PQR:(x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y) ->(Q x).
1 subgoal

  ==========================
(x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)->(Q x)
Intros.
1 subgoal

  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (Q x)



 
Por ejemplo, la táctica Apply t con el objetivo T nos provee del subgoal U. En general, si el objetivo es T y H es una hipótesis de nuestro entorno H:U1->U2->....Un->T, entonces Apply H nos remite a los subobjetivos U1,...,Un.

Goal (A,B:Prop)A->(A->B)->B.
1 subgoal

  ============================
   (A,B:Prop)A->(A->B)->B

Unnamed_thm < Intros.
1 subgoal

  A : Prop
  B : Prop
  H : A
  H0 : A->B
  ============================
   B

Unnamed_thm < Apply H0.
1 subgoal

  A : Prop
  B : Prop
  H : A
  H0 : A->B
  ============================
   A

Unnamed_thm < Assumption.
Subtree proved!

Unnamed_thm < Qed.
Intros.
Apply H0.
Assumption.

Unnamed_thm is defined

Coq < Print Unnamed_thm.
Unnamed_thm =
[A,B:Prop][H:A][H0:A->B](H0 H)
     : (A,B:Prop)A->(A->B)->B
 
 

También, se tiene la táctica Cut.
Si tenemos la situación siguiente:
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (P x)->(Q x)

PQR < Cut (R x x).
2 subgoals

  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (R x x)->(P x)->(Q x)

subgoal 2 is:
 (R x x)


                              E[G]|- U:S     E[G]|- t:T   T£ bdi U
Regla Conv           --------------------------------------
                                              E(G) |-  t:U

Ejemplo: táctica Change : si partimos de:
 
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (Q x)

PQR < Change (([n:nat](Q n)) x).
1 subgoal

  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   ([n:nat](Q n) x)