recursion - 如何让 Coq 评估特定的 redex(或者 - 在这种情况下它为什么拒绝？)

Question

当我试图证明一个关于递归函数的定理时(见下文)，我最终得到了一个可约表达式

(fix picksome L H := match A with .... end) L1 H1 = RHS

我想扩展 match表达，但 Coq 拒绝了。做 simpl只是将右手边扩展成无法阅读的困惑。为什么 Coq 不能用 simpl; reflexivity 完成证明，以及应该如何指示 Coq 精确展开 redex，并完成证明？

该函数是一个递归函数 pick这需要一个 list nat并取第一个 nat叫 a , 丢弃以下 a列表中的项目，并在剩余的列表上递归。 IE。

pick [2;3;4;0;1;3])=[2; 0; 1]

我试图证明的定理是，该函数在只包含零的列表上“什么都不做”。这是导致问题的发展:

Require Import Arith.
Require Import List.
Import ListNotations.

Fixpoint drop {T} n (l:list T) :=
  match n,l with
    | S n', cons _ l' => drop n' l'
    | O, _ => l
    | _, _ => nil
  end.

第一个引理:

Lemma drop_lemma_le : forall {T} n (l:list T), length (drop n l) <= (length l).
Proof.
  intros; generalize n; induction l; intros; destruct n0; try reflexivity;
  apply le_S; apply IHl.
Defined.

第二个引理:

Lemma picksome_term: forall l l' (a :nat),
       l = a::l' -> Acc lt (length l) ->  Acc lt (length (drop a l')).
Proof.
  intros; apply H0; rewrite H; simpl; apply le_lt_n_Sm; apply drop_lemma_le.
Defined.

还有几个定义:

Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat :=
  match l as m return l=m -> _ with
    | nil       => fun _  => nil
    | cons a l' => fun Hl =>
                     cons a (picksome (drop a l')
                                      (picksome_term _ _ _ Hl H))
  end
    (eq_refl _).

Definition pick (l:list nat) : list nat := picksome l (lt_wf (length l)).

Inductive zerolist : list nat -> Prop :=
| znil : zerolist nil
| hzlist : forall l, zerolist l -> zerolist (O::l).

现在，我们可以证明我们的定理，如果我们有引理 H :

Theorem pickzero': (forall k, pick (0::k) = 0::pick k) ->
                forall l, zerolist l -> pick l = l.
Proof.
  intros H l H0; induction H0; [ | rewrite H; rewrite IHzerolist]; reflexivity.
Qed.

(* but trying to prove the lemma *)
Lemma pickzero_lemma : forall k, pick (0::k) = 0::pick k.
  induction k; try reflexivity.
  unfold pick at 1.
  unfold picksome.

这是目标和背景:

a : nat
k : list nat
IHk : pick (0 :: k) = 0 :: pick k
============================
 (fix picksome (l : list nat) (H : Acc lt (length l)) {struct H} :
    list nat :=
    match l as m return (l = m -> list nat) with
    | [] => fun _ : l = [] => []
    | a0 :: l' =>
        fun Hl : l = a0 :: l' =>
        a0 :: picksome (drop a0 l') (picksome_term l l' a0 Hl H)
    end eq_refl) (0 :: a :: k) (lt_wf (length (0 :: a :: k))) =
 0 :: pick (a :: k)

Answer 1

Coq 关于定点的归约规则非常简单:当且仅当定点应用于“构造”项时，您才能展开定点的一个步骤。例如 length (1 :: nil)会减少，但在上下文中是 l = 1 :: nil , length l不会减少。您必须明确替换 l按构造项1 :: nil以减少追加。

在您的目标中，picksome由 H 上的结构递归定义，可访问性证明。如果您尝试 simpl ，减少实际上发生，并在此参数不再“构造”时停止。在您的特定情况下，在 simpl 之后你最终会得到一个 (fix picksome ...) (drop a1 l'0) (nat_ind <big term>)证明，并且 Coq 不能减少 picksome了。

编辑:为了完成你的证明，我首先尝试证明:

Lemma picksome_unfold : 
  forall (hd:nat) (tl:list nat) (H:Acc lt (length (hd::tl))), picksome (hd::tl) H = 
    cons hd (picksome (drop hd tl) (picksome_term (hd::tl) tl hd (eq_refl (hd::tl)) H)).

(如果您破坏 H ，这很容易)。然而要完成 pickzero_lemma引理，我需要证明可访问性证明的相等性，这可能需要证明无关紧要。我不确定，抱歉。