Stream: Coq users

Topic: Strange unification with Acc


view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Aug 31 2020 at 14:30):

What does Show Proof. say?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Janno (Aug 31 2020 at 14:46):

Yes, I think it is

view this post on Zulip 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!

view this post on Zulip Janno (Aug 31 2020 at 14:52):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 31 2020 at 15:12):

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

view this post on Zulip 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)

view this post on Zulip 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: Jan 29 2023 at 03:28 UTC