Коиндукция и зависимые типы

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 неохотно раскрывает коиндуктивный 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) приводит к очень большому сроку, как я уже говорил выше.

Кто-нибудь может дать мне несколько советов по этому поводу?

Answer 1

Проблема в том, что 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 не держит происходит в s перед nй позиции. Несмотря на этот недостаток, эта функция может быть более удобной в использовании, потому что вам не нужно передавать проверочный объект ей.

Наконец, вы также можете доказать лемму о take_while показать, как она сокращается, и применять эту лемму каждый раз, когда вы хотите упростить выражение, включающее эту функцию. Таким образом, упрощение становится неуклюжим, поскольку вам нужно сделать это явно, но, по крайней мере, вы сможете доказать take_while,

Answer 2

В качестве дополнения к ответу Амори, вот теоремы, которые вам нужны для вычисления вашей функции.

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.