## Stream: Coq users

### Topic: ✔ Why does this rewrite fail to work?

coq_rewrite.png

#### Théo Winterhalter (Mar 30 2022 at 13:36):

`H` is not an equality, but a disjunction.

destruct H first

#### PieQ (Mar 30 2022 at 14:11):

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

#### Théo Winterhalter (Mar 30 2022 at 14:12):

You have either `f a = y` or `In y (map f l)` from the math point of view.

#### Théo Winterhalter (Mar 30 2022 at 14:12):

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

#### Enrico Tassi (Mar 30 2022 at 14:18):

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.

#### PieQ (Mar 30 2022 at 14:27):

I don't know what I'm doing.

#### Théo Winterhalter (Mar 30 2022 at 14:46):

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

#### PieQ (Mar 30 2022 at 16:06):

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

#### PieQ (Mar 30 2022 at 16:42):

coq_rewrite2.png can I get a hint?

#### James Wood (Mar 30 2022 at 17:31):

I think the last `exists l1.` is wrong. The witness in that case should be the same as the witness of the recursive call.

#### PieQ (Mar 30 2022 at 17:40):

holy crap! I think you were right

#### PieQ (Mar 30 2022 at 17:41):

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

#### PieQ (Mar 30 2022 at 17:58):

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.

#### James Wood (Mar 30 2022 at 20:17):

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

#### James Wood (Mar 30 2022 at 20:18):

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

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

#### James Wood (Mar 30 2022 at 20:18):

That gives output:

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

#### Notification Bot (Mar 31 2022 at 11:41):

PieQ has marked this topic as resolved.

Last updated: Sep 26 2023 at 12:02 UTC