如何使勒柯克評估特定歸約（或 - ？它爲什麼在這種情況下拒絕）

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這是很容易的）。但是爲了完成這個引理，我需要證明可訪問性證明的平等性，這可能需要證明不相關。我不確定，對不起。