Coq 证明了无意义的归纳属性含义？

Question

在 Logical Foundations 的 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] 的情况一样，那么这个含义就很简单了。