在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. 如何从In x l推导出存在n使index x l = Some n？希望获得证明思路提示。

解答 #

关于引理的优化证明 #

你的证明方式是合理的，但可以借助Coq内置库简化步骤：

• 对于index_singleton和index_double，利用Nat.eqb_refl（自然数等于自身时，等于判断返回true）可直接跳过矛盾分支的处理：

  Lemma index_singleton : forall x, index x [x] = Some 0.
  Proof.
    intros x. unfold index. simpl. rewrite Nat.eqb_refl. reflexivity.
  Qed.
  
  Lemma index_double : forall x, index x [x; x] = Some 0.
  Proof.
    intros x. unfold index. simpl. rewrite Nat.eqb_refl. reflexivity.
  Qed.
  

  这种方式更简洁，无需手动处理false分支的矛盾，因为Nat.eqb_refl直接保证了x =? x为true。

关于index_in定理的证明思路 #

核心是对列表l进行归纳，结合In谓词的结构分情况讨论：

1. 归纳基例：当l为空时，In x []本身是矛盾命题，直接destruct H即可终止证明。
2. 归纳步骤：当l = a :: t时，In x l分为两种情况：
   • x = a：此时index x l会直接返回Some 0，构造存在量0即可完成证明。
   • x在t中：此时调用归纳假设（In x t蕴含存在n使得index x t = Some n），同时注意index x (a::t)递归时会传入i+1，因此最终的存在量应为n+1。
     处理a =? x的false分支时，可通过Nat.eqb_neq推导出a <> x，从而排除x = a的情况，确保x一定在t中，进而应用归纳假设。

完整的定理证明代码 #

Theorem index_in : forall l x, In x l -> exists n, index x l = Some n.
Proof.
  unfold index. intro l. generalize dependent 0. induction l.
  - intros _ _ [].
  - intros n x H. unfold index_aux. destruct (a =? x) eqn:E; fold index_aux.
    + exists n. reflexivity.
    + rewrite Nat.eqb_neq in E. destruct H as [->|H].
      * contradiction.
      * apply IHl with (n:=n + 1) in H. assumption.
Qed.

内容的提问来源于stack exchange，提问作者Lepticed