Stream: Coq users

Topic: ✔ Stuck in combine_split


view this post on Zulip 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 ?..

view this post on Zulip Li-yao (Jan 27 2022 at 17:52):

Have you tried simplifying

view this post on Zulip Paolo Giarrusso (Jan 27 2022 at 21:30):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Notification Bot (Jan 28 2022 at 21:47):

Gantsev Denis has marked this topic as resolved.


Last updated: Mar 29 2024 at 06:39 UTC