Can someone explain to me why
apply succeeds in the following case?
Inductive R : nat -> nat -> Prop := . Lemma foo (H : Acc R 1) : Acc R 0. Proof. apply H.
Is this some special case for the accessibility predicate?
Show Proof. say?
(fun H : Acc R 1 => let H0 : forall y : nat, R y 1 -> Acc R y := match H with | @Acc_intro _ _ _ x => x end in H0 0 ?Goal)
As far as I can tell it is implicitly using the fact that something is accessible if it is related to something larger that is accessible.
This seems to me more like the logic in
apply that destructs records/inductives to find a fact that is applicable to the current goal.
Hmm, that makes sense, if I first destruct H then I get something that makes more sense to apply and seems to agree with the subgoals generated. Interesting, I was not aware of this behavior.
Is this the
If the conclusion of the type of term does not match the goal and the conclusion is an inductive type isomorphic to a tuple type, then each component of the tuple is recursively matched to the goal in the left-to-right order.
part of the documentation about
Yes, I think it is
Aha. It was so unexpected that even after reading the manual, I could not see how that applied. Well, thanks for the explanation!
I only learned about it very recently from @Paolo Giarrusso. I find this behaviour extremely surprising.
My approach seems more or less to get burned, etch the surprising behavior into memory, and repeat it at the slightest provocation for the next >=3 years.
except I wasn't quite _burned_ by this particular one :smile:
I only learned about it very recently from Paolo Giarrusso. I find this behaviour extremely surprising.
I think this exists to allow you to
apply an equivalence (which is just and and of two implications)
I'm familiar with that behavior, which is also supported by rewrite and by ssreflect views, but neither destructs arbitrary inductives...
Last updated: Jan 29 2023 at 03:28 UTC