The Coq mailing list

[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
>