The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

If you want Coq to write your "convoy patterns" for you, you can 
program-by-proving, then print the result:

Definition step' (t:Ty) (M:Exp t) : Exp t.
simple inversion M.
- intros. exact M.
- intros e1 e2 e3.
  case e1.
  + intros. rewrite H2 in e2. exact e2.
  + intros. rewrite H2 in e3. exact e3.
Defined.

Print step'.

I find this to be much easier than either writing convoy patterns 
directly, or using Program, which seems rather buggy.  For instance, 
Program Definition doesn't work with the original definition of step 
(the one where Definition alone works).

-- Jonathan

On 08/29/2014 02:00 PM, J. Ian Johnson wrote:
> 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