Coq递归函数中构造证明项的问题求助

问题背景 #

刚接触Coq，尝试编写一个列表插入函数，通过sumor类型返回结果：若索引合法则返回插入后的新列表，若索引非法则返回对应的证明。递归逻辑已理清，但构造证明项时遇到困难。

初始代码 #

Fixpoint insert {A: Type} (lst: list A) (n: nat) (x: A): (list A)+{n >= length lst} :=
  match lst, n return (list A)+{n >= length lst} with
  | [ ], O => inleft [ x ]
  | [ ], S n' => inright (* proof term for `n >= length lst` *)
  | h :: t, S n' => match insert' _ t n' with
                    | inleft lst' => inleft (h :: lst')
                    | inright P (* : n' >= length lst' *) => inright _ (* proof term for n >= length lst *)
                    end
  | _, O => inleft x :: lst
  end.

后续尝试与错误 #

定义了三个辅助引理：

Lemma simple_test: forall (A: Type) (lst: list A) (n: nat), lst = [] /\ n > 0 -> n > length lst.
Lemma Sn_gt_0: forall n: nat, S n > 0.
Lemma Sn_gt_len_tail: forall (A: Type) (h: A) (t: list A) (n': nat),
    n' >= length t -> S n' >= length (h :: t).

修改后的实现：

Fixpoint insert' {A: Type} (lst: list A) (n: nat) (x: A): (list A)+{n >= length lst} :=
  match lst return (list A)+{n >= length lst} with
  | [ ] => match n with
           | O => inleft [ x ]
           | S n' => inright _
                       (* proof term for `n >= length lst` *)
                       (simple_test A lst n (conj (eq_refl lst) (Sn_gt_0 n')))
           end
  | h :: t => match n with
              | O => inleft x :: lst
              | S n' => fun _ => 
                          match insert' _ t n' with
                          | inleft lst' => inleft h :: lst'
                          | inright P (*: n' >= length t*) => inright _ (Sn_gt_len_tail P)
                          end
              end
  end.

遇到错误：

The term conj eq_refl (Sn_gt_0 n') has type lst = lst /\ S n' > 0 while it is expected to have type lst = [] /\ n > 0.

核心问题与修复 #

1. 空列表分支的证明项不匹配 #

在lst = []的分支里，上下文已经明确lst就是[]，所以直接用eq_refl（即[] = []）即可；同时n就是S n'，Sn_gt_0 n'正好对应n > 0。把simple_test的参数替换为具体的[]和S n'就能匹配类型。

2. 递归分支多余的匿名函数 #

fun _ =>会破坏类型一致性，直接去掉即可。另外Sn_gt_len_tail需要传入所有参数（之前漏了A、h、t、n'），补全后才能正确构造证明。

3. 语法错误：缺少括号 #

Coq的优先级规则会把inleft x :: lst解析成(inleft x) :: lst，完全不符合预期，必须给x :: lst加上括号。

完整修正后的代码 #

Lemma simple_test: forall (A: Type) (lst: list A) (n: nat), lst = [] /\ n > 0 -> n > length lst.
Proof.
  intros A lst n [Hl Hn]. simpl. rewrite Hl. apply Hn.
Qed.

Lemma Sn_gt_0: forall n: nat, S n > 0.
Proof.
  intros n. simpl. reflexivity.
Qed.

Lemma Sn_gt_len_tail: forall (A: Type) (h: A) (t: list A) (n': nat),
    n' >= length t -> S n' >= length (h :: t).
Proof.
  intros A h t n' H. simpl. apply le_n_S. apply H.
Qed.

Fixpoint insert' {A: Type} (lst: list A) (n: nat) (x: A): (list A)+{n >= length lst} :=
  match lst return (list A)+{n >= length lst} with
  | [] => match n with
          | O => inleft [x]
          | S n' => inright (simple_test A [] (S n') (conj eq_refl (Sn_gt_0 n')))
          end
  | h :: t => match n with
              | O => inleft (x :: lst)
              | S n' => match insert' t n' x with
                        | inleft lst' => inleft (h :: lst')
                        | inright P => inright (Sn_gt_len_tail A h t n' P)
                        end
              end
  end.

学习资料建议 #

• 《Software Foundations》：Coq官方入门教程，分卷讲解基础逻辑、函数式编程、程序验证，重点看第一卷《Logical Foundations》中的递归函数、依赖类型、证明构造章节。
• 《Coq in a Hurry》：快速入门手册，聚焦常用语法和证明技巧，适合解决具体问题时查阅。
• Coq标准库文档：重点关注List和Arith模块，里面有大量现成的引理（如length_cons、le_S等），可以避免重复造轮子。
• 实战练习：尝试实现链表、二叉树等简单数据结构的操作并验证性质，逐步积累依赖类型编程的经验。

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