I am stucked by a proof using coq. I have the following definitions:

我被一个使用Coq的证据难住了。我有以下定义：

Require Import List.
Require Import Nat.

Fixpoint Inb(x: nat) (A: list nat) :=
 match A with
 | nil => false
 | h :: t => if h =? x then true else (Inb x t)
 end.

Definition In (x: nat) (A: list nat) := 
  Inb x A = true.

Then I want to proof the theorem:

然后我想证明这个定理：

Theorem inside_thm: forall x, In x (3::4::nil) -> x = 3 \/ x = 4.

However, I got stucked and no idea of how can I proof it.

然而，我被卡住了，不知道如何证明它。

Could you please give me a guide and write an example to solve it?

你能给我一个指导并写一个解题的例子吗？

For instance, you may start with a few helpful lemmas about In.

例如，你可以从一些关于in的有用的词条开始。

Lemma In1 x y l : In x (y::l) <-> y = x \/ In x l. 
  Proof.    
   unfold In;  simpl; rewrite <- PeanoNat.Nat.eqb_eq. 
    case (y =? x).  
     - split;  auto. 
     - split.
       + auto. 
       + destruct 1; [discriminate | auto]. 
Qed.

Lemma In2 x : ~ In x nil. 
Proof. 
 discriminate. 
Qed. 

Then your lemma can be easily proved.

那么你的引理就可以很容易地证明了。

Theorem inside_thm: forall x, In x (3::4::nil) -> x = 3 \/ x = 4.
Proof.
  intros x H; rewrite In1 in H. 
  (* ... *)

Another, very specific, approach to proving this particular theorem could be to:

证明这一特定定理的另一种非常具体的方法可能是：

1. first, assume that x = 3 and then show, in that case, that the statement is trivially true, after rewriting everywhere x by 3;


2. now, under the hypothesis that x is not equalt to 3, do the same, assuming now that x = 4;


3. finally, show that, if x is neither 3 nor 4, the statement remains valid, since, by expanding the definitions of In and Inb, you can show that all the tests in the Coq-generated if statement are false (Coq is able to unroll all the calls to Inb, since the list argument is a constant in your case), yielding false = true as an hypothesis in the goal, which makes it trivially true.

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.

您必须考虑自然数和布尔值在Coq中是如何工作的。布尔条件式的全部困难在于，您必须建设性地确定条件是否成立，以便确定表达式的值。同样，自然数的归纳构造的一个特点是，您可以(建设性地)确定一个自然数是否为0、是否为1、是否为2、是否为3等，并且您必须使用这样的推理链才能将x(3：：4：：nil)中的布尔表达式展开为类似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

综上所述，您的证明可以非常简单地通过重复测试x是否为0、1、2、3……直到校样完成。这样做的一个方便的习惯用法是

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:

相比之下，如果您使用的是用命题表达式定义的内置List.in，那么对应的定理就足够简单了，Coq自己就能搞清楚：

Theorem inside_thm2 : forall x, List.In x (3::4::nil) -> x = 3 \/ x = 4.
Proof. firstorder. Qed.