The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hello --

Something like the following might be helpful:

Definition cast_nat (F : nat -> Type) (a b : nat) (x : F a) : option (F b) :=

  match PeanoNat.Nat.eq_dec a b with

  | left pf => Some match pf in _ = t return F t with

                    | eq_refl => x

                    end

  | right _ => None

  end.

(* 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

    cast_nat (Target i) (i+i) j (TA i)  (* <-- cast [Target i (i+i)] to [Target i j] *)

  | SB i j => None

  end.

Essentially the [cast_nat] function performs a decidable equality an then uses the proof to cast the result.

On Fri, May 22, 2015 at 8:08 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/