`H`

is not an equality, but a disjunction.

destruct H first

Alright, thanks. why exactly does this not work, from the math point of view?

You have either `f a = y`

or `In y (map f l)`

from the math point of view.

You don't know which, so you have to look at both cases.

Also, you have an induction hypothesis and you did not use it... at least in one of the two branches of your proof you will have to.

I don't know what I'm doing.

Perhaps you should stop and try to perform your proof on paper first.

Yeah I'm lost with this one. Might have to look up the answer

coq_rewrite2.png can I get a hint?

I think the last `exists l1.`

is wrong. The witness in that case should be the same as the witness of the recursive call.

holy crap! I think you were right

final proof. Done. Can you explain more in detail what you mean? What happened when I used l1 instead of x?

Theorem In_map_iff :

forall (A B : Type) (f : A -> B) (l : list A) (y : B),

In y (map f l) <->

exists x, f x = y /\ In x l.

Proof.

intros A B f l y. split.

```
+ intros A1'. induction l as [|l1]. simpl in A1'. destruct A1'.
simpl in A1'. destruct A1'. exists l1. Focus 2. simpl. destruct IHl.
```

apply H. exists x. split. destruct H0. apply H0. destruct H0.

right. apply H1. split. apply H. simpl. tauto.

- intros. destruct H. destruct H. rewrite <- H. apply In_map.

apply H0.

Qed.

Should post the code.

`l1`

is the head of the list you're doing induction over. You had that `y`

was in `map f (l1 :: l2)`

, did a case analysis on that proof, and were in the case where `y`

was in `map f l2`

(note that `map f (l1 :: l2)`

normalises to `f l1 :: map f l2`

, which is where the term `map f l2`

comes from). From that point, `l1`

is essentially irrelevant; you're looking in `l2`

. The fact that you're looking at `l2`

is a good sign to deploy the induction hypothesis as soon as possible.

By the way, you can preformat your code on Zulip using:

```
```
... code here ...
```
```

That gives output:

```
... code here ...
```

PieQ has marked this topic as resolved.

Last updated: Sep 26 2023 at 12:02 UTC