Coq 递减参数映射

Question

我有一个定义如下的图表。

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

这是从

loc

(

positive

) 到值

nat

和两个子项的映射。每个节点都“生活”在一个水平或深度上。沿着右边缘，深度相同，沿着下边缘，深度减小。终端顶点

zero

的深度为 0。

Inductive bounded_depth (ls : ldd_state) : loc → nat → Prop :=
      | depth_f : ∀ n : nat, bounded_depth ls ldd_zero n (* ldd_zero must be same depth as any node *)
      | 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).

这曾经依赖于给予节点的额外参数。

Definition ldd_state : Type := gmap loc ((nat * nat) * (loc * loc)).
Inductive bounded_depth (ls : ldd_state) : loc → nat → Prop :=
      | depth_f : ∀ n : nat, bounded_depth ls ldd_zero n (* ldd_zero must be same depth as any node *)
      | depth_t :            bounded_depth ls ldd_one 0
      | depth_x : ∀ (id d r : loc) (v : nat) (n : nat),
          ls !! id = Some ((v, n + 1), (d, r)) →
          bounded_depth ls d n →
          bounded_depth ls r (n+1) → bounded_depth ls id (n+1).

但是，这个额外的论点并不是我想添加的。 然而，使用这个参数，可以定义递减参数。

Definition measure := (slexprod _ _ lt lt).

这使用添加的参数作为第一个参数，并且节点的值增加到 s 沿右边缘，值增加直至达到最大值。

Inductive bounded_value (ls : ldd_state) : loc → nat → Prop :=
      | value_zero : ∀ n, bounded_value ls ldd_zero n (* ldd_one & ldd_zero have no value *)
      | 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 → (* all nodes have a max value p *)
          bounded_value ls d nd →
          bounded_value ls r nr → bounded_value ls id n.

我的问题是，假设我想定义一个遍历该图的固定点。应该有足够的信息来找到减少的论据，但是，即使在尝试了很多天之后，我也找不到一个。这可能吗？如果可以，如何实现？

谢谢你。

编辑。 我想要计算的不动点由以下函数定义。

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.

Answer 1

这里最简单的解决方案是使用图表的大小作为燃料。

Fixpoint semantics_of_ldd_fueled (fuel : nat) (id : loc) : gset (list loc)
  := match fuel with
     | O => empty (* out of fuel, dummy result *)
     | S fuel => _ (* use the smaller fuel for recursive calls *)
     end.
Definition semantics_of_ldd : id -> gset (list loc)
  := semantics_of_ldd_fueled (size ls).

那么你可以证明，只要

fuel

大于当前节点的深度（=递归深度；与你定义的“深度”不同），

semantics_of_ldd fuel

计算出正确的结果（示例属性是：（1）只要燃料足够大，它总是会产生相同的结果；（2）语义与归纳定义的树上的简单定义相同）。

---

另一个度量可能是当前节点

id

本身，如果您可以依赖节点的

id

始终大于其子节点的不变量。

---

如果您有证据表明输入满足

bounded_value

，那么您可以使用该证据作为递减参数。一个简单的方法就是将其设为

Type

而不是

Prop

:

Inductive bounded_value (ls : ldd_state) : loc → nat → Type :=

然后你可以将固定点写为

Fixpoint semantics_of_ldd (id : loc) (n : nat) (b : bounded_value ls id n) : gset (list loc)
  := match b with
     | depth_f _ => _ (* id = ldd_zero *)
     | depth_t => _ (* id = ldd_one *)
     | depth_x id d r v n p H bd br =>
         _ (* here you can call (semantics_of_ldd d _ bd) and (semantics_of_ldd r _ br) *)
     end.

将

bounded_value

谓词保留为

Prop

也是可能的，但更困难。当然，要产生这样的证据，您需要依赖更简单的终止参数（例如前面的参数）。