Stream: Coq users

Topic: ✔ Why does this rewrite fail to work?


view this post on Zulip PieQ (Mar 30 2022 at 13:35):

coq_rewrite.png

view this post on Zulip Théo Winterhalter (Mar 30 2022 at 13:36):

H is not an equality, but a disjunction.

view this post on Zulip Enrico Tassi (Mar 30 2022 at 13:37):

destruct H first

view this post on Zulip PieQ (Mar 30 2022 at 14:11):

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

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Mar 30 2022 at 14:12):

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

view this post on Zulip 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.

view this post on Zulip PieQ (Mar 30 2022 at 14:27):

I don't know what I'm doing.

view this post on Zulip Théo Winterhalter (Mar 30 2022 at 14:46):

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

view this post on Zulip PieQ (Mar 30 2022 at 16:06):

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

view this post on Zulip PieQ (Mar 30 2022 at 16:42):

coq_rewrite2.png can I get a hint?

view this post on Zulip 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.

view this post on Zulip PieQ (Mar 30 2022 at 17:40):

holy crap! I think you were right

view this post on Zulip PieQ (Mar 30 2022 at 17:41):

coq_rewrite3.png

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

view this post on Zulip 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.

Should post the code.

view this post on Zulip 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.

view this post on Zulip James Wood (Mar 30 2022 at 20:18):

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

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

view this post on Zulip James Wood (Mar 30 2022 at 20:18):

That gives output:

... code here ...

view this post on Zulip Notification Bot (Mar 31 2022 at 11:41):

PieQ has marked this topic as resolved.


Last updated: Jan 28 2023 at 06:30 UTC