Coq Decreasing Argument mapping

Question

I have a graph defined as follows.

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

This is a mapping from a loc (positive) to a value nat, and two children. Every node "lives" on a level, or depth. Along right edges, the depth is the same, and following the down edge, the depth decreases. The terminal vertex zero has depth 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).

This used to depend on an extra argument that was given to the nodes.

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).

However, this extra argument is not something I want to add. Using this argument, however, it was doable to define a decreasing argument.

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

This uses the added argument as the first argument, and the value of the node increasing to a s Along the right edges, the values increase until a maximum value.

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.

My question is, suppose I want to define a Fixpoint that goes over this graph. There should be enough information to find a decreasing argument, however, even after trying for many days, I cannot find one. Is this possible, and if so, how?

Thank you.

Edit. The fixed point I would like to compute is defined by the following function.

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

The simplest solution here is to use the size of the graph as fuel.

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).

Then you can prove that as long as the fuel is greater than the depth of the current node (= the depth of recursion; which is distinct from the "depth" you've defined), semantics_of_ldd fuel computes the correct result (example properties are: (1) it always produces the same result as long as the fuel is large enough; (2) the semantics is identical to a simple definition over an inductively defined tree).

---

Another measure could be the current node id itself, if you can rely on the invariant that a node's id is always greater than its children's.

---

If you have evidence that the input satisfies bounded_value, then you can use that evidence as the decreasing argument. A simple way is to make it a Type instead of Prop:

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

Then you can write the fixpoint as

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.

Keeping the bounded_value predicate as Prop is also possible but more difficult. And of course, to produce such evidence, you will need to rely on simpler termination arguments (such as the previous ones).