The Coq mailing list

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

My apologies. Was my mistake transcribing the question of the exercise.
nat do the difference :)

Once again, thank you.
Ricardo Sousa

Pierre Casteran wrote:
> 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
>>
>>
>>
>>
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature