The Coq mailing list

["Wan Hai" <wan.whyhigh AT gmail.com>]

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