The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hi, Vadim --

I have found this to be a pretty good way to formalize things if you want to use dependent types. The alternative, which some people will prefer, is to write the simply-typed version and have a separate proof that the output that you produce has the desired property. This can be convenient for some things because it avoids some of the complexity of dependent types, but it can also be quite annoying because (in some cases) you will need to prove that your function always returns a "good" target object. Some of the tradeoffs are outlined in Chapter 4 of my dissertation (http://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory.html). My dissertation opts for no dependent types purely for computational efficienty.

On Tue, May 26, 2015 at 6:47 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

> On May 26, 2015, at 18:12 , Vadim Zaliva <vzaliva AT cmu.edu> wrote:
>
> Compute compile (i:=0) (j:=0) (fun x => x) (SA 2 2).
>
> gives me:
>
> = Some (TA 0) : option (Target 0 0)
>
> Which is incorrect.

I think the link between formal and computed values of ‘i' and ‘j' was missing.
I’ve modified you example by adding one ‘if’ statement:

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 ni i) && (beq_nat nj j) then
      cast_nat (Target i) (i+i) j (TA i)
    else
      None
  | SB i j => None
  end.

and now it works as expected:

The following:

Compute compile (i:=2) (j:=2) (fun x => x) (SA 2 2).
Compute compile (i:=20) (j:=40) (fun x => x) (SA 2 2).
Compute compile (i:=2) (j:=2) (fun x => x) (SA 1 2).
Compute compile (i:=20) (j:=40) (fun x => x) (SA 1 2).

return ‘None'. And the following:

Compute compile (i:=1) (j:=2) (fun x => x) (SA 1 2).

returns 'Some (TA 1)’

I am still not 100% sure that this is the best way to formalize my problem but I will experiment with it more. Thanks for your help!

Sincerely,
Vadim Zaliva

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

--

gregory malecha