coq - 如何在 Coq 中销毁列表（nil 或非 nil）

Question

我想在两种情况下破坏我的列表类型对象，例如：

H: lst = nil.
H: lst <> nil

Answer 1

自定义案例分析的一种可能模式是提供自定义案例分析引理，该模式如下所示：

From Coq Require Import List.
Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive list_spec A : list A -> Type :=
  | Nil_case : forall x, x = [] -> list_spec x
  | Cons_case : forall x, x <> [] -> list_spec x.

Lemma listP A (l : list A) : list_spec l.
Proof. now case l; constructor. Qed.

Lemma foo A (l : list A) : False.
Proof.
case (listP l); intros x Hx.

然后你会在你的上下文中得到正确的假设。使用destruct而不是case将清除l残留的虚假内容。

请注意，ssreflect的case策略包括对这种案例分析引理的特殊支持，您通常会这样做case: l / listP.

Answer 2

如果你使用destruct lst as [ | fst_elnt lst_tl] eqn:H你得到两个目标，在第一个目标中，你确实有你需要的假设。

H : lst = nil

在第二个目标中，您有一个形式的假设

H : lst = fst_elnt :: lst_tl

这不是你所期望的H，它实际上更强大。要获得H预期的语句，您可以键入以下内容：

rename H into H'.  (* to free the name H *)
assert (H : lst <> nil).
   rewrite H'; discriminate.

discriminate是表达数据类型的两个不同构造函数不能返回相等值这一事实的基本策略。