The Coq mailing list

[Matt Ridsdale <matt.ridsdale AT cl.cam.ac.uk>]

Hi

I'm getting to know Coq and have proved 0 + x = x + 0 as a simple example.
I want to be able to re-use this result in proving further theorems.

Can anyone tell me why the result is accessible in the current environment
if
I prove it for Coq's native type nat, but not if I define nat myself using
the "Inductive" keyword?

Below is the Coq code and error message.


(* This works fine *)
Lemma z_plus_commutes : forall y:nat, plus 0 y = plus y 0.

intro y; elim y; auto; intro m; intro; simpl; rewrite <- H; simpl; auto.

Qed.

Check z_plus_commutes.

Coq < z_plus_commutes
     : forall y : nat, 0 + y = y + 0


======================================================================
(* This gives an error *)
Inductive mynat : Set :=          
| Q : mynat               
| T : mynat -> mynat.       

Definition myprim_rec := mynat_rec (fun i:mynat => mynat).

Definition myplus (n m:mynat) := myprim_rec m (fun p rec:mynat => T rec) n.

Lemma z_plus_commmutes : forall y : mynat, myplus Q y = myplus y Q.

intro y; elim y; auto; intro m; intro; simpl; rewrite <- H; simpl; auto.

Qed.

Check z_plus_commutes.

Coq < Toplevel input, characters 7-22
> Check z_plus_commutes.
>       ^^^^^^^^^^^^^^^
Error: The reference z_plus_commutes was not found in the current
environment


Apologies if this is something obvious, but I've looked through the forums
and a couple of tutorials
and can't see anything that relates to it.

cheers,

Matt
-- 
View this message in context: 
http://www.nabble.com/Check-lemma_name-gives-error-immediately-after-lemma-is-proved-tp21900669p21900669.html
Sent from the Coq mailing list archive at Nabble.com.