Open herbelin opened 3 years ago
With destruct
/induction
it seems there is a guarantee that there is no remaining dependency on the variable? For instance if you try
Lemma foo X (x:X) (e:x=x) (H:e = eq_refl) : False.
destruct e.
it will fail rather than doing some sort of dummy match, and in succesful cases the variable would get replaced by the appropriate constructor application. Maybe I missed an edge case though?
With apply
/rewrite
clearly there is no guarantee, IMO if we have to analyse whether there is a dependency to be able to decide if we're clearing we just shouldn't clear.
I guess the alternative is to force clear by default, failing if there is a dependency, with a syntax to skip clearing, but that feels somewhat strange to me.
I see three typical cases:
Reversible steps, i.e. cases where the information used can be reconstructed from the new goal
This is typically the case of destruct x
when x
is of an inductive type whose indices are fresh distinct variables.
This is typically also the case of subst x
or rewrite H
when H
has a type of the form x = t
and x
does not occur in t
, or when H
has a type of the form C(x1,...,xn)
and each position of C
is invertible so that C(x1,...,xn) = t
is equivalent to the conjunctions of equations of the form xi = proji t
and the xi
do not occur in ti
(a typical example is (x,y) = t
). In this case the reverse steps are remember
or set
depending on whether x
is part of an equality or a local definition.
Irreversible steps with dependencies
This is typically the case of destruct (x args) eqn:H
which explicitly asks for remembering something about x
.
Other irreversible steps
This is the case of apply x
or destruct x
, when x
has still arguments (or at least arguments in non-proof-irrelevant types), or rewrite H
with H
of type t=u
and t
is not inversible over its variables.
@SkySkimmer, your example fails but the failure is not a guarantee that a non failure of destruct x
with x
of inductive type is w/o loss of information. Consider e.g. Lemma foo (x:nat) (e:x = S x) : x = x. destruct e.
which works but loses the information that there is a contradiction.
It seems that my question is about the "other irreversible steps". Assuming that we give a modifier to force a clear
or to prevent a clear
when the default is not what is expected, what is the most useful default, to clear or not to clear? That is, is it more common to use resources linearly or not?
[Added] More precisely, it seems to me that either those apply
and rewrite
of the third category should clear by default, or those destruct
of the third category should not clear (disregarding questions of compatibility).
I don't care about reversibility tbh, it seems like the wrong thing to look at.
Description of the problem
The rules for clearing or not by default the argument of a tactic when it is a variable are undocumented and a bit unclear.
For
destruct
/induction
, the variable is cleared by default when there is nowith
oreqn
clause orin
clause and it is thee
-variant of them. The restriction toeqn
orin
is obvious because a dependency remains but the restriction toedestruct/einduction
andwith
is however unclear (see in particular #13521). Note that there is a syntax to cancel the clearing when it is the default: it is to surround the variable with parentheses, e.g.destruct (n)
.For
apply
/rewrite
, the variable is not cleared by default (when it is a variable). The practice would suggest that it is however more common to use an hypothesis once than more than once. So a clearing by default could be a convenient default. Note that there is an undocumented syntax to force clearing, namelyapply >H
orrewrite >H
.