勒柯克「護航模式」

Question

我試圖用「護航模式」，保留3個變量（兩個參數和返回值）之間的依賴關係：在最後一個定義

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. 

，就會出現問題。任何建議，爲什麼它不工作？

Answer 1

你明白了吧。問題出在你的return子句中，它是不依賴的。你需要的是

match n return forall (w: svector A n), (svector_is_dense w) -> (Vector.t A n) with 

使D0是svector_is_dense v類型並不像它會在你的情況，但svector_is_dense v0。

順便說一下，在第二個構造函數中，我猜你的意思是Vector.tl v0和svector_tl_dense D0。這裏是足月我寫的（不cons介意其它附加_，我沒有implicits激活）：

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.