The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Gregory,

Thanks for your suggestion. I do not think this is what I am trying to 
achieve.
I have to tweak it a bit to your code a little by replacing 
PeanoNat.Nat.eq_dec with
Coq.Arith.Peano_dec.eq_nat_dec. However:

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

gives me:

= Some (TA 0) : option (Target 0 0)

Which is incorrect. Informally what I am trying to do is to have a source type
parametrized by ‘x’ and ‘y’ which are unconstrained and target
type which parameters ‘i’ and ‘j’ are dependent.

My compile function checks if given values of ‘x’ and ‘y’ do match type 
constraints
of the target type return a value of it. Otherwise it returns None.

So, in example above (SA (x:=2) (y:=2)) could not be compiled to (TA (i:=2) 
(j:=2))
since ‘i’ and ‘j’ values are not satisfying constraints that j must be twice 
the
value of i.

One can think of my ‘Source' type as a language which defines some abstract 
syntax.
It allows to define expressions which are syntactically correct but not always
valid. Compilation to target language checks some additional constraints and 
may
reject some original expressions as invalid. My function ‘f’ may be viewed as 
variable resolution mechanism, which convert variable names in the original 
syntax to their 
value in the target language. For example x/y is syntactically correct in 
source language 
but once we resolve ‘x’ and ‘y’ to their values, we may reject expressions 
where y=0.

I hope this makes sense.

Sincerely,
Vadim


> On May 25, 2015, at 20:43 , Gregory Malecha 
> <gmalecha AT cs.harvard.edu>
>  wrote:
> 
> 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.
> 

Sincerely,
Vadim Zaliva

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