Coq：將信息保存在匹配語句中

Question

我正在構建一個遞歸函數，它在列表l上執行match。在cons分支中，我需要使用l = cons a l'爲了證明遞歸函數終止的信息。但是，當我使用match l時，信息會丟失。

如何使用match來保存信息？

下面是函數（drop和drop_lemma_le在最後給出，爲便於閱讀）：

Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat. 
    refine (
     match l with 
      nil => nil 
      | cons a l' => cons a (picksome (drop a l') _) 
     end 
    ). 

    apply H. 
    assert (l = cons a l') by admit. (* here is where I need the information *) 
    rewrite H0. 
    simpl. 
    apply le_lt_n_Sm. 
    apply drop_lemma_le. 
Defined. (* Can't end definition here because of the 'admit'. *) 

我其實能夠通過refine定義功能全像下面，但它是不是真的讀。做Print picksome.揭示Coq如何處理這個問題，但它也是相當長，並且嵌套函數等無法閱讀。

必須有一個更可讀的方式來寫它，對吧？

Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat. 
Proof. 
    refine (_). 
    remember l as L. 
    destruct l as [| a l']. 
    apply nil. 
    apply (cons a). 
    apply (picksome (drop a l')). 
    apply H. 
    rewrite HeqL. 
    simpl. 
    apply le_lt_n_Sm. 
    apply drop_lemma_le. 
Defined. 

我第一次嘗試是試圖像這樣

Definition list_cons_dec {T} (l:list T) : 
    {exists a l', l=a::l'} + {~ exists a l', l=a::l'}. 
    remember l as L. 
    destruct l as [| a l']. 
    - right; subst L; intros [a [A B]]; inversion B. 
    - left; exists a, l'; apply HeqL. 
Defined. 

Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat. 
Proof. 
    refine (
     match list_cons_dec l with 
     | right Hdec => nil 
     | left Hdec => cons _ (picksome (drop _ _) _) 
     end 
    ). 
    destruct l. 
    inversion Hdec. (* fails *) 

我無法擺脫實際a和l'是l被製成。 Coq抱怨：

Error: Inversion would require case analysis on sort Set which is not allowed 
for inductive definition ex. 

什麼是適當的（可讀）的方式來做到這一點？

---

下面是drop和drop_lemma_le的定義。

Fixpoint drop {T} n (l:list T) := 
    match n with 
    | O => l 
    | S n' => match l with 
       | nil => nil 
       | cons _ l' => drop n' l' 
       end 
    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. 

Answer 1

要記住你在模式匹配上的列表是什麼樣的，你需要簡單地改變匹配的返回類型，就像這樣。

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

這是什麼match l as m return l = m -> list nat的意思是，你正在執行上l匹配的模式，你會調用對應的形式m，而且鑑於一個證明l等於m，將構建列表NATS。

現在，match塊的類型會略有不同：它不是隻提供list nat，而是提供l = l -> list nat類型的功能。幸運的是，eq_refl l提供了一個證明，l等於自己，所以我們可以將該匹配應用於此，並取回我們的初始list nat。

縱觀本場比賽的分支，我們可以看到：

• 在nil情況下，可以忽略額外的假設，你不需要。

• 在cons情況下，爲您提供精確急需的假設，你可以排出像這樣的證明義務：

  apply H. 
  rewrite Hyp. 
  simpl. 
  apply le_lt_n_Sm. 
  apply drop_lemma_le. 
  

  定義。