如何为无额外参数的LDD图定义Fixpoint的递减参数？

背景定义 #

LDD状态结构 #

定义的LDD图结构如下：

Definition ldd_state : Type := gmap loc (nat * (loc * loc)).

该结构是loc（对应positive类型）到nat值+两个子节点的映射。节点层级规则：右子节点深度与父节点一致，下子节点深度递减，终端节点ldd_zero深度为0。

有界深度归纳定义 #

配套的bounded_depth归纳定义用于约束节点深度：

Inductive bounded_depth (ls : ldd_state) : loc → nat → Prop :=
      | depth_f : ∀ n : nat, bounded_depth ls ldd_zero n (* ldd_zero可匹配任意节点的深度 *)
      | depth_t :            bounded_depth ls ldd_one 0
      | depth_x : ∀ (id d r : loc) (v : nat) (n : nat) (p : path),
          ls !! id = Some (v, (d, r)) →
          bounded_depth ls d n →
          bounded_depth ls r (n+1) → bounded_depth ls id (n+1).

有界值归纳定义 #

bounded_value归纳定义约束节点存储的nat值范围：

Inductive bounded_value (ls : ldd_state) : loc → nat → Prop :=
      | value_zero : ∀ n, bounded_value ls ldd_zero n (* ldd_one与ldd_zero无实际值 *)
      | value_one  : ∀ n, bounded_value ls ldd_one n
      | value_s    : ∀ (id d r : loc) (n nd nr : nat),
          ls !! id = Some (n, (d, r)) →
          ldd_compare ls id r = Datatypes.Lt →
          n < S p → (* 所有节点值不超过p *)
          bounded_value ls d nd →
          bounded_value ls r nr → bounded_value ls id n.

需求问题 #

想要定义遍历该LDD图的递归函数，例如目标函数semantics_of_ldd：

Function semantics_of_ldd (id : loc) (rn : nat * nat) 
    (H : rn = (compute_measure ls id)) {wf measure rn} : gset (list loc) :=
    match ls !! id with
    | None => if Loc.eq_dec id ldd_zero then ∅ (* ldd_zero *) else {[ [] ]} (* ldd_one *)
    | Some ((v, depth), (d, r)) =>
      match rn with
      | (0, _) => {[ [] ]} (* ldd_one, error分支 *)
      | (_, 0) => ∅ (* ldd_zero, error分支 *)
      | _ =>
        let sd := semantics_of_ldd d (compute_measure ls d) 
          (eq_refl (compute_measure ls d)) in
        let sr := semantics_of_ldd r (compute_measure ls r) 
          (eq_refl (compute_measure ls r)) in
        set_map (λ x : path, id :: x) sd ∪ sr
      end
  end.

现有bounded_depth和bounded_value理论上已提供足够信息构造递减排序参数，但多次尝试未成功。需确认该递归函数是否可合法定义，以及具体实现方式。

实现方案 #

完全可行，核心是利用已有的归纳约束构造良基递归的递减测度，以下是三种具体实现路径：

路径1：基于深度+值的字典序测度 #

1. 提取节点属性：为每个节点从bounded_depth中提取深度值depth_of ls id，从bounded_value中提取存储值value_of ls id。
2. 定义良基序：使用nat×nat的字典序（lexprod nat_lt nat_lt），该序是良基的，符合Coq对递归的要求。
3. 证明递减性：
   • 下子节点d：根据depth_x子句，depth_of ls d = n，父节点id的深度为n+1，因此(n, value_of d) < (n+1, value_of id)。
   • 右子节点r：深度与父节点相同（n+1），但ldd_compare ls id r = Lt对应value_of ls r < value_of ls id，因此(n+1, value_of r) < (n+1, value_of id)。
4. 修改函数定义：用Function或Program Fixpoint指定该字典序为良基测度，并补全递减性证明。

路径2：直接利用bounded_depth的归纳原理 #

无需显式定义测度，通过将bounded_depth的存在性作为函数参数，利用归纳结构约束递归调用：

Fixpoint semantics_of_ldd (ls : ldd_state) (id : loc) (H : ∃ n, bounded_depth ls id n) : gset (list loc) :=
  match ls !! id with
  | None => if Loc.eq_dec id ldd_zero then ∅ else {[ [] ]}
  | Some (v, (d, r)) =>
    match H with
    | ex_intro n (depth_x _ _ _ _ _ _ Hmap Hd Hr) =>
      let sd := semantics_of_ldd ls d (ex_intro _ Hd) in
      let sr := semantics_of_ldd ls r (ex_intro _ Hr) in
      set_map (λ x, id :: x) sd ∪ sr
    | ex_intro _ depth_f => ∅
    | ex_intro _ depth_t => {[ [] ]}
    end.

该方式通过bounded_depth的归纳子句自然保证递归调用的合法性——每个递归调用都对应子节点的深度约束，满足良基递归的要求。

路径3：使用Program Fixpoint自动推导 #

保留类似原代码的结构，用Program Fixpoint结合约束条件让Coq自动处理良基关系：

Require Import Program.Wf.

Program Fixpoint semantics_of_ldd (ls : ldd_state) (id : loc) 
  (H_depth : ∃ n, bounded_depth ls id n)
  (H_value : bounded_value ls id p) {wf (depth_of ls id, value_of ls id) (lexprod nat_lt nat_lt)} : gset (list loc) :=
  match ls !! id with
  | None => if Loc.eq_dec id ldd_zero then ∅ else {[ [] ]}
  | Some (v, (d, r)) =>
    set_map (λ x, id :: x) (semantics_of_ldd ls d _ _) ∪ (semantics_of_ldd ls r _ _)
  end.
Next Obligation.
(* 证明d的测度严格小于id的测度：depth_of ls d < depth_of ls id *)
Admitted.
Next Obligation.
(* 证明r的测度严格小于id的测度：深度相同但value_of ls r < value_of ls id *)
Admitted.
Next Obligation.
(* 提供d的bounded_depth存在性假设 *)
Admitted.
Next Obligation.
(* 提供d的bounded_value假设 *)
Admitted.
Next Obligation.
(* 提供r的bounded_depth存在性假设 *)
Admitted.
Next Obligation.
(* 提供r的bounded_value假设 *)
Admitted.

需要补全的义务证明均可通过bounded_depth和bounded_value的归纳假设推导得出。

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