Coinduction和從屬類型

Question

我試圖編寫一個Coq函數，它需要一個Stream和一個謂詞並返回，作爲list，該屬性擁有的流的最長前綴。這是我有：

Require Import List Streams. 
Require Import Lt. 

Import ListNotations. 
Local Open Scope list_scope. 

Section TakeWhile. 

Context {A : Type} {P : Stream A -> Prop}. 
Hypothesis decide_P : forall s : Stream A, {P s} + {~ P s}. 

Program Fixpoint take_while (s : Stream A) 
    (H : Exists (fun s => ~ P s) s) : list A := 
    if decide_P s 
    then hd s :: take_while (tl s) _ 
    else []. 

Next Obligation. 
    destruct H; tauto. 
Defined. 

End TakeWhile. 

但是，當我試圖使用該功能進行計算，我得到一個非常大的項與所有的定義擴大。我不知道爲什麼，但我猜測Coq不願意展開共同誘惑的說法。這裏有一個例子：

Require Import Program.Equality. 
Require Import Compare_dec. 

Lemma not_lt_le : 
    forall n m : nat, ~ n < m -> m <= n. 
Proof. 
    pose le_or_lt. 
    firstorder. 
Qed. 

Definition increasing (s : Stream nat) : Prop := 
    forall n : nat, Exists (fun s => ~ hd s < n) s. 

CoFixpoint nats (n : nat) := Cons n (nats (S n)). 

Theorem increasing_nats : 
    forall n : nat, increasing (nats n). 
Proof. 
    intros n m. 
    induction m. 
    - left. 
    pose lt_n_0. 
    firstorder. 
    - dependent induction IHm. 
    * apply not_lt_le, le_lt_or_eq in H. 
     destruct H. 
     + left. 
     pose le_not_lt. 
     firstorder. 
     + right. 
     left. 
     simpl in *. 
     rewrite H. 
     pose lt_irrefl. 
     firstorder. 
    * right. 
     simpl. 
     apply IHIHm. 
     reflexivity. 
Qed. 

鑑於此，命令Eval compute in take_while (fun s => lt_dec (hd s) 5) (nats 0) (increasing_nats 0 5)導致非常大的名詞，正如我上面提到。

任何人都可以給我一些指導嗎？

Answer 1

問題是take_while是在H上遞歸定義的。由於證明通常在Coq中不明確定義（因爲定理爲increasing_nats），因此take_while將無法​​減少期限並且會卡住，產生您看到的巨大期限。即使你結束了increasing_nats與Defined而不是Qed的證明，強制它的定義是透明的，該證明使用了也被不明確定義的其他引理，從而使評估也陷入困境。

一個解決方案是證明increasing_nats沒有使用任何額外的引理，並結束與Defined的證明。這種方法並沒有擴展到更有趣的情況，因爲您可能需要使用Defined來譴責很多定理。

另一種解決方案是通過take_while一個明確的綁定參數：

Section TakeWhile. 

Variable A : Type. 
Variable P : A -> Prop. 
Variable decide_P : forall a, {P a} + {~ P a}. 

Fixpoint take_while_bound n (s : Stream A) : list A := 
    match n with 
    | 0 => [] 
    | S n => 
     if decide_P (hd s) then 
     hd s :: take_while_bound n (tl s) 
     else 
     [] 
    end. 

End TakeWhile. 

如果要使用此功能來顯示所提取的前綴是最大的，那麼你就必須證明一些元素，其P在之前的位置不存在s。儘管存在這個缺點，這個函數可能會更方便使用，因爲您不必將證明對象傳遞給它。

最後，您還可以證明一個關於take_while的引理，說明它如何減少，並且在每次想要簡化涉及該函數的表達式時應用該引理。因此，簡化變得笨拙，因爲你需要明確地做到這一點，但至少你可以證明take_while的事情。

Answer 2

作爲Amori答案的附錄，下面是計算函數所需的定理。

Definition le_IsSucc (n1 n2 : nat) (H1 : S n1 <= n2) : IsSucc n2 := 
    match H1 with 
    | le_n  => I 
    | le_S _ _ => I 
    end. 

Definition le_Sn_0 (n1 : nat) (H1 : S n1 <= 0) : False := 
    le_IsSucc _ _ H1. 

Fixpoint le_0_n (n1 : nat) : 0 <= n1 := 
    match n1 with 
    | 0 => le_n _ 
    | S _ => le_S _ _ (le_0_n _) 
    end. 

Fixpoint le_n_S (n1 n2 : nat) (H1 : n1 <= n2) : S n1 <= S n2 := 
    match H1 with 
    | le_n  => le_n _ 
    | le_S _ H2 => le_S _ _ (le_n_S _ _ H2) 
    end. 

Fixpoint le_or_lt (n1 n2 : nat) : n1 <= n2 \/ S n2 <= n1 := 
    match n1 with 
    | 0 => or_introl (le_0_n _) 
    | S _ => 
    match n2 with 
    | 0 => or_intror (le_n_S _ _ (le_0_n _)) 
    | S _ => 
     match le_or_lt _ _ with 
     | or_introl H1 => or_introl (le_n_S _ _ H1) 
     | or_intror H1 => or_intror (le_n_S _ _ H1) 
     end 
    end 
    end. 

Definition not_lt_le (n1 n2 : nat) (H1 : S n1 <= n2 -> False) : n2 <= n1 := 
    match le_or_lt n2 n1 with 
    | or_introl H2 => H2 
    | or_intror H2 => 
    match H1 H2 with 
    end 
    end. 

Definition le_pred' (n1 n2 : nat) : pred n1 <= pred n2 -> pred n1 <= pred (S n2) := 
    match n2 with 
    | 0 => fun H1 => H1 
    | S _ => le_S _ _ 
    end. 

Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 := 
    match H1 with 
    | le_n  => le_n _ 
    | le_S _ H2 => le_pred' _ _ (le_pred _ _ H2) 
    end. 

Definition le_S_n (n1 n2 : nat) (H1 : S n1 <= S n2) : n1 <= n2 := 
    le_pred _ _ H1. 

Fixpoint le_Sn_n (n1 : nat) : S n1 <= n1 -> False := 
    match n1 with 
    | 0 => fun H1 => le_Sn_0 _ H1 
    | S _ => fun H1 => le_Sn_n _ (le_S_n _ _ H1) 
    end. 

Definition le_Sn_le (n1 n2 : nat) (H1 : S n1 <= n2) : n1 <= n2 := 
    le_S_n _ _ (le_S _ _ H1). 

Fixpoint le_not_lt (n1 n2 : nat) (H1 : n1 <= n2) : S n2 <= n1 -> False := 
    match H1 with 
    | le_n  => le_Sn_n _ 
    | le_S _ H2 => fun H3 => le_not_lt _ _ H2 (le_S_n _ _ (le_S _ _ H3)) 
    end. 

Definition le_lt_or_eq (n1 n2 : nat) (H1 : n1 <= n2) : S n1 <= n2 \/ n1 = n2 := 
    match H1 with 
    | le_n  => or_intror eq_refl 
    | le_S _ H2 => or_introl (le_n_S _ _ H2) 
    end. 

Theorem increasing_nats : forall n : nat, increasing (nats n). 
Proof. 
unfold increasing. 
unfold not. 
unfold lt. 
intros n m. 
induction m. 
    apply Here. 
    apply (le_Sn_0 (hd (nats n))). 

    dependent induction IHm. 
    apply not_lt_le in H. 
    apply le_lt_or_eq in H. 
    destruct H. 
     apply Here. 
     apply (le_not_lt _ _ H). 

     apply Further. 
     apply Here. 
     rewrite H. 
     apply le_Sn_n. 
    apply (Further (nats n) (IHIHm _ eq_refl)). 
Defined.