Empezaremos con hechos puramente lógicos. En
Coq la cuantificación universal y la implicación están
predefinidas. Todos los demás operadores lógicos están
definidos. Todas las variables han de tener un tipo y todas las proposiciones
tienen tipo Prop.
Los objetivos o conclusiones (Goals) a probar aparecen
como:
Contexto
========
Conclusión
Un contexto es una lista de declaraciones: variables con su tipo e hipótesis con su expresión.
Ejemplo 1:
Prompt del sistema: coqtop
Welcome to Coq V6.2.2 (September
1998)
Coq < Theorem trivial:
(A: Prop) A -> A.
1 subgoal
============================
(A:Prop)A->A
trivial <
El problema consiste en "construir" un valor (un término)
para trivial con la ayuda de las
"tácticas".
La táctica Intro "empuja"
variables o hipótesis al contexto.
trivial < Intros A H';
Exact H'.
Subtree proved!
trivial < Qed.
Intros A H'; Exact H'.
trivial is defined
Coq < print trivial.
trivial = [A:Prop][H':A]H':
(A:Prop)A->A
Usar la táctica Assumption
para buscar una hipótesis cuyo tipo coincida con el objetivo.
Usar Exact <término>
si hay alguna hipótesis (término) cuyo tipo coincide con
el objetivo.
| Utilizar sólo la táctica Exact para probar este resultado en un solo paso |
Ejemplo 2:
Coq < Variables
A,B,C:Prop.
A is assumed
B is assumed
C is assumed
Coq < Goal (A->(B->C))->(A->B)->(A->C).
1 subgoal
============================
(A->B->C)->(A->B)->A->C
Unnamed_thm < Intros.
1 subgoal
H : A->B->C
H0 : A->B
H1 : A
============================
C
Utilizar solo la tactica Exact para
probar este objetivo.
| Utilizar sólo la táctica Exact para probar C |
| Completar la siquiente
demostración usando Apply y Exact.
Coq
< Theorem resolution: (p,q:Type->Prop)(a:Type)
============================
|
Ejemplo 3 (Despues de ver la lección de Tipos Inductivos)
Coq < Lemma and_commutative
: A/\B -> (B/\A).
1 subgoal
============================
A/\B->B/\A
and_commutative <
Intro.
1 subgoal
H : A/\B
============================
B/\A
and_commutative < Elim H.
1 subgoal
H : A/\B
============================
A->B->B/\A
and_conmutative
< Split.
2 subgoals
H : (and A
B)
H0 : A
H1 : B
============================
B
subgoal 2 is:
A
| En lugar de Split, podríamos haber hecho su equivalente Intros;Apply conj. Comprobarlo y terminar la demostración |
| Probar el teorema (A,B: Prop) A /\ B -> B /\ A y comparar con el anterior. |
Coq < Print or.
Inductive or [A:Prop;
B:Prop] : Prop :=
or_introl : A->(or A B) | or_intror : B->(or A B)
| Probar el teorema (A,B: Prop) A \/ B -> B \/ A. |
Después de estudiar la Lección de Tipos Inductivos
2.
| Comprobar si es cierto que Replace term1 with term2 equivale a Cut term2=term1. Intro H;Rewrite <- H; Clear H. |
| Probar, utilizando Simpl el Teorema commut:(n,m:nat)(plus m n)=(plus n m) |
| Definiendo:
Inductive le [n:nat] : nat -> Prop := le_n : (le n n) |le_S : (m:nat)(le n m)->(le n (S m)). Definition lt := [n,m:nat](le (S n) m). Definition gt := [n,m:nat](lt m n). probar: (n:nat)(le O n) (n,m:nat)(le n (plus m n)) (n,m:nat)(le n (plus n m)) |
| Probar que (n,m:nat) (lt n m) -> (Ex [p:nat](plus n p)=m) |
Coq < Fixpoint prim_rec [b:nat;p:nat->nat->nat;n:nat]:nat:=
Coq < Cases
n of
Coq <
O => b
Coq < |(S x) => (p x (prim_rec
b p x))
Coq < end.
prim_rec is recursively defined
y la función Prim_rec como:
Coq < Definition Prim_rec:=(nat_rec
[_:nat]nat).
Prim_rec is defined
|
|
Error messages:
1.Intro needs a product
Variants:
1.Intros
It is equivalent to Repeat Intro, except that
it fails when the goal is not a product.
2.Intro ident
Applies Intro but forces ident to be the name
of the introduced hypothesis.
Error message: name ident is already bound
Remark: Intro doesn't check the whole current
context. Actually, identifiers declared or defined in required modules
can be used as ident and, in this case, the old ident of the module is
no more reachable.
3.Intros ident1 ...identn
Is equivalent to the composed tactic Intro
ident1; ...; Intro identn.
More generally, the Intros tactic takes a
pattern as argument in order to introduce names for components of an inductive
definition.
4.Intros until ident
Repeats Intro until it meets a premise of
the goal having form ( ident : term ) and discharges the variable named
ident of the current goal.
Error message: No such hypothesis in current
goal
ASSUMPTION: This tactic applies to any goal. It implements the ``Var'' rule of typing . It looks in the local context for an hypothesis which type is equal to the goal. If it is the case, the subgoal is proved. Otherwise, it fails.
Error messages:
1.No such assumption
EXACT <term>: This tactic applies to any goal. It gives directly the exact proof term of the goal. Let T be our goal, let p be a term of type U then Exact p succeeds iff T and U are convertible.
Error messages:
1.Not an exact proof
APPLY <term>This tactic applies to any goal. The argument term is a term well-formed in the local context. The tactic Apply tries to match the current goal against the conclusion of the type of term. If it succeeds, then the tactic returns as many subgoals as the instantiations of the premises of the type of term.
Error messages:
1.Impossible to unify ...with ...
Since higher order unification is undecidable,
the Apply tactic may fail when you think it should work. In this case,
if you know that the conclusion of term and the current goal are unifiable,
you can help the Apply tactic by transforming your goal with the Change
or Pattern tactics.
2.Cannot refine to conclusions with meta-variables
This occurs when some instantiations of premises
of term are not deducible from the unification. This is the case, for instance,
when you want to apply a transitivity property. In this case, you have
to use one of the variants below:
Variants:
1.Apply term with term1 ...termn
Provides Apply with explicit instantiations
for all dependent premises of the type of term which do not occur in the
conclusion and consequently cannot be found by unification. Notice that
term1 ...termn must be given according to the order of these dependent
premises of the type of term.
Error message: Not the right number of missing arguments
2.Apply term with ref1 := term1 ...refn :=
termn
This also provides Apply with values for instantiating
premises. But variables are referred by names and non dependent products
by order.
3.EApply term
The tactic EApply behaves as Apply but does
not fail when no instantiation are deducible for some variables in the
premises. Rather, it turns these variables into so-called existential variables
which are variables still to instantiate. An existential variable is identified
by a name of the form ?n where n is a number. The instantiation is intended
to be found later in the proof.
4.LApply term
This tactic applies to any goal, say G. The
argument term has to be well-formed in the current context, its type being
reducible to a non-dependent product A -> B with B possibly containing
products. Then it generates two subgoals B->G and A. Applying LApply H
(where H has type A->B and B does not start with a product) does the same
as giving the sequence Cut B. 2:Apply H. where Cut is described below.
Warning: Be careful, when term contains more than one non dependent product the tactic LApply only takes into account the first product.
This tactic applies to any goal. It implements the ``App'' rule. Cut U transforms the current goal T into the two following subgoals: U -> T and U.
Error messages:
1.Not a proposition or a type
Arises when the argument form is neither of
type Prop, Set nor Type.
ELIM This tactic applies
to any goal. The type of the argument term must be an inductive constant.
Then according to the type
of the goal, the tactic Elim chooses the right
destructor and applies it (as in the case of the Apply tactic). For instance,
assume that our proof context contains n:nat,
assume that our current goal is T of type Prop, then Elim n is
equivalent to Apply nat_ind with n:=n.
Error messages:
1.Not an inductive product
2.Cannot refine to conclusions
with meta-variables
As Elim uses Apply,
see section 7.3.4 and the variant Elim ...with ... below.
Variants:
1.Elim term also works when the
type of term starts with products and the head symbol is an inductive definition.
In that case the
tactic tries both to find an object in the inductive definition and to
use this inductive definition for
elimination. In case
of non-dependent products in the type, subgoals are generated corresponding
to the
hypotheses. In the
case of dependent products, the tactic will try to find an instance for
which the elimination
lemma applies.
2.Elim term with term1 ...termn
Allows the user to
give explicitly the values for dependent premises of the elimination schema.
All arguments must
be given.
Error message: Not
the right number of dependent arguments
3.Elim term with ref1 := term1
...refn := termn
Provides also Elim
with values for instantiating premises by associating explicitly variables
(or non dependent
products) with their
intended instance.
4.Elim term1 using term2
Allows the user to
give explicitly an elimination predicate term2 which is not the standard
one for the underlying
inductive type of
term1. Each of the term1 and term2 is either a simple term or a term with
a bindings list (see
7.3.7).
5.ElimType form
The argument form
must be inductively defined. ElimType I is equivalent to Cut I. Intro Hn;
Elim
Hn; Clear Hn Therefore
the hypothesis Hn will not appear in the context(s) of the subgoal(s).
Conversely, if t
is a term of (inductive) type I and which does not occur in the goal then
Elim t is equivalent to
ElimType I; 2: Exact
t.
Error message: Impossible
to unify ...with ...
Arises when form
needs to be applied to parameters.
6.Induction ident
Is equivalent to
Intros until ident; Pattern ident; Elim ident
7.Induction num
Is analogous to Induction
ident but for the num-th non-dependent premise of the goal.
Load nombre carga el fichero nombre.v. El sistema busca el fichero en todos los directorios en el camino de acceso. Se pueden añadir nuevos directorios a este camino con AddPath. En general el camino se inicializa por el contenido del fichero .coqrc.
Inspect n muestra los nombres y los tipos de los n últimos objetos del entorno.
Check t verifica si el objeto t está bien construido y muestra su tipo.
Print nombre muestra la definición y el tipo del objeto "nombre" del entorno.
Reset nombre elimina del entorno el objeto "nombre".