Hello

I am currently stuck at `https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html`

, exercise `Theorem combine_split`

.

My proof state is following:

```
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
intros X Y.
induction l.
- intros. injection H as H1 H2. rewrite <- H1. rewrite <- H2. reflexivity.
- intros.
```

=====

```
1 goal
X : Type
Y : Type
x : X * Y
l : list (X * Y)
IHl : forall (l1 : list X) (l2 : list Y), split l = (l1, l2) -> combine l1 l2 = l
l1 : list X
l2 : list Y
H : split (x :: l) = (l1, l2)
______________________________________(1/1)
combine l1 l2 = x :: l
```

The book was explaining how we can use `destruct `

and `unfold`

tactics just before that exercise, however, neither of these seem to help much. Any help ?..

Have you tried simplifying

`simpl.`

on this goal won't make a difference, will it?

Paolo Giarrusso said:

`simpl.`

on this goal won't make a difference, will it?

nope, of course I tried it, it makes zero progress

`simpl`

won’t make a difference on the goal, however `simpl`

on the hypothesis `H`

will be more helpful… And it should give you a good hint at what you should try and `destruct`

next.

Meven Lennon-Bertrand said:

`simpl`

won’t make a difference on the goal, however`simpl`

on the hypothesis`H`

will be more helpful… And it should give you a good hint at what you should try and`destruct`

next.

Enormous thanks to you, you got me unstuck ! I finished the proof!

Gantsev Denis has marked this topic as resolved.

Last updated: Sep 30 2023 at 05:01 UTC