I'm doing the Software foundations exercises and doing the combine_split
exercise I'm running into a wall when trying to prove an auxiliary lemma.
When applying reflexivity
within the assert
the Proof Process just hangs there despite the equation just being (x, y) = (x, y)
which is obviously true.
Here is the implementation
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
intros X Y.
intros l.
induction l as [| n l' IHl'].
- simpl. intros l1 l2 H. injection H as H1 H2. rewrite <- H1, <-H2. reflexivity.
- destruct n as [n1 n2]. simpl. destruct (split l').
intros l1 l2 H. injection H as H1 H2.
rewrite <- H1, <- H2. simpl.
assert ( Hc : combine x y = l'). { apply IHl'. reflexivity.}
apply Hc.
Qed.
Why is this happening?
Looks like a parsing bug in Proof General, in its sentence splitting. It appears to be sending reflexivity.}
to Coq based on the highlighting when you wanted it split into reflexivity.
and then }
as a separate command. In any case coqc
doesn't lex this as desired, interpreting .}
as a single (unknown) token. (I'm actually confused why if it's sending reflexivity.}
you don't get that lexing error.)
You can fix this by adding a space: reflexivity. }