Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] toy language

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] toy language


Chronological Thread 
  • From: Vadim Zaliva <vzaliva AT cmu.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] toy language
  • Date: Fri, 9 Jan 2015 17:48:21 -0800


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




Archive powered by MHonArc 2.6.18.

Top of Page