Recordemos que una prueba de "x:A.P(x), consiste en un Programa que a cada entrada a:A le hace corresponder una prueba de P(a). De modo que para construir un par formado por un elemento a de A y una prueba de P(a), nos basta con tener una función (constructor que llamaremos ex_intro) que nos asocie con cada programa p, prueba de "x:A.P(x), un par formado por a:A y p(a):P(A). Al elemento a:A le llamamos "el testigo" (witness) de P.
Se escribe
que es una abreviatura (hay otras) de (ex P [x:A](P x)), y su definición, como tipo inductivo, será:
Coq
< Inductive ex [A:Set;P:A->Prop]:Prop :=
Coq
< ex_intro:(x:A)(P x)->(ex A P).
ex_ind
is defined
ex
is defined
Coq
< Print ex_ind.
ex_ind
=
[A:Set]
[P:A->Prop]
[P0:Prop]
[f:(x:A)(P x)->P0]
[e:(ex A P)]Cases e of (ex_intro x x0) => (f x x0) end
: (A:Set)(P:A->Prop)(P0:Prop)((x:A)(P x)-> P0) ->(ex A P)->P0
Fijémonos en el tipo de ex_ind. Nos dice que para probar un objetivo de la forma $x:A.P(x) => P0, lo que hemos de hacer es construir una función que a cada prueba h:$x:A.P(x) le asocie una prueba de P0. Para ello basta tomar un elemento "genérico" de A, y, sin utilizar ninguna propiedad específica de este elemento, y usando P(a), demostrar P0. Este proceso es el que implementa Elim h.
Por ejemplo:
Coq
< Section Predicate_calculus.
Coq
< Variable D:Set.
D
is assumed
Coq
< Variable R:D->D->Prop.
R
is assumed
Supongamos que R es una relación
simétrica y transitiva.
Coq
< Section R_sym_trans.
Coq
< Hypothesis R_symmetric:(x,y:D) (R x y) -> (R y x).
R_symmetric
is assumed
Coq
< Hypothesis R_transitive : (x,y,z:D)(R x y) -> (R y z) -> (R x z).
R_transitive
is assumed
Coq
< Lemma refl_if : (x:D)(EX y:D|(R x y))->(R x x).
1
subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
============================
(x:D)(EX y | (R x y))->(R x x)
refl_if
< Intros x x_Rlinked.
1
subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
x : D
x_Rlinked : (EX y | (R x y))
============================
(R x x)
refl_if
< Elim x_Rlinked.
1
subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
x : D
x_Rlinked : (EX y | (R x y))
============================
(x0:D)(R x x0)->(R x x)
refl_if
< Intros y Rxy.
1
subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
x : D
x_Rlinked : (ex D [y:D](R x y))
y : D
Rxy : (R x y)
============================
(R x x)
refl_if
< Apply R_transitive with y.
2
subgoals
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
x : D
x_Rlinked : (ex D [y:D](R x y))
y : D
Rxy : (R x y)
============================
(R x y)
subgoal
2 is:
(R
y x)
refl_if
< Assumption.
1
subgoal
D : Set
R : D->D->Prop
R_symmetric : (x,y:D)(R x y)->(R y x)
R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
x : D
x_Rlinked : (ex D [y:D](R x y))
y : D
Rxy : (R x y)
============================
(R y x)
refl_if
< Apply R_symmetric; Assumption.
Subtree
proved!
refl_if is defined
Coq
< End R_sym_trans.
Constant
refl_if
: ((x,y:D)(R x y)->(R y x))
->((x,y,z:D)(R x y)->(R y z)->(R x z))
->(x:D)(ex D [y:D](R x y))->(R x x)
.....
La aplicación del
constructor de tipo, da origen en este caso a la táctica Exists
============================
(A:Set)(P:A->Prop)A->(Ex P)
absurdo
< Intros.
1
subgoal
A : Set
P : A->Prop
x : A
============================
(Ex P)
absurdo
< Exists x.
1
subgoal
A : Set
P : A->Prop
x : A
============================
(P x)
Coq
< Inductive eq [A:Set; x:A] : A->Prop := refl_equal : (eq A x
x).
eq_ind
is defined
eq_rec
is defined
eq
is defined
Coq
< Check eq_ind.
eq_ind
: (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)(eq A x y)->(P y)
La expresión (eq A x x)se simplifica a x=x.Y en general, (eq A x y) se escribe x=y. De nuevo, disponemos de la eliminación y de tácticas que aplican el constructor. Entre estas últimas están las tácticas Rewrite y Replace
Por ejemplo:
Coq
< Variable f:nat->nat.
f
is assumed
Coq
< Hypothesis foo:(f O)=O.
foo
is assumed
Coq
< Lemma L1: (k:nat)k=O -> (f k)=k.
1
subgoal
============================
(k:nat)k=O->(f k)=k
L1
< Intros k E.
1
subgoal
k : nat
E : k=O
============================
(f k)=k
L1
< Rewrite E.
1
subgoal
k : nat
E : k=O
============================
(f O)=O
L1
< Apply foo.
Subtree
proved!
L1
< Save.
Intros
k E.
Rewrite
E.
Apply
foo.
L1 is defined
Coq
< Lemma L2: (f (f O))=O.
1
subgoal
============================
(f (f O))=O
L2
< Replace (f O) with O.
2
subgoals
============================
(f O)=O
subgoal
2 is:
O=(f
O)
L2
< Apply foo.
1
subgoal
============================
O=(f O)
L2
< Symmetry.
1
subgoal
============================
(f O)=O
L2
< Apply foo.
Subtree
proved!
Para ilustrar la eliminación,
propongamos un caso genérico:
Coq
< variable A:Set. Variable P:A->Prop.
A
is assumed
P
is assumed
Coq
< Variable x:A.
x
is assumed
Coq
< Lemma kk:(y:A)x=y -> (P y).
1
subgoal
============================
(y:A)x=y->(P y)
kk
< Intros.
1
subgoal
y : A
H : x=y
============================
(P y)
kk
< Elim H.
1
subgoal
y : A
H : x=y
============================
(P x)
En el ámbito Type, al
igual que en el Set, se puede hacer Cálculo de Predicados. por ejemplo,
el constructor del cuantificador universal (EXT x | (P x)) es:
Coq
< Check exT_intro.
exT_intro
: (A:Type)(P:A->Prop)(x:A)(P x)->(ExT P)
Analogamente, la igualdad sobre Type está disponible y se escribe ==.
Las tácticas siguen siendo las mismas que antes.
Por ejemplo:
Coq
< Theorem Witnesses: (a,b: Type) (p: Type -> Prop) (p a) \/ (p b) ->
(ExT [x: Type] (p x)).
1
subgoal
============================
(a,b:Type)(p:Type->Prop)(p a)\/(p b)->(EXT x:Type | (p x))
Coq
< Intros.
a : Type
b
: Type
p : Type->Prop
H : (p a)\/(p b)
============================
(EXT x:Type | (p x))
Coq
< Elim H.
2
subgoals
a : Type
b
: Type
p : Type->Prop
H : (p a)\/(p b)
============================
(p a) -> (EXT x:Type | (p x))
Coq
< Intro.
2
subgoals
a : Type
b
: Type
p : Type->Prop
H : (p a)\/(p b)
H0: (p a)
============================
(EXT x:Type | (p x))
subgoal
2 is:
(p
b)->(EXT x:Type | (p x))
Witnesses
< 2: Intro.
2
subgoals
a : Type
b : Type
p : Type->Prop
H : (p a)\/(p b)
H0 : (p a)
============================
(EXT x:Type | (p x))
subgoal
2 is:
(EXT
x:Type | (p x))
Witnesses
< Exists a.
2
subgoals
a : Type
b : Type
p : Type->Prop
H : (p a)\/(p b)
H0 : (p a)
============================
(p a)
subgoal
2 is:
(EXT
x:Type | (p x))
Witnesses
< Assumption.
1
subgoal
a : Type
b : Type
p : Type->Prop
H : (p a)\/(p b)
H0 : (p b)
============================
(EXT x:Type | (p x))
Witnesses
< Exists b; Assumption.
Subtree
proved!
Un tratamiento análogo al caso de Set. Por ejemplo:
Theorem
Simple: (A: Set)(R: A -> A -> Prop)
((x,y,z: A) (R x y) /\ (R y z) -> (R x z)) ->
((x,y: A) (R x y) -> (R y x)) ->
(x: A) ((Ex [y: A] (R x y))) -> (R x x).
1
subgoal
============================
(A:Set)
(R:A->A->Prop)
((x,y,z:A)(R x y)/\(R y z)->(R x z))
->((x,y:A)(R x y)->(R y x))->
(x:A)(EX y | (R x y))->(R x x)
Simple
< Intros A R H' H'0 x h.
1
subgoal
A0 : Set
R : A0->A0->Prop
H' : (x,y,z:A0)(R x y)/\(R y z)->(R x z)
H'0 : (x,y:A0)(R x y)->(R y x)
x : A0
h : (EX y:A0 | (R x y))
============================
(R x x)
Simple
< Elim h.
1
subgoal
A0 : Set
R : A0->A0->Prop
H' : (x,y,z:A0)(R x y)/\(R y z)->(R x z)
H'0 : (x,y:A0)(R x y)->(R y x)
x : A0
h : (EX y:A0 | (R x y))
============================
(x0:A0)(R x x0)->(R x x)
Simple
< Intros y E.
1
subgoal
A0 : Set
R : A0->A0->Prop
H' : (x,y,z:A0)(R x y)/\(R y z)->(R x z)
H'0 : (x,y:A0)(R x y)->(R y x)
x : A0
h : (EX y:A0 | (R x y))
y : A0
E : (R x y)
============================
(R x x)
Simple
< Apply H' with y.
1
subgoal
A0 : Set
R : A0->A0->Prop
H' : (x,y,z:A0)(R x y)/\(R y z)->(R x z)
H'0 : (x,y:A0)(R x y)->(R y x)
x : A0
h : (EX y:A0 | (R x y))
y : A0
E : (R x y)
============================
(R x y)/\(R y x)
Simple
< Split;[Assumption|Idtac].
1
subgoal
A0 : Set
R : A0->A0->Prop
H' : (x,y,z:A0)(R x y)/\(R y z)->(R x z)
H'0 : (x,y:A0)(R x y)->(R y x)
x : A0
h : (EX y:A0 | (R x y))
y : A0
E : (R x y)
============================
(R y x)
Simple
< Apply H'0;Assumption.
Subtree
proved!
Coq
< Inductive bool:Set := true:bool | false:bool.
bool_ind
is defined
bool_rec
is defined
bool_rect
is defined
bool
is defined
Coq
< Check bool_ind.
bool_ind
: (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
Coq
< Lemma duality:(b:bool)(b=true)\/(b=false).
1
subgoal
============================
(b:bool)b=true\/b=false
duality
< Intro h.
1
subgoal
h : bool
============================
h=true\/h=false
duality
< Elim h.
2
subgoals
h : bool
============================
true=true\/true=false
subgoal
2 is:
false=true\/false=false
duality
< 2: Right.
2
subgoals
h : bool
============================
true=true\/true=false
subgoal
2 is:
false=false
duality
< Left.
2
subgoals
h : bool
============================
true=true
subgoal
2 is:
false=false
duality
< Apply refl_equal.
1
subgoal
h : bool
============================
false=false
duality
< Trivial.
Subtree
proved!
El tipo vacio:
Coq
< Inductive Falso:Prop :=.
Falso_ind
is defined
Falso
is defined
Coq
< Print False.
Inductive
False : Prop :=
Coq
< Check False_ind.
False_ind
: (P:Prop)False->P
Coq
< Inductive Verdad: Prop := U:Verdad.
Verdad_ind
is defined
Verdad_rec
is defined
Verdad
is defined
Coq
< Check Verdad_ind.
Verdad_ind
: (P:Prop)P->Verdad->P
Coq
< Check U.
U
: Verdad
Coq
< Print True.
Inductive
True : Prop := I : True
Coq
< Check True_ind.
True_ind
: (P:Prop)P->True->P
Coq
< Theorem deFalso : Falso -> O = (S O).
1
subgoal
============================
Falso->(0)=(1)
deFalso
< Intro.
1
subgoal
H : Falso
============================
(0)=(1)
deFalso
< Elim H.
Subtree
proved!
O también:
Coq
< Theorem deFalse: False -> (1)=(2).
1
subgoal
============================
False->(1)=(2)
deFalse
< Contradiction.
Subtree
proved!
deFalso
< Undo.
La táctica Absurd P también prueba cualquier objetivo por eliminación de la proposición False, si P y ~P pueden derivarse del contexto. En Coq la proposición ~P es simplemente una abreviatura de (P -> False). Por lo tanto, si se tienen f:~P y a:P, entonces (f a):False.
Coq
< Theorem sinsentido: (Q:Prop) ~(O=O) -> Q.
1
subgoal
============================
(Q:Prop)~(0)=(0)->Q
sinsentido
< Intro Q.
1
subgoal
Q : Prop
============================
~(0)=(0)->Q
sinsentido
< Intro H.
1
subgoal
Q : Prop
H : ~(0)=(0)
============================
Q
sinsentido
< Absurd (0)=(0).
2
subgoals
Q : Prop
H : ~(0)=(0)
============================
~(0)=(0)
subgoal
2 is:
(0)=(0)
sinsentido
< Assumption.
1
subgoal
Q : Prop
H : ~(0)=(0)
============================
(0)=(0)
sinsentido
< Trivial.
Subtree
proved!
Coq
< Save.
sinsentido
is defined
Coq
< Check False_ind.
False_ind
: (P:Prop)False->P
Coq
< Print sinsentido.
sinsentido
=
[Q:Prop][H:~(0)=(0)](False_ind
Q
(H (refl_equal nat(0)))):
(Q:Prop)~(0)=(0)->Q
This tactic applies to any goal. The type of term must have the form
(x1:A1) ...(xn:An)term1=term2.
Then Rewrite term replaces every occurrence of term1 by term2 in the
goal. Some of the variables x1 are solved by
unification, and some of the types A1, ..., An become new subgoals.
Remark: In case the type of term1 contains occurrences of variables
bound in the type of term, the tactic tries first to
find a subterm of the goal which matches this term in order to find
a closed instance term'1 of term1, and then all
instances of term'1 will be replaced.
Error messages:
1.No equality here
2.Failed to progress
This happens if term1 does not occur in the
goal.
Variants:
1.Rewrite -> term
Is equivalent to Rewrite term
2.Rewrite <- term
Uses the equality term1=term2 from right to
left
3.Rewrite term in ident
Analogous to Rewrite term but rewriting is
done in the hypothesis named ident.
4.Rewrite -> term in ident
Behaves as Rewrite term in ident.
5.Rewrite <- term in ident
Uses the equality term1=term2 from right to
left to rewrite in the hypothesis named ident.
This tactic applies to any goal. It replaces all free occurrences of
term1 in the current goal with term2 and generates the
equality term2=term1 as a subgoal. It is equivalent to Cut term1=term2.
Intro Hn; Rewrite <- Hn; Clear
Hn.
Variants:
1.Replace term1 with term2 in ident This replaces term1
with term2 in the hypothesis named ident, and
generates the subgoal term2=term1.
Error messages:
1.No such hypothesis
7.6 INTRODUCTIONS
Introduction tactics address goals which are inductive constants. They
are used when one guesses that the goal can be
obtained with one of its constructors' type.
Constructor num
This tactic applies to a goal such that the head of its conclusion is
an inductive constant (say I). The argument num must
be less or equal to the numbers of constructor(s) of I. Let ci be the
i-th constructor of I, then Constructor i is
equivalent to Intros; Apply ci.
Error messages:
1.Not an inductive product
2.Not enough Constructors
Variants:
1.Constructor This tries Constructor 1 then Constructor
2, ..., then Constructor n where n if
the number of constructors of the head of
the goal.
2.Constructor num with bindings_list
Let ci be the i-th constructor of I, then
Constructor i with bindings_list is equivalent to Intros;
Apply ci with bindings_list.
Warning: the terms in the bindings_list are
checked in the context where Constructor is executed and not in
the context where Apply is executed (the introductions
are not taken into account).
3.Split
Applies if I has only one constructor, typically
in the case of conjunction A/\ B. It is equivalent to Constructor
1.
4.Exists bindings_list
Applies if I has only one constructor, for
instance in the case of existential quantification. It is equivalent
to Intros; Constructor 1 with bindings_list.
5.Left, Right
Apply if I has two constructors, for instance
in the case of disjunction A\/ B. They are respectively equivalent to
Constructor 1 and Constructor 2.
6.Left bindings_list, Right bindings_list, Split bindings_list
Are equivalent to the corresponding Constructor
i with bindings_list.
AUTO
This tactic implements a Prolog-like resolution procedure to solve the
current goal. It first tries to solve the goal using the
Assumption tactic, then it reduces the goal to an atomic one using
Intros and introducing the newly generated
hypotheses as hints. Then it looks at the list of tactics associated
to the head symbol of the goal and tries to apply one of
them (starting from the tactics with lower cost). This process is recursively
applied to the generated subgoals. The
maximal search depth is 5 by default.
Variants:
1.Auto num
Forces the search depth to be num.
2.Trivial This tactic is a restriction
of Auto for doing hypotheses and hints of cost 0. Typically it solves goals
such as trivial equalities X=X.
IDTAC
The constant Idtac is the identity tactic: it
leaves any goal unchanged .
CONTRADICTION
This tactic applies to any goal. The Contradiction tactic attempts
to find in the current context (after all Intros)
one which is equivalent to False. It permits to prune irrelevant cases.
This tactic is a macro for the tactics sequence
Intros; ElimType False; Assumption.
Error messages:
1.No such assumption
ABSURD TERM
This tactic applies to any goal. The argument term is any proposition
P of type Prop. This tactic applies False
elimination, that is it deduces the current goal from False, and generates
as subgoals ~P and P. It is very useful in
proofs by cases, where some cases are impossible. In most cases, P
or ~P is one of the hypotheses of the local context.