Gantsev Denis (Jan 27 2022 at 17:51): 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:
simplwon’t make a difference on the goal, howeversimplon the hypothesisHwill be more helpful… And it should give you a good hint at what you should try anddestructnext.
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: Oct 13 2024 at 01:02 UTC