2

我正在尝试编写一个 Coq 函数，该函数接受 aStream和一个谓词，并以 a 的形式返回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 不愿意展开共归纳Stream论证。这是一个例子：

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)会导致一个非常大的术语，正如我上面提到的。

谁能给我一些指导？

4

2 回答 2

3

问题是在take_while上递归定义H。由于证明通常在 Coq 中定义不透明（就像您的increasing_nats定理一样），take_while因此无法减少increasing_nats 0 5术语并且会卡住，从而产生您看到的巨大术语。即使你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不存在的元素出现在第 th 位置s之前。n尽管有这个缺点，但这个函数使用起来会更方便，因为您不必将证明对象传递给它。

最后，您还可以证明一个引理来take_while说明它是如何减少的，​​并在每次要简化涉及该函数的表达式时应用该引理。因此，简化变得更加笨拙，因为您需要明确地进行，但至少您将能够证明关于take_while.

于 2013-07-17T23:22:29.307 回答
0

作为 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.
于 2013-07-18T14:24:41.780 回答