如何在 Coq 中破坏列表（nil 或 not 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 是表达数据类型的两个不同构造函数不能 return 相等值这一事实的基本策略。

如何在 Coq 中破坏列表（nil 或 not nil）

How do destruct list in Coq (nil or not nil)

coq

coqide

coq-tactic