Coq 证明无意义的归纳 属性 蕴涵？

Question

在逻辑基础的 IndProp.v 中，我们有以下归纳法 属性：

Inductive nostutter {X:Type} : list X -> Prop :=
  | nos_nil : nostutter []
  | nos_one : forall x, nostutter [x]
  | nos_cons : forall x h l, nostutter (h :: l) -> (x <> h) -> (nostutter (x :: h :: l)).

是否可以解决这个问题：

1 subgoal
X : Type
x : X
H : nostutter [] -> nostutter [x]
______________________________________(1/1)
False

大概需要某种歧视或矛盾，因为 nostutter [] -> nostutter [x] 似乎没有任何意义，但我看不到任何能让我取得进步的东西。只是无法证明吗？

Answer 1

我认为对蕴涵的含义有些混淆。 nostutter [] -> nostutter [x] 是一个完全合理的假设——事实上，它是一个 定理:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive nostutter {X:Type} : list X -> Prop :=
  | nos_nil : nostutter []
  | nos_one : forall x, nostutter [x]
  | nos_cons : forall x h l, nostutter (h :: l) -> (x <> h) -> (nostutter (x :: h :: l)).

Lemma not_goal {X} (x : X) : @nostutter X [] -> nostutter [x].
Proof. intros _; apply nos_one. Qed.

一个蕴涵A -> B说我们可以通过证明A为真来证明B。如果我们可以在没有额外假设的情况下证明 B，就像 nostutter [x] 的情况一样，那么这个推论就成立了。