The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

  Dear Hendrik Boom,

> Thanks for your reply, but I'm sorry to say that I'm still not out
> of the woods.

  ... what you try to do is actually very subtle!

> As far as I understand from the manual, the <> notation serves to specify
> the type returned by the cases construction.  Somehow your suggestion 
> implies
> that the bound variables inside the type inside the angle brackets
> are somehow accessible inside the Cases clause. 

  Yes.

> Where is this documented?

  Sections 2.2 and 4.5.4 of the reference manual.
 
> Your example works -- the simplified version with the "en" removed.
> Unfortunately, it is now the "en" in the real case that is giving me 
> problems.
> 
> Following your advice. I tried 
> 
>     Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
> (hasType1 e x t)] : t
>     :=
>       <[e; x; t; p : (hasType1 e x t)]t>
>       Cases p of
>         (typedId e x t zzz) => (en x)
>       | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) 
> (eval x2 e2 t2 en r2)) 
>       | (isfn e x xt body bt q) =>
>       [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en i))) 
> q)
>       end
>     .

  Since "en" is a mapping expected in correspondence with "e", you
need to express this dependency. The solution is to move deeply "en"
in your definition as follows:

Fixpoint eval[x:exp; e:env; t:Set;p:(hasType1 e x t)]: ((u:Id) (e u)) -> t
    :=
      <[e; x; t; p : (hasType1 e x t)]((u:Id) (e u))-> t>
      Cases p of
        (typedId e x t www) => [en:(u:Id) (e u)](en x)
      | (iscall e2 f2 x2 t2 tx2 q2 r2) => [en:(u:Id) (e2 u)]
          ((eval f2 e2 (tx2->t2) q2 en) (eval x2 e2 tx2 r2 en)) 
      | (isfn e x xt body bt q) => [en:(u:Id) (e u)]
        [z : xt](eval body ([i]if (eqId i x) then xt else (e i)) bt q 
[i:Id](<[b:bool](if b then xt else (e i))>if (eqId i x) then z else (en i)))
      end.

Please notice I also changed "e" in the last clause to some expression
in correspondence with the new assignment
"[i : Id](if (eqId i x) then z else (en i))".

  This definition of eval works ... almost.

  It remains a subtlety, Coq cannot deal with: to recognize that if
zzz:(e x)==t then (en x) of type (e x) has also type t. Coq does not
use equations based on Leibniz equality to check equality (actually
convertibility) between types.

  The solution is to change the definition of hasType1 as follows

Inductive hasType1 : env -> exp -> Set -> Set :=
  | typedId : (e: env)(x:Id)(hasType1 e (id x) (e x))
  | iscall : (e : env)(f : exp)(x : exp) (t : Set) (tx : Set)
        (hasType1 e f (tx->t))
      ->(hasType1 e x tx) -> (hasType1 e (call f x) t)
  | isfn : (e:env)(x : Id)(xt : Set)(body : exp)(bt : Set)
        (hasType1 ([i : Id] (if (eqId i x) then xt else (e i))) body bt)
      ->(hasType1 e (fn x body) (xt->bt)).

  (Notice that the type of x is now directly taken to be (e x)), then
the following definition (no more "zzz") works:

Fixpoint eval[x:exp; e:env; t:Set;p:(hasType1 e x t)]: ((u:Id) (e u)) -> t
    :=
      <[e; x; t; p : (hasType1 e x t)]((u:Id) (e u))-> t>
      Cases p of
        (typedId e x) => [en:(u:Id) (e u)](en x)
      | (iscall e2 f2 x2 t2 tx2 q2 r2) => [en:(u:Id) (e2 u)]
          ((eval f2 e2 (tx2->t2) q2 en) (eval x2 e2 tx2 r2 en)) 
      | (isfn e x xt body bt q) => [en:(u:Id) (e u)]
        [z : xt](eval body ([i]if (eqId i x) then xt else (e i)) bt q 
[i:Id](<[b:bool](if b then xt else (e i))>if (eqId i x) then z else (en i)))
      end.

  Hope it helps,

                                                  Hugo Herbelin

PS:

Coq < Eval Compute in
    (eval (id (makeid O)) [id]nat nat (typedId [id]nat (makeid O)) [u](S O)).
      = (S O)
     : nat

Fine!