coq - 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说，我们可以B通过证明这A是真的来证明。如果我们可以在没有额外假设的情况下证明B，就像 的情况一样nostutter [x]，那么蕴含意义微不足道。