The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I would also add that setting [i] and [o] as implicits is likely to be a bad idea, as you are likely to need to add '@' in some places, and when it is not needed, you might be lost when reading what you write. This is less likely to occur with constructors, and implicits should probably only used here.

Inductive Vop (A:Type) (i :nat) : nat -> Type :=
| Vid : Vop i
| Vappend : Vop (i + i)
| Vcompose : forall t o, Vop A t o -> Vop A i t -> Vop A i o
.

Arguments Vid: A i.
Arguments Vappend: A i.
Arguments Vcompose: {A} {t} {o} l r.

Also, the "Vappend" is quite misleading. Vduplicate or Vdouble would probably be better.
Or maybe, you would like to use this construction:

Vcat : forall i1 i2 o1 o2, Vop i1 o1 -> Vop i2 o2 -> Vop (i1+i2) (o1+o2)

2015-01-07 8:01 GMT+01:00 Amin Timany <amintimany AT gmail.com>:

Hi,

Looking at your inductive type definition for Vop, “i" and “o" seem not to be related: “Inductive Vop {A:Type} {i o:nat}: Type” but looking at your constructors, they are. “o” can be easily determined from “i” (and output size of the first Vop in case of Vcompose). Note that the proofs of equality (arguments of Vid and Vappend) are not considered by the type checker and thats why you need to use the program system to write your eval fixpoint. If you change you definition of Vop to the following, you won’t need the program system and you can define your fixpoint very easily and prove your lemma:

Inductive Vop {A:Type} {i :nat}: nat -> Type :=
| Vid : Vop i
| Vappend : Vop (i + i)
| Vcompose {t o:nat}: @Vop A t o -> @Vop A i t -> @Vop A i o
.

Fixpoint eval {A:Type} {i o:nat} (t:@Vop A i o) (x:Vector.t A i): Vector.t A o :=
 match t with
     | Vid => x
     | Vappend => Vector.append x x
     | Vcompose _ _ vop1 vop2 => ((eval vop1) ∘ (eval vop2)) x
 end.

Lemma test:
 forall A n (v:Vector.t A n),
   eval (
       Vcompose
         (Vappend)
         (Vid))
        v
   =
   eval (Vappend)
        v.
  Proof.
    trivial.
  Qed.

Regards,
Amin

> On 07 Jan 2015, at 04:21, Vadim Zaliva <vzaliva AT cmu.edu> wrote:
>
> Hi!
>
> I want to solicit some advise on designing proper representation for a simple language. Let us say we have a language which operates on vectors of type {A}. Each operator takes as an input a vector of size {i} and returns as an output a vector of size {o}. I've described the language by the following inductive type:
>
> Require Import Program.
> Require Import Vector.
> Import Vector.VectorNotations.
>
> Inductive Vop {A:Type} {i o:nat}: Type :=
> | Vid {H:i=o}: Vop
> | Vappend {H:o=i+i}: Vop
> | Vcompose {t:nat}: @Vop A t o -> @Vop A i t -> @Vop A i o
> .
>
> Now I can write 'eval' function which takes an operator (t:Vop) and input vector {x}
> of size {i} and returns a resulting vector of size {o}:
>
> Program Fixpoint eval {A:Type} {i o:nat} (t:@Vop A i o) (x:Vector.t A i): Vector.t A o :=
>  match t with
>      | Vid _ => x
>      | Vappend H => Vector.append x x
>      | Vcompose _ vop1 vop2 => ((eval vop1) ∘ (eval vop2)) x
>  end.
> Solve All Obligations using auto with arith.
>
> So far so good. Now let us try to prove a simple lemma:
>
> Lemma test:
>  forall A d n (v:Vector.t A n) {H:d=n+n} {H1:n=n},
>    eval (
>        Vcompose
>          (Vappend (H:=H))
>          (Vid (H:=H1) (o:=n)))
>         v
>    =
>    eval (Vappend (H:=H) (o:=d))
>         v.
>
> Once I try to prove this lemma I can see that it gets pretty messy due to 'eq_rect', lambda expressions and obligations which are part of the 'eval' definition:
>
> Proof.
>  intros.
>  unfold eval.
>  ...
>
> 1 subgoals, subgoal 1 (ID 93)
>
>  A : Type
>  d : nat
>  n : nat
>  v : t A n
>  H : d = n + n
>  H1 : n = n
>  ============================
>   ((fun x : t A n =>
>     eq_rect (n + n) (fun H0 : nat => t A H0) (append x x) d
>       (eval_obligation_2 A n d Vappend x H eq_refl))
>    ∘ (fun x : t A n =>
>       eq_rect n (fun H0 : nat => t A H0) x n
>         (eval_obligation_1 A n n Vid x H1 eq_refl))) v =
>   eq_rect (n + n) (fun H0 : nat => t A H0) (append v v) d
>     (eval_obligation_2 A n d Vappend v H eq_refl)
>
>
> It is also looks a bit weird to provide {H1:n=n} implicitly.
>
> This is a simplified example and my actual language will be more complex but it illustrates the kind of problems I am running into.
>
> Perhaps I am doing it wrong and there is a better way to define such language?
> Your advice is greatly appreciated.
>
> Sincerely,
> Vadim Zaliva
>