1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
\DOC UNIFY_ACCEPT_TAC
\TYPE {UNIFY_ACCEPT_TAC : term list -> thm -> 'a * term -> ('b list * instantiation) * 'c list * (instantiation -> 'd list -> thm)}
\SYNOPSIS
Unify free variables in theorem and metavariables in goal to accept theorem.
\DESCRIBE
Given a list {l} of assignable metavariables, a theorem {th} of the form {A |-
t} and a goal {A' ?- t'}, the tactic {UNIFY_ACCEPT_TAC} attempts to unify {t}
and {t'} by instantiating free variables in {t} and metavariables in the list
{l} in the goal {t'} so that they match, then accepts the theorem as the
solution of the goal.
\FAILURE
Fails if no unification will work. In fact, type instantiation is not at
present included in the unification.
\EXAMPLE
An inherently uninteresting but instructive example is the goal:
{
# g `(?x:num. p(x) /\ q(x) /\ r(x)) ==> ?y. p(y) /\ (q(y) <=> r(y))`;;
}
\noindent which could of course be solved directly by {MESON_TAC[]} or
{ITAUT_TAC}. In fact, the process we will outline is close to what {ITAUT_TAC}
does automatically. Let's start with:
{
# e STRIP_TAC;;
val it : goalstack = 1 subgoal (1 total)
0 [`p x`]
1 [`q x`]
2 [`r x`]
`?y. p y /\ (q y <=> r y)`
}
\noindent and defer the actual choice of existential witness by introducing a
metavariable:
{
# e (X_META_EXISTS_TAC `n:num` THEN CONJ_TAC);;
val it : goalstack = 2 subgoals (2 total)
0 [`p x`]
1 [`q x`]
2 [`r x`]
`q n <=> r n`
0 [`p x`]
1 [`q x`]
2 [`r x`]
`p n`
}
\noindent Now we finally fix the metavariable to match our assumption:
{
# e(FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n:num`]));;
val it : goalstack = 1 subgoal (1 total)
0 [`p x`]
1 [`q x`]
2 [`r x`]
`q x <=> r x`
}
\noindent Note that the metavariable has also been correspondingly instantiated
in the remaining goal, which we can solve easily:
{
# e(ASM_REWRITE_TAC[]);;
val it : goalstack = No subgoals
}
\USES
Terminating proof search when using metavariables. Used in {ITAUT_TAC}
\SEEALSO
ACCEPT_TAC, ITAUT, ITAUT_TAC, MATCH_ACCEPT_TAC.
\ENDDOC
|
