Coq：将信息保留在匹配声明中 [英] Coq: keeping information in a match statement

问题描述

我正在构建一个递归函数，该函数对列表 l 进行匹配。在 cons 分支中，我需要使用 l = cons a l'的信息来证明递归功能终止。但是，当我使用 match l 时，信息就会丢失。

I'm building a recursive function that does a match on a list l. In the cons branch I need to use the information that l = cons a l' in order to prove that the recursive function terminates. However, when I use match l the information gets lost.

如何使用匹配以保留信息？

这里是函数（ drop 和 drop_lemma_le 在末尾给出，以提高可读性）：

Here is the function (drop and drop_lemma_le are given at the end, for readability):

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是如何处理该问题的，但是它也很长而且无法使用嵌套函数等读取。

I am actually able to define the whole function via refine like below, but it is not really readable. Doing Print picksome. reveals how Coq has handled the problem, but it is also quite long and unreadable with nested functions, etc.

必须有一种更具可读性的书写方式，对吧？

There must be a more readable way to write it, right?

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.

我的第一次尝试是尝试类似的事情

My first attempt was to try something like this

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抱怨：

I'm unable to get out the actual a and l' that l is made from. Coq complains:

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

这样做的正确（可读）方式是什么？

What would be the proper (readable) way to do this?

以下是 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.

推荐答案

记住模式匹配的列表看起来，您只需要像这样简单地更改匹配的返回类型。

To remember what the list you are pattern-matching on looks like, you need to simply change the return type of your match like so.

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

此匹配l为m return m = m->列表nat 的意思是，您正在 l 上执行模式匹配，因此将匹配形式称为 m ，并给出 l 等于 m 的证明，您将构建一个列表

What this match l as m return l = m -> list nat is saying is that you are performing a pattern matching on l, that you'll call the matching form m and that, given a proof that l equals m, you'll build a list of nats.

现在， match 块的类型会略有不同：不仅仅是提供 list nat ，它将提供类型为 l = l->的函数。列出nat 。对我们来说幸运的是， eq_refl l 证明了 l 等于自己，因此我们可以将匹配应用于回到我们最初的清单nat 。

Now, the type of the match block will be slightly different: instead of just delivering a list nat, it will deliver a function of type l = l -> list nat. Luckily for us, eq_refl l delivers a proof that l is equal to itself so we can apply the match to that and get back our initial list nat.

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

Looking at the branches of the match, we can see that:

• 在 nil 的情况下，您可以忽略多余的假设

• In the nil case, you can ignore the extra Hypothesis which you don't need.

在缺点的情况下，它恰好为您提供了急需的假设，并且您可以这样履行您的证明义务：

In the cons case, it provides you precisely the much needed hypothesis and you can discharge your proof obligation like so:

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

已定义。

这篇关于Coq：将信息保留在匹配声明中的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！