如何在Coq中通过自然数案例分析来证明？

Question

我被使用 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.

那么我要证明定理：

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

但是，我被困住了，不知道如何证明它。

您能给我一个指南并写一个例子来解决它吗？

Answer 1

例如，您可以从一些关于

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) eqn: Hxy. 
     - split;  auto. 
     - split; [ auto | intro H; destruct H; try discriminate; auto].
Qed.

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

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

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