The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Amin & Cedric,

Thank you for your suggestions. It was very helpful. I changed my type to 
make "o" dependent
on "i" and it simplified things a bit. I tried to make "A" and "i" explicit, 
but it turns out it is more terse to have them implicit as there are not too 
many cases where I have to use "@".

Unfortunately there are few more cases which still lead to unsolved 
obligations and I have to resort back to "Program" to solve them. Here is the 
example modified by adding two more operators: Vhalf and Vconst. With these 
two operators I want to illustrate two patterns I encounter in my operator 
language:

1. Fixed size of input vector {H:i=1}.
2. Input vector size is twice the output: {H:i=o+o}

Unfortunately these lead to obligations in 'eval'. My first question is there 
is a better
way to represent these 2 patterns?

Require Import Program.
Require Import Vector.
Import Vector.VectorNotations.

Inductive Vop {A:Type} {i:nat} : nat -> Type :=
| Vid: Vop i
| Vduplicate: Vop (i + i)
| Vhalf {o:nat} {H:i=o+o}: Vop o
| Vconst {o:nat} {H:i=1}: Vop o
| Vcompose : forall t o, @Vop A t o -> @Vop A i t -> @Vop A i o
.
(* Helper function *)
Definition take {A} {m} (p:nat) : Vector.t A (p+m) -> Vector.t A p.  admit. 
Defined.

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
    | Vhalf o H => take (m:=o) o x
    | Vduplicate => Vector.append x x
    | Vconst o H => Vector.const (hd (n:=0) x) o
    | Vcompose _ _ vop1 vop2 => ((eval vop1) ∘ (eval vop2)) x
end.

Lemma test1:
  forall A n (v:Vector.t A n),
    eval (Vcompose _ _ (Vduplicate) (Vid)) v = eval (Vduplicate) v.
 Proof.
   trivial.
 Qed.

 Lemma test2:
   forall A n {n2:nat} {H:n2=n+n} (v:Vector.t A n2) ,
     eval (Vcompose _ _ (Vhalf (H:=H)) (Vid)) v = eval (Vhalf (H:=H) (o:=n)) 
v.
 Proof.
   intros.
   unfold eval.
   trivial. 
 Qed.

We are lucky the second lemma is also solved by "trivial", but in some more 
complex situations
where I have a complex expression constructed from many operators "trivial" 
does not work.

My second question/thought is about dealing with coercions in the eval code. 
For example I have {H:i=1} and implementation expects vector of type (vector 
A 1) I have auto generated type coercion from (vector A i) to (vector A 1) 
using eq_rect and "H". When I am trying to prove something about this code I 
have to deal with this eq_rect. I would love to be able to get rid of this 
coercion, and instead add "H" to my proof context. Perhaps it is better 
illustrated by an example:

Inductive T {i:nat} : Type :=
| T1 {H:i=1}: T.

Definition f {A:Type} (x:Vector.t A 1) : A := hd x.

Program Definition evalT {i:nat} (o:@T i) {A:Type} (x:Vector.t A i) : A :=
  match o with
    | T1 H => f x
  end.

If we try to prove something like:

Lemma bad: forall (x:nat) {H:1=1},
               evalT (T1 (H:=H)) [x] = x.
Proof.
  intros.
  unfold evalT.
  ...

we will end up with:

1 subgoals, subgoal 1 (ID 193)
  
  x : nat
  H : 1 = 1
  ============================
   f
     (eq_rect 1 (fun H0 : nat => t nat H0) [x] 1
        (evalT_obligation_1 1 T1 nat [x] H eq_refl)) = x

but what we are actually proving here is that: "f [x] = x" under
the assumption that length of [x] is 1. Which could be said as
the type of [x] is (vector nat i) and {i=1}. Something like:

  x : nat
  H : i = 1
  v : vector nat i
  A : v = [x]
  ============================
   f v = x

I am looking for a generic way dealing with such cases. Perhaps I should 
define 'eval' differently, or maybe I can resort to some tactics which will 
fold these coercions into
form shown above?

Thanks!

Sincerely,
Vadim Zaliva