Coq：将信息保存在匹配语句中

我正在构建一个递归函数match在清单上l。在里面cons分支我需要使用以下信息l = cons a l'为了证明递归函数终止。但是，当我使用match l信息丢失。

我该如何使用match保留信息？

这是函数（drop and 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 and l' that l是由.奶牛抱怨：

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

执行此操作的正确（可读）方法是什么？

以下是以下的定义drop and 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.

要记住您正在进行模式匹配的列表是什么样子，您只需像这样更改匹配的返回类型即可。

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 equals m，您将构建一个 nat 列表。

现在，类型match块会略有不同：而不是仅仅提供一个list nat，它将提供类型的函数l = l -> list nat。对我们来说幸运的是，eq_refl l提供了一个证明l等于它自己，所以我们可以将匹配应用于它并取回我们的初始值list nat.

查看比赛的分支，我们可以看到：

• In the nil在这种情况下，您可以忽略不需要的额外假设。

• In the cons在这种情况下，它恰好为您提供了急需的假设，您可以像这样履行证明义务：

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

  Defined.