The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

I would still insist on not using equality proofs.

Inductive Vop_i {A:Type} (i:nat) : nat -> Type :=
| Vid: Vop_i i i
| Vduplicate: Vop_i i (i + i)
.

Inductive Vop_o {A:Type} (o:nat) : nat -> Type :=
| Vhalf : Vop_o o (o + o)
| Vconst : Vop_o o 1
.

Inductive Vop {A : Type} {i o : nat} :=
| VI : @Vop_i A i o -> Vop
| VO : @Vop_o A o i -> Vop
| Vcompose : forall t, @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.

Definition eval_i {A:Type} {i o:nat} (t:@Vop_i A i o) (x:Vector.t A i): 
Vector.t A o :=
match t with
   | Vid => x
   | Vduplicate => Vector.append x x
end.

Definition eval_o {A:Type} {i o:nat} (t:@Vop_o A o i) (x:Vector.t A i): 
Vector.t A o :=
(match t in @Vop_o _ _ i return Vector.t A i -> Vector.t A o 
   with
     | Vhalf => fun y => take (m:=o) o y
     | Vconst => fun y => Vector.const (hd (n:=0) y) o
   end) x.

Fixpoint eval {A:Type} {i o:nat} (t:@Vop A i o) (x:Vector.t A i): Vector.t A 
o :=
match t with
   | VI vi => eval_i vi x
   | VO vo => eval_o vo x
   | Vcompose _ vop1 vop2 => ((eval vop1) ∘ (eval vop2)) x
end.

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

Lemma test2:
  forall A n (v:Vector.t A (n + n)) ,
    eval (Vcompose _ (VO (Vhalf _)) (VI (Vid _))) v = eval (VO (Vhalf _)) v.
Proof.
  trivial. 
Qed.


> On 08 Jan 2015, at 03:20, Vadim Zaliva 
> <vzaliva AT cmu.edu>
>  wrote:
> 
> 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
>