I am currently stuck at
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
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
Meven Lennon-Bertrand said:
simplwon’t make a difference on the goal, however
simplon the hypothesis
Hwill be more helpful… And it should give you a good hint at what you should try and
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