Stream: Coq users

Topic: ✔ Why does this rewrite fail to work?

PieQ (Mar 30 2022 at 13:35):

coq_rewrite.png

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

H is not an equality, but a disjunction.

Enrico Tassi (Mar 30 2022 at 13:37):

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

coq_rewrite3.png

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: Oct 13 2024 at 01:02 UTC