The Coq mailing list

["许庆国" <qgxu AT mail.shu.edu.cn>]

Hello coq user:

-----------------------------------------------
Definition first_of_htree :
  forall (A:Set) (n:nat), htree A n -> htree A (S n) -> htree A n.
  intros A n v t.
 generalize v.
 change (htree A (pred (S n)) -> htree A (pred (S n))).
 case t.
 intros x v'; exact v'.
 intros p x t1 t2 v'; exact t1.
Defined.
--------------------------------------------------

I think "first_of_htree" is a function. Is it necessary for the definiionare 
to have the corresponding proof scripts " intros A.... exact t1."
"first_of_three" should take 2 arguments-- one of is type of " htree A n" , 
and the other is type of " htree A (S n)"-- and then can give us the result 
type of   "htree A n".
Hence,  the proof scripts  should be replaced by the form of  " :=  ... " 
instead.   and  ":=..." should provide the process for how to   apply the 2 
arguments and how to calculate the associated results.

What's the problem about my opinion? 

Thanks for your any reply.

2010-09-12 

Qgxu



From:  Wan Hai 
Date:  2007-11-20  21:18:07 
To:  Coq Club 
Cc:  
Subject:  [Coq-Club] about the exercise 6.46 in Coq Art book 
  
Dear all
I am working on the exercise 6.46 in Coq Art.
---------------------
Inductive htree (A:Set) : nat -> Set :=
  | hleaf : A -> htree A 0
  | hnode : forall n:nat, A -> htree A n -> htree A n -> htree A (S n).
Definition first_of_htree :
  forall (A:Set) (n:nat), htree A n -> htree A (S n) -> htree A n.
 intros A n v t.
 generalize v.
 change (htree A (pred (S n)) -> htree A (pred (S n))).
 case t.
 intros x v'; exact v'.
 intros p x t1 t2 v'; exact t1.
Defined.
---------------------
After first_of_htree is defined, I used the Print command to see the
detail of first_of_htree, I got this:
---------------------
1) first_of_htree =
2) fun (A : Set) (n : nat) (v : htree A n) (t : htree A (S n)) =>
3) match t in (htree _ n0) return (htree A (pred n0) -> htree A (pred n0)) 
with
4) | hleaf _ => fun v' : htree A (pred 0) => v'
5) | hnode p _ t1 _ => fun _ : htree A (pred (S p)) => t1
6) end v  (*this v confused me*)
7)      : forall (A : Set) (n : nat), htree A n -> htree A (S n) -> htree A n
---------------------
I do not know the exact meaning of "end v" in the sixth line.
I defined a first_of_htree' similar to first_of_htree as this:
---------------------
1) first_of_htree' =
2) fun (A : Set) (n : nat) (_ : htree A n) (t : htree A (S n)) =>
3) match t in (htree _ n0) return (htree A (pred n0) -> htree A (pred n0))
4) | hleaf _ => fun v' : htree A (pred 0) => v'
5) | hnode p _ t1 _ => fun _ : htree A (pred (S p)) => t1
6) end
7)      : forall (A : Set) (n : nat),
8)        htree A n ->
9)        htree A (S n) -> htree A (pred (S n)) -> htree A (pred (S n))
---------------------
the two definitions differed only in the sixth line, one has "v" and
one does not. This "v" makes their types different.
Could any one explain why?
btw, I search the manual using key word "match", it seems that, all
the "end"s corresponding to "match" are end up with nothing.
-- 
Hai Wan
--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club