The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I do not like much to split your operator into three classes (Vop_i, Vop_o, others).

This distinction sounds awkward to me, and each lemma/definition will likely be split in three…

This is not much convenient, and reading will be harder.

Here are definitions using only indices for i and o.

I also added the implementation of your take and drop functions in the most natural way I found.

The main difficulty in this approach is to understand how the "match _ as _ in _ return _ with _ end" works.

It took me some time to understand how it works and how to use it. Do not expect to fully understand it at the first try.

But once you perfectly know how it works and how to use it, I think you cannot seriously be considered as a beginner in Coq.

So it can be worth to understand it, even if later, you find creative ways to avoid dealing with dependent pattern matching.

----------------------------------------------------------

Require Import Program.

Require Import Vector.

Import Vector.VectorNotations.

Inductive Vop (A : Type) : nat -> nat -> Type :=

| Vid : forall n, Vop A n n

| Vduplicate : forall i, Vop A i (i+i)

| Vhalf : forall o, Vop A (o+o) o

| Vconst : forall o, Vop A 1 o

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

| Vcross: forall i1 o1 i2 o2, Vop A i1 o1 -> Vop A i2 o2 -> Vop A (i1+i2) (o1+o2)

.

Arguments Vcompose {A} {i} {t} {o} v1 v2.

Arguments Vcross {A} {i1} {o1} {i2} {o2} v1 v2.

(* Helper functions *)

Definition take {A : Type} {m : nat} : forall p, Vector.t A (p+m) -> Vector.t A p :=

  fix take p :=

  match p as p return Vector.t A (p+m) -> Vector.t A p with

  | O => fun _ => nil A

  | S p => fun v => cons A (hd v) p (take p (tl v))

  end.

Definition drop {A : Type} {m : nat} : forall p, Vector.t A (p+m) -> Vector.t A m :=

  fix drop p :=

  match p as p return Vector.t A (p+m) -> Vector.t A m with

  | O => fun v => v

  | S p => fun v => drop p (tl v)

  end.

Definition eval {A:Type} : forall {i} {o}, Vop A i o -> Vector.t A i -> Vector.t A o :=

  fix eval {i} {o} op :=

  match op in Vop _ i o return Vector.t A i -> Vector.t A o with

  | Vid _ => fun v => v

  | Vduplicate _ => fun v => Vector.append v v

  | Vhalf o => fun v => take o v

  | Vconst o => fun v => Vector.const (hd v) o

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

  | Vcross n _ _ _ xop1 xop2 => fun v => Vector.append (eval xop1 (take n v))

                                                       (eval xop2 (drop n v))

end.

2015-01-10 2:48 GMT+01:00 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