如何使勒柯克评估特定归约（或 - ？它为什么在这种情况下拒绝）

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

现在，我们可以证明我们的定理˚F我们有引理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是P适用于所有的假设下成立了一个列表ys列表的长度较短，那么我们有P所有列表。

现在，让我们证明了表达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. 

Answer 2

勒柯克的关于不动点减少规则很简单：你可以展开一个固定点，当且仅当的步骤固定点适用于“构造”术语。例如length (1 :: nil)会减少，但在上下文中分别为l = 1 :: nil,length l不会减少。您必须用构造的术语1 :: nil明确替换l，以便减少追加。

在你的目标中，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这是很容易的）。但是为了完成这个引理，我需要证明可访问性证明的平等性，这可能需要证明不相关。我不确定，对不起。