The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

Hi John,

there  are  many  errors  when i run  this  though  solved  by  import  ZArith.

martin@ubuntu:~/hilbertreborn$ coqtop

Welcome to Coq 8.4pl6 (December 2015)

Coq < Require Import ZArith.

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).[Loading ML file z_syntax_plugin.cmxs ... done]

[Loading ML file quote_plugin.cmxs ... done]

[Loading ML file newring_plugin.cmxs ... done]

[Loading ML file omega_plugin.cmxs ... done]

Coq < Coq < Coq < Coq < tree is defined

tree_rect is defined

tree_ind is defined

tree_rec is defined

Coq < Coq < Coq < Coq < Coq < In is defined

In_ind is defined

Coq < Coq < Coq < Coq < is_empty is defined

Coq < Coq < Coq < 1 subgoal

  

  ============================

   forall s : tree, is_empty s = true <-> (forall x : Z, ~ In x s)

is_empty_correct < 1 subgoal

  

  ============================

   forall s : tree, is_empty s = true <-> (forall x : Z, ~ In x s)

is_empty_correct < 2 subgoals

  

  H : true = true

  x : Z

  H0 : In x Empty

  ============================

   False

subgoal 2 is:

 false = true

is_empty_correct < 1 subgoal

  

  s1 : tree

  z : Z

  s2 : tree

  H : forall x : Z, In x (Node s1 z s2) -> False

  ============================

   false = true

is_empty_correct < 1 subgoal

  

  s1 : tree

  z : Z

  s2 : tree

  H : forall x : Z, In x (Node s1 z s2) -> False

  ============================

   In z (Node s1 z s2)

is_empty_correct < destruct s; simpl; intuition.

 inversion_clear H0.

 elim H with z; auto.

Error: Attempt to save an incomplete proof

is_empty_correct < is_empty_correct < order is defined

order_rect is defined

order_ind is defined

order_rec is defined

is_empty_correct < is_empty_correct < compare is assumed

Warning: compare is declared as a parameter because it is at a global level

is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < mem is recursively defined (decreasing on 2nd argument)

is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < Toplevel input, characters 149-150:

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

>                         ^

Error: In environment

bst : tree -> Prop

x : ?177

l : tree

r : tree

y : Z

The term "y" has type "Z" while it is expected to have type 

"nat".

is_empty_correct < is_empty_correct < is_empty_correct < Toplevel input, characters 39-42:

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

>                ^^^

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

is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < is_empty_correct < Toplevel input, characters 74-75:

>   | Lt => x<y

>           ^

Error: In environment

x : Z

y : Z

The term "x" has type "Z" while it is expected to have type 

"nat".

is_empty_correct < is_empty_correct < Toplevel input, characters 13-25:

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

>             ^^^^^^^^^^^^

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

is_empty_correct < 

Regards,

Martin 

---

From: tesleft AT hotmail.com
To: johnw AT newartisans.com
CC: coq-club AT inria.fr
Date: Sat, 23 Jan 2016 09:50:24 +0800
Subject: RE: [Coq-Club] how to run this program to verify a simple function?

Hi  ,

when i continue to run,  got  some  error

[Loading ML file quote_plugin.cmxs ... done]

[Loading ML file newring_plugin.cmxs ... done]

[Loading ML file omega_plugin.cmxs ... done]

Coq < Coq < Coq < Coq < Error: tree already exists.

Coq < 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.Coq < Coq < Coq < Toplevel input, characters 192-193:

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

>                                       ^

Error: In environment

In : Z -> tree -> Prop

x : Z

l : tree

r : ?8

The term "x" has type "Z" while it is expected to have type 

"tree".

Regards,

Martin 

> From: johnw AT newartisans.com
> To: tesleft AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] how to run this program to verify a simple function?
> Date: Fri, 22 Jan 2016 17:48:17 -0800
>
> >>>>> Mandy Martino <tesleft AT hotmail.com> writes:
>
> > Error: The reference Z was not found in the current environment.
>
> I'm not sure whether the course defines Z some place, but otherwise you should
> just need:
>
> Require Import ZArith.
>
> --
> John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2