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

Question

我正在构建一个递归函数，在列表

match

上执行

l

。在

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

的证明，您将建立一个 nat 列表。

现在，

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.
  

  已定义。

Answer 2

这是实现您想要的效果的低功率方法。加莱提供的解决方案很有启发性，但稍后尝试破坏如此复杂的匹配可能会产生类型错误。这个问题可以通过 ssreflect 解决，也许还有其他方法，但也许您只是想要最直接的解决方案。

Definition is_cons : forall ls : list nat,
   {x | ls = cons (fst x) (snd x)} + { ls = nil }.
Proof. destruct ls eqn:K. now right. now left; exists (n,l). Qed.

Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat.
  refine (if is_cons l then _ else nil).     
  destruct s as [(a, l') K].
  refine (cons a (picksome (drop a l') _)).
  apply H.
  assert (l = cons a l') by auto.  (* There you go! :) *)