The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Yet another approach to this:

If you are willing to dispense with "real" type indexes and instead 
simulate them with type parameters and equalities (t=NAT in CONST), then 
Coq's match is most happy - at least in this case (your mileage may vary 
in more complex cases):

Inductive Exp(t : Ty) : Type :=
| CONST: nat -> t=NAT -> Exp t
| IFZ  : Exp NAT -> Exp t -> Exp t -> Exp t.

Definition step(t:Ty)(M:Exp t) : Exp t :=
match M with
| CONST _ _ _ => M
| IFZ _ (CONST _ _ _) e2 _ => e2
| IFZ _ (IFZ _ _ _ _) _ e3 => e3
end.

I have read that there are proposals for modifying Coq's match (or 
adding a new match-like construct) that does the type-index-induced 
context alterations in the branches - so that it becomes more like what 
is available in Agda or Idris, where one can use type indexes and not 
need to use anonymous functions (the convoy pattern), which damage the 
readability (and writability).

-- Jonathan

On 08/30/2014 03:19 AM, Cédric wrote:
> Le Fri, 29 Aug 2014 19:35:49 +0200, Randy Pollack 
> <rpollack AT inf.ed.ac.uk> a écrit:
>
> > Here is a very cut down example that checks in version 8.4pl3:
> >
> > ===============
> > Inductive Ty := NAT | A.
> >
> > Inductive Exp : Ty -> Type :=
> > | CONST: nat -> Exp NAT
> > | IFZ  : forall t, Exp NAT -> Exp t -> Exp t -> Exp t.
> >
> > Definition step (t:Ty) (M:Exp t) : Exp t :=
> >   match M in Exp s return Exp s with
> >     | CONST c => CONST c
> >     | IFZ t0 e1 e2 e3 =>
> >       match e1 with
> >         | CONST 0 => e2
> >         | _ => e3
> >       end
> >   end.
> > =================
> >
> > I want to replace the first match case of [step]  with
> >
> >      | CONST c => M
> >
> > so I tried
> >
> > ========================
> > Program Definition step (t:Ty) (M:Exp t) : Exp t :=
> >   match M in Exp s return Exp s with
> >     | CONST c => M
> >     | IFZ t0 e1 e2 e3 =>
> >       match e1 with
> >         | CONST 0 => e2
> >         | _ => e3
> >       end
> >   end.
> > ========================
> >
> > which fails with:
> >
> > Error: The variable anonymous' was not found in the current environment.
> >
> > Thanks for any help with making my Definition work.
> >
> > --Randy
>
> I am not sure you find it acceptable, but you can use:
>
> Definition step (t:Ty) (M:Exp t) : Exp t :=
>   match M in Exp s return Exp s -> Exp s with
>     | CONST c => fun x (* is in fact bound to M *) => x
>     | IFZ t0 e1 e2 e3 => fun _ =>
>       match e1 with
>         | CONST 0 => e2
>         | _ => e3
>       end
>   end M (* M is out of the match, so there is no typing issue *).