CONG_TAC
bossLib.CONG_TAC : int option -> tactic
Applies congruence rules backwards repeatedly to attack an equality
Applying CONG_TAC dopt to a goal ?- x = y attempts to apply
congruence rules backwards repeatedly, generating a number of further
equality subgoals. The dopt parameter limits the number of times this
will be done: when dopt is NONE, there is no limit: the base
transformation will be tried on the initial and all subsequent goals. If
dopt is SOME i, then i is the total number of transformations that
will be made. (If dopt is SOME 0 then CONG_TAC dopt is equivalent
to ALL_TAC.)
If at least one of the equality's arguments is an abstraction (possibly paired), then the transformation rewrites with function extensionality, strips the universally quantified variables, and beta-reduces where necessary.
If at least one of the equality's arguments is a set comprehension, then the transformation rewrites with set-extensionality and applies the conversion that calculates what it is for a term to be a member of a comprehension to one or both sides of the equality. Unless both sides are set comprehensions, this is likely to be the last transformation possible.
If the goal matches the conclusion of any of the theorems stored as
congruences for the definition package (with attribute name defncong
or cong), then this theorem is applied backwards to generate new
sub-goals. If the new sub-goals include preconditions and universally
quantified variables, these are stripped into the assumptions.
Finally, the "base transformation" depends on the shape of the
equality's arguments. If both sides are combinations (M e1 and N e2,
say), then the base transformation will be similar to an application of
MK_COMB_TAC, generating at least the goals ?- M = N and
?- e1 = e2. When the head terms of both applications are equal, then
one step of the base transformation is taken to be the iteration of
MK_COMB_TAC that strips all arguments, so that
?- f e1 .. en = f e1' .. en' will turn into n subgoals, each of the
form ?- ei = ei'. (The ?- f = f subgoal will be eliminated
immediately, as below.)
In all cases, new subgoals that are instances of reflexivity, or which occur in the goal's assumptions (with either orientation) are immediately eliminated.
Failure
Fails if the provided depth is either NONE or SOME i with i
greater than zero, and the goal is not an equality at all, or cannot be
changed by any of the transformations described above. For example, with
f : 'a -> num and g : num -> num, the goal ?- f a = g n cannot be
reduced.
Example
The following involves a handling of abstractions:
> CONG_TAC NONE ([], “(∀x. f (z:'a) < x) ⇔ (∀y. c < y)”);
val it = ([([], “f z = c”)], fn): goal list * validation
Slightly altering the goal, and keeping the depth as NONE turns
something true into something unprovable:
> CONG_TAC NONE ([], “(∀x. f (z:'a) < x) ⇔ (∀y. y < 6)”);
val it = ([([], “f z = x”), ([], “x = 6”)], fn): goal list * validation
where the x in each sub-goal is completely fresh.
Finally, user-congruences can give richer contexts when proving functions equal:
> CONG_TAC NONE
([], “MAP (λa. f a + 1) (l1:'a list) = MAP g (l2:'a list)”);
val it = ([([“MEM x l2”], “f x + 1 = g x”), ([], “l1 = l2”)], fn):
goal list * validation
Comments
This is a powerful tool for taking apart two terms that share a skeleton and need only have their leaves shown to be equal. Equally, it is quite possible for this tactic to turn a solvable goal into an unsolvable one.
An application of CONG_TAC will never break apart the function
applications that lie within the representation of natural number
numerals.
The name cong_tac can be used as an alias for CONG_TAC.