The Coq mailing list

[Ricardo Sousa <c0107040 AT alunos.dcc.fc.up.pt>]

Hi.
In the exercise 6.29, where i can only use certain rules to prove
"Theorem plus_n_O : forall n, n+0 =n.", there is a problem in the given
solution
(http://www.labri.fr/perso/casteran/CoqArt/structinduct/SRC/plus_n_O.v)
on the application step.

Open Scope nat_scope.

Theorem plus_n_O : forall n, n+0 =n.
Proof.
 intro n; elim n; simpl.
 reflexivity.
 intros n0 e.
 apply eq_ind with (P:= fun n => S(n0 + 0) = S n) (x:= n0 + 0).
 reflexivity.
 assumption.
Qed.

I can't find why this doesn't work.
I also don't understand in which step of the unification this error
corresponds. Is in the app rule? Or is in other?

Toplevel input, characters 260-324
> apply eq_ind with (P:= fun n1 => S (n0 + 0) = S n1)(x:= (n0 +0)).
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Impossible to unify "S (n0 + 0) = S ?29" with "S n0 = S n0 + 0"

Thank you in advance,
Ricardo Sousa

Attachment: signature.asc
Description: OpenPGP digital signature