The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> 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