The Coq mailing list

[Hendrik Boom <hendrik AT topoi.cam.org>]

Now I think I have figured it out.

>   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!

Subtleties are what tests the limits of a logic.

> 
> > 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.

My experiments suggest otherwise. (well, maybe not if you stretch the
meaning of "somehow").  When I change the names of just those variables,
eveything still works.

A detailed analysis of one of the cases follows, as a check that I
now have it right.  I haven't found this stuff explained clearly
anywhere yet.  So if I *am* right, perhaps I should write a few paragraphs
for the manual.  Or perhaps a version of this text should be included
as an example.

Here are the most relevant definitions.  (The entire file is appended
after this message for reference).

Inductive hasType1 : env -> exp -> Set -> Set :=
  | typedId : (e : env) (x : Id) (hasType1 e (id x) (e x))
        (* Unfortunately, this does not constrain the third arg. *)
  | 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))
.

Fixpoint eval3[x : exp; e : env; t : Set; p : (hasType1 e x t)] : ((u : Id) 
(e u)) -> t
:=
  <[e0; x0; t0; p0 : (hasType1 e0 x0 t0)] ((v : Id)(e0 v)) -> t0>
  (* a function that,
     given the args to the inductive type and a value of the inductive type,
     returns the type to be returned by the cases expression.
  *)
  Cases p of
    (typedId e1 x1) => [en : (u : Id) (e1 u)](en x1)
  | (iscall e2 f2 x2 t2 tx2 q2 r2) => [en : (w : Id) (e2 w)]((eval3 f2 e2 
(tx2->t2) q2 en) (eval3 x2 e2 tx2 r2 en)) 
  | (isfn e x xt body bt q) =>
        ([en : (uu : Id) (e uu)]
           [z : xt]
             ( eval3 body ([i : Id](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
.

For the sake of clarity, I have provided distinct names for many of the
distinct variables in eval2.

It appears that the expression in the <> brackets before "Cases"
is a type-valued function, called the elimination function.  Its parameters
are:
    one argument for each parameter of the inductive type being deconstructed
    one argument for a value of the inductive type being deconstructed.
It returns the type that the Cases clause is to return, expressed
in terms of these parameters. 

It was the parameters and value of the elimination function that
were the key information I fought hard to find.  Once I had those,
some experimentation and thinking revealed a possible mechanism:

In this case, we are deconstructing p : (hasType e x t).  hasType is an
inductive type whose parameters are e : env, x : exp, and t : Set.
So the parameters for the elimination function are
[e0; x0; t0; p0 : (hasType1 e0 x0 t0)], which appears in this context to be
an acceptable abbreviation for
[e0 : env; x0 : exp; t0 : Set; p0 : (hasType1 e0 x0 t0)]
I used new variables e0, x0, t0, and p0 because I could. and thereby
I avoided confusion with other vaiables named e, x, t, and p.
Notice that the type of p0 is expressed in terms of e0, x0, and t0 instead
of e, x, and t.

The elimination function returns the type being returned by the Cases clause,
again expressed in terms of e0, x0, t0, and p0.  The language does
not require you to use the parameters of the elimination function,
but this example won't work if you don't.

Now let us examine how coq can type-check the first case:

  Cases p of
    (typedId e1 x1) => [en : (u : Id) (e1 u)](en x1)
  | ...

p is of type (hasType1 e x t).

Consider the corresponding part of the definition of hasType1:

Inductive hasType1 : env -> exp -> Set -> Set :=
  | typedId : (e : env) (x : Id) (hasType1 e (id x) (e x))
  | ...

This gives us:
    (typedId e1 x1) : (hasType1 e1 (id x1) (e1 x1))
    e1 : env
    x1 : Id

coq tries to find arguments for the parameters e0, x0, t0 of the
elimination function that will the last parameter p0 have the
type (hasType1 e1 (id x1) (e x1)), which is the type of (typedId e1 x1).
Obviously, we must fill in e1 foe e0, (id x1) for x0, and (e x1) for t0.
With these arguments, the value of the elimination function is the
type ((v : Id)(e1 v) -> (e1 x1).
Does the first case [en : (u : Id) (e1 u)](en x1) have this type?
Let's see. It's a function that returns the value (en x1).  Now the
type of the type of en is (u : Id) (e1 u), so (en x1) has the type (e1 x1),
and [en : (u : Id) (e1 u)](en x1) is of type (en : (u : Id) (e1 u))(e1 x1).

Yes, that's what we need.

-- hendrik.


And here's the entire file:


Inductive Id : Set := makeid : nat -> Id .

Hypothesis inteq : nat -> nat -> bool.

Definition eqId : Id -> Id -> bool :=
  [i : Id][j : Id]
    Cases i of
      (makeid ian) =>
        Cases j of
          (makeid jn) => (inteq ian jn)
        end
    end.

Inductive exp : Set :=
  | id : Id -> exp
  | call : exp -> exp -> exp
  | fn : Id -> exp -> exp.

Inductive exp2 : Set :=
  | id2 : Id -> exp2
  | exp2IsCall : Call -> exp2
  | exp2IsFn : Fn -> exp2
with Call : Set :=
  | call2 : exp2 -> exp2 -> Call
with Fn : Set :=
  | fn2 : Id -> exp2 -> Fn.

Definition env : Type := (id : Id)Set.

Inductive hasType1 : env -> exp -> Set -> Set :=
  | typedId : (e : env) (x : Id) (hasType1 e (id x) (e x))
        (* Unfortunately, this does not constrain the third arg. *)
  | 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))
.

Fixpoint eval3[x : exp; e : env; t : Set; p : (hasType1 e x t)] : ((u : Id) 
(e u)) -> t
:=
  <[e0; x0; t0; p0 : (hasType1 e0 x0 t0)] ((v : Id)(e0 v)) -> t0>
  (* a function that,
     given the args to the inductive type and a value of the inductive type,
     returns the type to be returned by the cases expression.
  *)
  Cases p of
    (typedId e1 x1) => [en : (u : Id) (e1 u)](en x1)
  | (iscall e2 f2 x2 t2 tx2 q2 r2) => [en : (w : Id) (e2 w)]((eval3 f2 e2 
(tx2->t2) q2 en) (eval3 x2 e2 tx2 r2 en)) 
  | (isfn e x xt body bt q) =>
        ([en : (uu : Id) (e uu)]
           [z : xt]
             ( eval3 body ([i : Id](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
.