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:

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

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:

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

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?

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')`

?

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')
```