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