Coq实现BDD时apply_and函数类型推断失败，求解决方案

我尝试在Coq中基于2CNF公式实现二元决策图（BDD），但编写的apply_and递归函数无法通过Coq的终止性检查。添加表示BDD大小之和的参数后，又遇到类型推断错误，以下是具体问题和解决方法：

现有代码实现 #

导入语句 #

Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.EqNat.
Require Import Program.Wf.

文字与子句类型定义 #

Inductive literal := 
  | L (val: nat).

Inductive two_clause := 
  Or (left: literal) (right: literal).

BDD类型及操作函数 #

Inductive bdd := 
  | Vertex (L: literal) (left_edge: bdd) (right_edge: bdd)
  | Leaf (val: Prop).

Definition get_bdd_var (b: bdd) : option literal :=
  match b with
    | Vertex l _ _  => Some l
    | _             => None
  end.

Definition get_high (b: bdd) : bdd := 
  match b with 
    | Vertex _ h _  => h
    | Leaf v        => Leaf v
  end.

Definition get_low (b: bdd) : bdd := 
  match b with 
    | Vertex _ _ l  => l
    | Leaf v        => Leaf v
  end.

问题代码（BDD构造与apply_and函数） #

Definition construct (p: literal) (T U: option bdd) : option bdd := 
  match (T, U) with 
    | (Some T, Some U)  => Some (Vertex p T U)
    | _                 => None
  end.

Fixpoint bdd_size (b: bdd) : nat := 
  match b with 
    | Leaf _ => 0
    | Vertex _ l r => 1 + (bdd_size l) + (bdd_size r)
  end.

Definition bdds_size (b1 b2: bdd) : nat := 
  bdd_size b1 + bdd_size b2.

Variable o_map : literal -> nat.

Fixpoint apply_and (T U : bdd) {bdds_size T U} : option bdd := 
  let tvaro := get_bdd_var T in
  let uvaro := get_bdd_var U in
  match (tvaro, uvaro) with
    | (Some tvar, Some uvar) =>  
      match (compare (o_map (tvar)) (o_map (uvar))) with 
        | Lt => construct
                  (tvar) 
                  (apply_and (get_high T: bdd) U)
                  (apply_and (get_low T: bdd) U)
        | _  => construct
                  (tvar)
                  (apply_and (get_high T:bdd) (get_high U:bdd))
                  (apply_and (get_low T:bdd) (get_low U:bdd))
      end 
    | _ => None
   end.

问题分析 #

原代码中Fixpoint apply_and的写法错误：{bdds_size T U}不是Coq认可的终止性证明语法，Coq无法自动推断该表达式对应的良基关系。此外，即使使用正确的measure语法，也需要明确证明每次递归调用的BDD大小之和严格递减。

解决方案 #

使用Program Fixpoint结合measure子句定义递归函数，并手动提供终止性证明义务：

修改后的apply_and函数 #

Program Fixpoint apply_and (T U : bdd) {measure (bdds_size T U)} : option bdd := 
  let tvaro := get_bdd_var T in
  let uvaro := get_bdd_var U in
  match (tvaro, uvaro) with
    | (Some tvar, Some uvar) =>  
      match (compare (o_map tvar) (o_map uvar)) with 
        | Lt => construct
                  tvar 
                  (apply_and (get_high T) U)
                  (apply_and (get_low T) U)
        | _  => construct
                  tvar
                  (apply_and (get_high T) (get_high U))
                  (apply_and (get_low T) (get_low U))
      end 
    | _ => None
   end.

终止性证明义务 #

定义完Program Fixpoint后，Coq会生成四个需要证明的义务，分别对应四次递归调用的大小递减关系，逐一证明：

(* 证明 apply_and (get_high T) U 的大小小于原大小 *)
Next Obligation.
  destruct T; simpl.
  - reflexivity.
  - apply Nat.lt_add_lt_r. apply Nat.lt_0_succ.
Qed.

(* 证明 apply_and (get_low T) U 的大小小于原大小 *)
Next Obligation.
  destruct T; simpl.
  - reflexivity.
  - apply Nat.lt_add_lt_r. apply Nat.lt_0_succ.
Qed.

(* 证明 apply_and (get_high T) (get_high U) 的大小小于原大小 *)
Next Obligation.
  destruct T, U; simpl.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - apply Nat.add_lt_add; apply Nat.lt_0_succ.
Qed.

(* 证明 apply_and (get_low T) (get_low U) 的大小小于原大小 *)
Next Obligation.
  destruct T, U; simpl.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - apply Nat.add_lt_add; apply Nat.lt_0_succ.
Qed.

说明 #

• Program Fixpoint允许我们延迟终止性证明，通过Next Obligation逐步完成。
• 每个证明义务利用bdd_size的定义：Vertex的大小等于1加上左右子节点的大小，因此子节点的大小必然小于父节点，进而保证递归调用的大小之和严格递减。
• o_map作为全局变量，在证明中可直接使用，无需额外处理。

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