Stream: math-comp users

Topic: ✔ `apply` works but `apply : ` fails


view this post on Zulip walker (Nov 03 2022 at 15:54):

I thought both are basically the same thing:

Until this:

I have propositionally defined version of in called PIn

and I had a lemma:

Lemma Pin_in_neg (A: eqType): forall (a: A) (l: seq A),  ~ PIn a l <-> a \notin l.
Proof.
Admitted.

Then

Goal forall (A: eqType) (a: A) (l: seq A) , ~ PIn a l -> a \notin l.
move => A a l.
apply: Pin_in_neg.

failed saying that Cannot apply lemma Pin_in_neg
I am not sure why ssreflect apply fails when normal apply works ?

view this post on Zulip Alexander Gryzlov (Nov 03 2022 at 16:08):

I think apply: treats bijections by trying to fit the expression on both sides, not the whole bijection, i.e. the following works: move => A a l H; apply/Pin_in_neg.. This can of course be further simplified to move => A a l /Pin_in_neg..

view this post on Zulip Enrico Tassi (Nov 03 2022 at 16:08):

It uses lemmas in one direction only. Unless you use the lemma as a view, in that case it tries both. Try apply/Pin_in_neg.

view this post on Zulip walker (Nov 03 2022 at 16:16):

I will use the opportunity to ask what does mean to use lemma as a view, and excatly does apply/Pin_in_neg do ?

view this post on Zulip Paolo Giarrusso (Nov 03 2022 at 22:49):

The two tactics have gazillions of corner cases where they differ, but here apply: simply skips the destruct step of apply :-).

view this post on Zulip Paolo Giarrusso (Nov 03 2022 at 22:50):

And I say "destruct" because it's not limited to bi-implications :smiling_devil:

view this post on Zulip Notification Bot (Nov 04 2022 at 10:18):

walker has marked this topic as resolved.


Last updated: Jul 25 2024 at 15:02 UTC