Stream: Coq users

Topic: Strange unification with Acc

Jakob Botsch Nielsen (Aug 31 2020 at 14:21):

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?

Ali Caglayan (Aug 31 2020 at 14:30):

What does Show Proof. say?

Jakob Botsch Nielsen (Aug 31 2020 at 14:31):

(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.

Janno (Aug 31 2020 at 14:32):

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.

Jakob Botsch Nielsen (Aug 31 2020 at 14:33):

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.

Jakob Botsch Nielsen (Aug 31 2020 at 14:45):

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?

Janno (Aug 31 2020 at 14:46):

Yes, I think it is

Jakob Botsch Nielsen (Aug 31 2020 at 14:47):

Aha. It was so unexpected that even after reading the manual, I could not see how that applied. Well, thanks for the explanation!

Janno (Aug 31 2020 at 14:52):

I only learned about it very recently from @Paolo Giarrusso. I find this behaviour extremely surprising.

Paolo Giarrusso (Aug 31 2020 at 15:10):

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.

Paolo Giarrusso (Aug 31 2020 at 15:12):

except I wasn't quite _burned_ by this particular one :smile:

Clément Pit-Claudel (Sep 02 2020 at 14:14):

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)

Paolo Giarrusso (Sep 02 2020 at 14:27):

I'm familiar with that behavior, which is also supported by rewrite and by ssreflect views, but neither destructs arbitrary inductives...

Last updated: Sep 23 2023 at 08:01 UTC