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