## Stream: math-comp users

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

#### 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.
``````

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 ?

#### 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.`.

#### 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.`

#### 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 ?

#### 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 :-).

#### Paolo Giarrusso (Nov 03 2022 at 22:50):

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

#### Notification Bot (Nov 04 2022 at 10:18):

walker has marked this topic as resolved.

Last updated: Jul 25 2024 at 15:02 UTC