Coq：目标变量出现在箭头左侧时未通过归纳转换

Question

我试图通过对 l 的归纳来证明以下定理。这是一个简单的定理，但是当我尝试在 Coq 中证明它时，我没有达到我期望的归纳目标。

Theorem nodup_app__disjoint: forall {X: Type} (l: list X),
  (forall l1 l2 : list X, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l.
Proof.
  intros X l. induction l.
  - intros F. apply nodup_nil.
  - (* ??? *)

此时的状态：

1 subgoal
X : Type
x : X
l : list X
IHl : (forall l1 l2 : list X, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l
______________________________________(1/1)
(forall l1 l2 : list X, x :: l = l1 ++ l2 -> Disjoint l1 l2) ->
NoDup (x :: l)

但这根本不是我期望的目标！ x :: l = l1 ++ l2不应该换成l = l1 ++ l2吗？

以下是我正在处理的建议，如果您想重现问题并亲自查看：

Inductive Disjoint {X : Type}: list X -> list X -> Prop :=
  | disjoint_nil: Disjoint [] []
  | disjoint_left: forall x l1 l2, Disjoint l1 l2 -> ~(In x l2) -> Disjoint (x :: l1) l2
  | disjoint_right: forall x l1 l2, Disjoint l1 l2 -> ~(In x l1) -> Disjoint l1 (x :: l2).

Inductive NoDup {X: Type}: list X -> Prop :=
  | nodup_nil: NoDup []
  | nodup_cons: forall hd tl, NoDup tl -> ~(In hd tl) -> NoDup (hd :: tl).

Answer 1

But that is not at all the goal I would expect! Shouldn't x :: l = l1 ++ l2 be replaced by l = l1 ++ l2?

简答：不应该！

列表的归纳原理

让我们回顾一下列表的归纳原理：

Check list_ind.
(*
list_ind
  : forall (A : Type) (P : list A -> Prop),
    P [] ->
    (forall (a : A) (l : list A), P l -> P (a :: l)) ->
    forall l : list A, P l
*)

这意味着为了证明谓词P对所有列表（forall l : list A, P l）成立，需要证明

P 适用于空列表 -- P [];
P 适用于所有 non-empty 列表，因为它适用于它们的尾巴 -- (forall (a : A) (l : list A), P l -> P (a :: l)).

将列表归纳原则应用于目标

现在，我们有以下目标：

(forall l1 l2, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l.

为了了解在尝试通过对 l 的归纳来证明陈述时我们应该达到什么目标，让我们在一种情况下机械地用 [] 替换上面的 l 和 h :: tl其他.

[] 案例：

(forall l1 l2, [] = l1 ++ l2 -> Disjoint l1 l2) -> NoDup [].

h :: tl 案例：

(forall l1 l2, h :: tl = l1 ++ l2 -> Disjoint l1 l2) -> NoDup (h :: tl).

这就是您在上面得到的（对重命名取模）。对于第二种情况，您还得到了归纳假设，我们从原始语句中将 tl 替换为 l:

(forall l1 l2, tl = l1 ++ l2 -> Disjoint l1 l2) -> NoDup tl.

顺便说一句，该定理是可证明的，您可能会发现以下辅助引理很有用：

Lemma disjoint_cons_l {X} (h : X) l1 l2 :
  Disjoint (h :: l1) l2 -> Disjoint l1 l2.
Admitted.

Lemma disjoint_singleton {X} h (l : list X) :
  Disjoint [h] l -> ~ In h l.
Admitted.

Coq：目标变量出现在箭头左侧时未通过归纳转换

Coq: goal variable not transformed by induction when appearing on left side of arrow

coq

induction

列表的归纳原理

将列表归纳原则应用于目标