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.