我想在两种情况下破坏我的列表类型对象,例如:
H: lst = nil.
H: lst <> nil
自定义案例分析的一种可能模式是提供自定义案例分析引理,该模式如下所示:
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.
如果你使用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
是表达数据类型的两个不同构造函数不能返回相等值这一事实的基本策略。