The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-01-08 3:20 GMT+01:00 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
.

I would either use a "Inductive Vop (A : Type) (i o : nat) : Type := …" (with equalities every where), either a "Inductive Vop (A : Type) : nat -> nat -> Type :=…" (with no equalities).
Both have advantages and inconvenients. I often find the second way more elegant, but also trickier to use. The first is heavier, but "you can't go wrong" using it.

The thing is that in the second way, when you destruct a "x:Vop A (a+b) (c+d)" to build a "Vop A a c" for instance, you can obtain a "y:Vop A e f" where "e" and "f" are new binders with their relation to "a" and "b" lost.
This is the way how "indices" work: destruction of "x" will replace all occurences of (a+b) and (c+d) everywhere, but if you have some occurence of "a" but not "a+b", you will lose information.
To deal with it, you often have to do tricks such as trying to change "Vop A a c" with "Vop A ((a+b)-b) ((c+d)-d)" so that you will end with proving "Vop A (e-b) (f-d)" from "y:Vop A e d".
To deal with these kind of problems, you can use "inversion x." instead of "destruct x." which will produce equalities for you, and I think there is something like "dependant induction" when you want to do some induction.

With the first way, as you have parameters and not indices, there is no replacement of occurences, and no need to keep a link between new variables and old ones (as there is only one variable which is kept).
The price to pay for this simplicity is that you need to carry equalities everywhere.

I will try to follow your developement with the first way.

Inductive Vop (A:Type) : nat -> nat -> Type :=
| Vid: forall i, Vop A i i
| Vduplicate: forall i, Vop A i (i + i)
| Vhalf : forall o, Vop A (o+o) o
| Vconst : forall o, Vop A 1 o
| Vcompose : forall i 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.

Definition eval (A : Type) : forall i o, Vop A i o -> Vector.t A i -> Vector.t A o :=
  fix eval i o (vop : Vop A i o) : Vector.t A i -> Vector.t A o :=
  match vop in Vop _ x y return Vector.t _ x -> Vector.t _ y with
  | Vid u => fun v => v
  | Vhalf o => take (m:=o) o
  | Vduplicate i => fun v => Vector.append v v
  | Vconst o => fun v => Vector.const (hd (n:=0) v) o
  | Vcompose i t o vo iv => ((eval t o vo) ∘ (eval i t iv))
  end.

(Program is not involved anymore. I also use Definition and not fixpoint to work in a closure containing A. This is because I do not like to pass the same argument to all recursive calls. Others prefer to use a Section, and others also do not really care on passing the same argument on recursive calls. I do not consider any of these practices as wrong, so do as you prefer.)
 

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

I do not know if it is much relevant, but maybe you could consider using these two functions:

Definition castl {x y : nat} {A : Type} (H : x = y) : Vector.t A y -> Vector.t A x :=
  match H in _=t return Vector.t A t -> Vector.t A x with eq_refl => fun x => x end.

Definition castr {x y : nat} {A : Type} (H : x = y) : Vector.t A y -> Vector.t A x :=
  match H in _=t return Vector.t A x -> Vector.t A t with eq_refl => fun x => x end.

These functions are specializations of eq_rect to Vector.t.

That means that you would end up with

  x : nat
  H : 1 = 1
  ============================
   f (castl/r (evalT_obligation_1 1 T1 nat [x] H eq_refl) [x]) = x

This would slightly increase readablity.

Note that dealing "computational" terms dealing with equalities is often very tricky. You often have to generalize the right arguments.
From there, I would need to test some ideas with Coq to test if it works or not (too tricky for me to solve it without the interpreter).