coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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” forevalVop definition. I am still investigating how it has arisen. But with your help I have certainly alreadymade 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
Vadim Zaliva
--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva
- [Coq-Club] toy language, Vadim Zaliva, 01/07/2015
- Re: [Coq-Club] toy language, Amin Timany, 01/07/2015
- Re: [Coq-Club] toy language, Cedric Auger, 01/07/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/08/2015
- Re: [Coq-Club] toy language, Amin Timany, 01/08/2015
- Re: [Coq-Club] toy language, Cedric Auger, 01/08/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/08/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/09/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/10/2015
- Re: [Coq-Club] toy language, Cedric Auger, 01/10/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/12/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/10/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/09/2015
- Re: [Coq-Club] toy language, Vadim Zaliva, 01/08/2015
- Re: [Coq-Club] toy language, Amin Timany, 01/07/2015
Archive powered by MHonArc 2.6.18.