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?

What does `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 `apply`

?

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:

Janno said:

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