The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Edsko de Vries wrote:
> Hey,
>
>   
> > 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.
> >     
>
> The 'match' statement returns a function; this function is then applied
> to 'v'.
>
> Edsko
>
> --------------------------------------------------------
> 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
>   
to be slightly more precise:  the expression that starts with "match" on 
line 3 and terminates
with "end" on line 6, is a function.  The type of this function is 

htree A (pred (S n)) -> htree A (pred (S n))

The type (htree A (pred (S n))) is actually convertible with (htree A 
n), which is the type of v,
so this function (the one returned by match ... end) can be applied to v.

Considering your first_of_htree', it is now a function with 5 arguments, 
while first_of_htree was
a function with 4 arguments.  This will probably change the way you can 
finish the exercise.

But the third argument of first_of_htree' is now useless (as shown by 
the fact that this
is bound to an anonymous variable) so you can define a third function 
first_of_htree'', that differs
with first_of_htree simply by the order of its arguments:

Definition first_of_htree'' : forall (A:Set) n (t:htree A (S n)), htree 
A n -> htree A n :=
 fun (A:Set)(n:nat)(t:htree A (S n)) =>
  match t in (htree _ n0) return (htree A (pred n0) -> htree A (pred 
n0)) with
    hleaf _=> fun v' : htree A (pred 0) => v'
  | hnode p _ t1 _ => fun _ : htree A (pred (S p)) => t1
  end.

Your last sentence, "btw ... end up nothing" was obscure to me, you can 
find a documentation of
"match" in section 1.2.13 of the reference manual.

Yves