You have to think about how natural numbers and booleans work in Coq. The whole difficulty with boolean conditionals is that you have to establish constructively whether or not the conditional holds in order to determine the value of the expression. Likewise, a hallmark of the inductive construction of natural numbers is that you can determine (constructively) whether or not a natural number is 0, whether it is 1, whether it is 2, whether it is 3, etc., and you have to use such a chain of reasoning in order to unwind the boolean expression In x (3::4::nil)
into an outcome like x = 3 ∨ x = 4
.
With all that said, your proof can be done very simply by repeatedly testing whether x
is 0, 1, 2, 3, ... until the proof finishes. One convenient idiom for doing so is
Theorem inside_thm: forall x, In x (3::4::nil) -> x = 3 \/ x = 4.
Proof. intros; repeat (destruct x; try intuition discriminate). Qed.
By contrast, if you're using the built-in List.In
which is defined with propositional expressions, then the corresponding theorem is trivial enough for Coq to figure out by itself:
Theorem inside_thm2 : forall x, List.In x (3::4::nil) -> x = 3 \/ x = 4.
Proof. firstorder. Qed.