The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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