The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

The problem is that Coq doesn't have occurrence typing. M is still of type 
Exp t, when the return type is refined to Exp NAT.
You can eta-expand and pass in the term itself to get the refinement like so

Definition step' (t:Ty) (M:Exp t) : Exp t :=
  match M in Exp s return Exp s -> Exp s with
  | CONST c => fun M' => M'
  | IFZ t0 e1 e2 e3 =>
    fun _ =>
     match e1 with
     | CONST 0 => e2
     | _ => e3
     end
  end M.
-Ian
----- Original Message -----
From: "Randy Pollack" 
<rpollack AT inf.ed.ac.uk>
To: "Coq-Club Club" 
<coq-club AT inria.fr>
Sent: Friday, August 29, 2014 1:35:49 PM GMT -05:00 US/Canada Eastern
Subject: [Coq-Club] "Program"

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