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 ?

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

.

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

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

do ?

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

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

walker has marked this topic as resolved.

Last updated: Jul 25 2024 at 15:02 UTC