2

と述語を取り、プロパティが保持するストリームの最長プレフィックスをStreamとして返すCoq 関数を作成しようとしています。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

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 に答える