The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

Hi  ,

i follow 

http://www.lix.polytechnique.fr/~barras/mpri/notes/cours007.html

got  error  when  run in coqtop  

Error: The reference Z was not found in the current environment.

Inductive tree : Set := 

| Empty

| Node : tree -> Z -> tree -> tree.

Inductive In (x:Z) : tree -> Prop :=

| In_left : forall l r y, (In x l) -> (In x (Node l y r))

| In_right : forall l r y, (In x r) -> (In x (Node l y r))

| Is_root : forall l r, (In x (Node l x r)).

Definition is_empty (s:tree) : bool := match s with

| Empty => true

| _ => false end.

Theorem is_empty_correct : 

forall s, (is_empty s)=true <-> (forall x, ~(In x s)).

Proof.

destruct s; simpl; intuition.

inversion_clear H0.

elim H with z; auto.

Qed. 

Inductive order : Set := Lt | Eq | Gt.

Hypothesis compare : Z -> Z -> order.

Fixpoint mem (x:Z) (s:tree) {struct s} : bool := match s with

| Empty => 

   false

| Node l y r => match compare x y with

   | Lt => mem x l

   | Eq => true

   | Gt => mem x r

  end

end.

Inductive bst : tree -> Prop :=

| bst_empty : 

   (bst Empty)

| bst_node : 

   forall x (l r : tree),

   bst l -> bst r -> 

   (forall y, In y l -> y < x) ->

   (forall y, In y r -> x < y) -> bst (Node l x r).

Theorem mem_correct : 

  forall x s, (bst s) -> (mem x s=true <-> In x s).

Hypothesis compare_spec :

  forall x y, match compare x y with

  | Lt => x<y

  | Eq => x=y

  | Gt => x>y

  end.

generalize (compare_spec x z); destruct (compare x z).

Regards,

Martin