The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Ricardo Sousa 
<c0107040 AT alunos.dcc.fc.up.pt>:


Hi,
 I tried again this solution with coqV8 (pl3) and found no problem.

 Could you send me a script of the session?

Pierre





> 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
>
>
>
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.