如何让Coq评估特定的Redex（或-为什么在这种情况下拒绝？）

larsr 发表于 Dev

拉尔

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

(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)

安东·特鲁诺夫（Anton Trunov）

@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.

本文收集自互联网，转载请注明来源。

如有侵权，请联系[email protected] 删除。