在Coq中证明函数索引的一些定理

Question

我正在尝试在 Coq 中实现一个索引函数。我写了这段代码：

Notation grid := (list nat).

Fixpoint index_aux (n : nat) (g : grid) (i : nat) : option nat :=
  match g with
  | [] => None
  | h :: t => if h =? n then Some i else index_aux n t (i + 1)
  end.

Definition index (n : nat) (g : grid) : option nat :=
  index_aux n g 0.

我尝试证明一些关于它的定理。首先，一些简单的引理：

Lemma index_nil : forall x, index x [] = None.
Proof. auto. Qed.

Lemma index_singleton : forall x, index x [x] = Some 0.
Proof.
  intros x. unfold index. simpl. destruct (x =? x) eqn:E.
  reflexivity. rewrite Nat.eqb_neq in E. contradiction.
Qed.

Lemma index_double : forall x, index x [x; x] = Some 0.
Proof.
  intros x. unfold index. simpl. destruct (x =? x) eqn:E.
  reflexivity. rewrite Nat.eqb_neq in E. contradiction.
Qed.

现在，我正在尝试证明一个更普遍的定理：

Theorem index_in : forall l x, In x l -> exists n, index x l = Some n.
Proof.
  intros l x H. induction l.
  - destruct H.
  - destruct H as [-> | H].
    + exists 0. unfold index. simpl. destruct (x =? x) eqn:E.
      * reflexivity.
      * rewrite Nat.eqb_neq in E. contradiction.
    + apply IHl in H as [n Hn].
      unfold index. simpl. destruct (a =? x) eqn:E.
      * exists 0. reflexivity.
      *

我有两个问题：

1. 在我证明的引理中，还有更好的证明吗？或者使用

   destruct

   和

   Nat.eqb_neq

   是证明这一点的好方法？
2. 我不知道以下证明该定理的策略是什么。我不知道如何从

   n

   推断出

   In x l

   的存在。我能怎么做？ （我会接受线索而不是完整的答案。我仍然想自己证明这一点，但我被困住了。）

Answer 1

2条线索：

1. 直接证明

   index

   上的属性意味着你证明了关于

   forall x l, index_aux x l 0

   的属性，这可能不够通用（你最终需要一些关于

   index_aux x l <something else>

   的东西）。这是一条一般规则（即使对于笔和纸规则）：归纳法证明可能需要推广才能使归纳法真正发挥作用。
2. 注意不要过早使用归纳假设。