Coq proving nonsensical inductive property implication?

Question

In IndProp.v from Logical Foundations we have the following inductive property:

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)).

Is it possible to solve this:

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

Presumably one would need some sort of discriminate or contradiction since nostutter [] -> nostutter [x] seems like it makes no sense, but I don't see anything that would allow me to make progress. Is it just not possible to prove?

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2021-03-22T21:26:26

I think there is some confusion about the meaning of the implication. nostutter [] -> nostutter [x] is a perfectly reasonable hypothesis -- indeed, it is a theorem:

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.

An implication A -> B says that we can prove B by proving that A is true. If we can prove B without additional hypotheses, as it is the case for nostutter [x], then the implication holds trivially.

Coq proving nonsensical inductive property implication?

1 Answers