Unable to use the induction hypothesis in In_map_iff

Using Coq
1

Hi!

I’m solving this problem from ‘Logic’ and I don’t know how to proceed further. I am unable to use IHl’. Here is my attempt:

image

image

If there is a more efficient way to approach this problem, please let me know. Thanks!

2

When you have a hypothesis IHl' that’s an implication and another hypothesis HB that matches the premises of IHl', you can apply IHl' to HB by apply IHl' in HB, or specialize (IHl' HB) (which is more robust if IHl' has more than one premises).

Note also that by using exists x in both branches after intros [HA|HB], you’re basically claiming that In y (map f (x :: l')) -> f x = y /\ In x (x :: l'). Can you see how that’s quite different from the original goal?

3

Thanks so much for replying!

I could understand the apply IHl' in HB part, but could not understand the point you made in the second paragraph. How is it In y (map f(x :: l')) and not In y (map f l')?

4

You have the goal

In y (map f l) -> exists x, f x = y /\ In x l

The tactic induction l as [|x l' IHl'] destructs l and, in the second subgoal, replaces l with (x :: l'). To avoid the name collision with exists x, that gets renamed to exists x0.

In y (map f (x :: l')) -> exists x0, f x0 = y /\ In x0 (x :: l')

Then the tactic intros [HA|HB] destructs the hypothesis In y (map f (x :: l')), and in both cases you instantiate the existential quantifier with exists x. The result of that instantiation is the same as if, from the previous goal, you removed the exists x0 quantifier and replace other occurrences of x0 with x:

In y (map f (x :: l')) -> f x = y /\ In x (x :: l')