## Stream: Coq users

### Topic: ✔ Stuck in combine_split

#### Gantsev Denis (Jan 27 2022 at 17:51):

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

#### Li-yao (Jan 27 2022 at 17:52):

Have you tried simplifying

#### Paolo Giarrusso (Jan 27 2022 at 21:30):

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

#### Gantsev Denis (Jan 27 2022 at 21:43):

Paolo Giarrusso said:

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

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

#### Meven Lennon-Bertrand (Jan 28 2022 at 09:20):

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

#### Gantsev Denis (Jan 28 2022 at 21:46):

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!

#### Notification Bot (Jan 28 2022 at 21:47):

Gantsev Denis has marked this topic as resolved.

Last updated: Jun 23 2024 at 23:01 UTC