The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Jan 8, 2015, at 17:39 , Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Unfortunately even I am not using equalities in type definition I’ve ended up with using “Program” for 

evalVop definition. I am still investigating how it has arisen. But with your help I have certainly already

made a great progress.

Here is the situation where I have not managed avoid “Program". Going along the lines of Amir’s 

suggestion, I have added one more high-level operator called Vcross. It takes two other operators

as parameters. Applies each of them to a part of input vector and returns concatenation of their results.

Unfortunately such definition leads to use of Program in eval, which in turns generates obligations

which makes profs extremely difficult.

Here is the problematic constructor:

Vcross: forall {x a:nat}  {Ca:a<=o} {Cx:x<=i}, @Vop A x a -> @Vop A (i-x) (o-a) -> @Vop A i o

Ca and Cx could be avoided if I use addition instead of multiplication:

Vcross: forall {i1 i2 o1 o2:nat}, @Vop A i1 o1 -> @Vop A i2 o2 -> @Vop A (i1+i2) (o1+o2)

and make it constructor of a new type Vop_io {A:Type}: nat -> nat-> Type. But I need

to use any Vop operators as parameters of Vcross, not just Vop_io. Defining Vop

and Vop_io types together seems to be a solution, but in this they both must have same 

parameters.

Unless I am missing something I do not see a way to avoid Cx and Ca.

P.S. The good news that for all other operators new type system works nicely and I was able to prove a lot

of lemmas I needed to prove on them.

Full example below:

Require Import Program.

Require Import Vector.

Import Vector.VectorNotations.

Inductive Vop_i {A:Type} (i:nat) : nat -> Type :=

| Vid: Vop_i i i

| Vduplicate: Vop_i i (i + i)

.

Inductive Vop_o {A:Type} (o:nat) : nat -> Type :=

| Vhalf : Vop_o o (o + o)

| Vconst : Vop_o o 1

.

Inductive Vop {A : Type} {i o : nat} :=

| VI : @Vop_i A i o -> Vop

| VO : @Vop_o A o i -> Vop

| Vcompose : forall t, @Vop A t o -> @Vop A i t -> @Vop A i o

| Vcross: forall {x a:nat}  {Ca:a<=o} {Cx:x<=i}, @Vop A x a -> @Vop A (i-x) (o-a) -> @Vop A i o

.

(* Helper functions *)

Definition take {A} {m} (p:nat) : Vector.t A (p+m) -> Vector.t A p.  admit. Defined.

Definition drop {A} {m} (p:nat) : Vector.t A (p+m) -> Vector.t A m. admit. Defined.

Definition eval_i {A:Type} {i o:nat} (t:@Vop_i A i o) (x:Vector.t A i): Vector.t A o :=

match t with

  | Vid => x

  | Vduplicate => Vector.append x x

end.

Definition eval_o {A:Type} {i o:nat} (t:@Vop_o A o i) (x:Vector.t A i): Vector.t A o :=

(match t in @Vop_o _ _ i return Vector.t A i -> Vector.t A o 

  with

    | Vhalf => fun y => take (m:=o) o y

    | Vconst => fun y => Vector.const (hd (n:=0) y) o

  end) x.

Program Fixpoint eval {A:Type} {i o:nat} (t:@Vop A i o) (v:Vector.t A i): Vector.t A o :=

match t with

  | VI vi => eval_i vi v

  | VO vo => eval_o vo v

  | Vcompose _ vop1 vop2 => ((eval vop1) ∘ (eval vop2)) v

  | Vcross x _ _ _ xop1 xop2 =>  Vector.append

                                   (eval xop1 (take (m:=(i-x)) x v))

                                   (eval xop2 (drop x v))

end.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD student

Mobile: +1(510)220-1060

Skype: vzaliva