Coq "convoy model"
I am trying to use a "convoy pattern" to keep the dependency between three variables (two parameters and a return value):
Require Import Vector.
(* "sparse" vector type *)
Notation svector A n := (Vector.t (option A) n).
Fixpoint svector_is_dense {A} {n} (v:svector A n) : Prop :=
match v with
| Vector.nil => True
| Vector.cons (None) _ _ => False
| Vector.cons (Some _) _ xs => svector_is_dense xs
end.
Lemma svector_tl_dense {A} {n} {v: svector A (S n)}:
svector_is_dense v -> svector_is_dense (Vector.tl v).
Admitted.
Lemma svector_hd {A} {n} (v:svector A (S n)): svector_is_dense v -> A.
Admitted.
Fixpoint vector_from_svector {A} {n} {v:svector A n} (D:svector_is_dense v): Vector.t A n :=
match n return (svector A n) -> (svector_is_dense v) -> (Vector.t A n) with
| O => fun _ _ => @Vector.nil A
| (S p) => fun v0 D0 => Vector.cons
(svector_hd v0 D0)
(vector_from_svector (Vector.tl v) (svector_tl_dense D))
end v D.
The problem arises in the last definition. Any suggestions why it doesn't work?
source to share
You're almost right. The problem lies in your proposal return
, which is independent of it. You need
match n return forall (w: svector A n), (svector_is_dense w) -> (Vector.t A n) with
so it D0
doesn't have a type svector_is_dense v
as it would in your case, but svector_is_dense v0
.
By the way, in the second constructor, I think you meant Vector.tl v0
and svector_tl_dense D0
. Here is the complete term I wrote (ignore the extra _
in cons
, I have no implications activated):
Fixpoint vector_from_svector {A} {n} {v:svector A n} (D:svector_is_dense v): Vector.t A n :=
match n return forall (w:svector A n), (svector_is_dense w) -> (Vector.t A n) with
| O => fun _ _ => @Vector.nil A
| (S p) => fun v0 D0 => Vector.cons _
(svector_hd v0 D0) _
(vector_from_svector (svector_tl_dense D0))
end v D.
source to share