如何使Coq评估特定的重新索引(或 - 为什么在这种情况下拒绝？)

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从列表中删除以下项,并在剩余列表上进行递归.即

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

@Vinz 解释了 Coq 不使用 减少 beta-redex 的原因fix。以下也是CDPT的相关摘录：

一项候选规则会说我们尽可能应用递归定义。然而，这显然会导致非终止的归约序列，因为该函数可能看起来完全应用在其自己的定义内，并且我们会天真地立即“简化”此类应用程序。相反，当递归参数的顶层结构已知时，Coq 仅对递归函数应用 beta 规则。

我只是想补充一点，可以在不假设额外公理的情况下证明引理 - 简单的概括就足够了。

让我们首先为列表定义一个新的归纳原则：

Definition lt_list {A} (xs ys : list A) := length xs < length ys.

Definition lt_list_wf {A : Type} : well_founded (@lt_list A) :=
  well_founded_ltof (list A) (@length A).

Lemma lt_list_wf_ind {A} (P : list A -> Prop) :
  (forall ys, (forall xs, length xs < length ys -> P xs) -> P ys) ->
  forall l, P l.
Proof. intros ? l; elim (lt_list_wf l); auto with arith. Qed.

本质上，lt_list_wf_ind归纳原理说，如果我们可以证明一个谓词在适用于所有较小长度列表的假设下P适用于一个列表，那么我们就对所有列表都成立。ysPP

现在，让我们证明一个引理，它表示 的可访问性参数的证明无关性picksome：

Lemma picksome_helper l : forall acc acc',
  picksome l acc = picksome l acc'.
Proof.
  induction l as [l IH] using lt_list_wf_ind; intros acc acc'.
  destruct l; destruct acc, acc'; [trivial |].
  simpl. f_equal.
  apply IH.
  simpl; rewrite Nat.lt_succ_r.
  apply drop_lemma_le.
Qed.

使用这个本地版本的无关性证明，Acc我们现在可以证明pick_zero引理：

Lemma pick_zero k : pick (0::k) = 0::pick k.
Proof.
  unfold pick.
  destruct (lt_wf (length (0 :: k))).
  simpl (picksome (0 :: k) _).
  f_equal.
  apply picksome_helper.
Qed.