The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Dear Coq experts,

I am looking for some guidance on how to approach in Coq a seemingly simple 
problem.
Consider a simple compiler from source to target language, both defined via
inductive types. Target language has stronger typing and not every expression
in source language could be compiled into target. Below is a sample 
definition:

Require Import Coq.Arith.EqNat.
Require Import Coq.Bool.Bool.
Require Import Coq.Program.Program.

(* Source language *)
Inductive Source: nat -> nat -> Type :=
| SA (i j:nat): Source i j
| SB (i j:nat): Source i j.

(* Target language *)
Inductive Target : nat -> nat -> Type :=
| TA (i:nat): Target i (i+i)
| TB: Target 0 1.

Now I want to define the compiler function. Something like this:

(* Compiler from source to target. *)
Definition compile {x y i j} (f:nat->nat) (a:Source x y): option (Target i j) 
:=
  match a with
  | SA x y =>
    let ni := f(x) in
    let nj := f(y) in
    if (beq_nat i (j+j)) && (beq_nat ni i) && (beq_nat nj j) then
      Some (TA i)
    else
      None
  | SB i j => None
  end.

In this example ‘f’ is introduced to demonstrate that mapping between
x,y and i,j is not static.

The compiler returns ‘None' if expression could not be compiled and (Some 
Target)
it it could be compiled. For example:

Lemma test1: compile (i:=0) (j:=0) (fun x => x) (SA 2 2) = None.
Lemma test2: compile (fun x => x) (SA 1 2) = Some (TA 1).

My ‘compile’ definition above in incorrect and probably require some tricky
type conversion to make it work. I guess some ‘match’-ing to convince type
checker that i=(j+j). Probably for that I will have to use something like
‘beq_nat_eq’ from standard library.

Assuming I will manage to make it work, a more general question is whenever it
is this the right approach to do things like this? At the end I will have many
constructors for both types and compile function will become quite big and 
complex. 
Using things like ‘refine’ and/or Program might complicate things even more. 
Maybe
there is a pattern how write definitions like this, perhaps splitting it into
several functions? Maybe some of them are easier to proof as lemmas, not write
as functional programs?

Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva