How to fold simplified goal?

Question

I have written a Program Fixpoint called generic_debugging_algorithm with a measure, and I have one obligation left to prove. To me the obligation reads like:

weight head < weight n

which is something I have already proved in the lemma parent_weight_gt_child_weight. However, Coq has simplified weight head to：

match head.(children) with
  | [] => 1
  | n0 :: l =>
      S
        (weight n0 +
         list_sum
           (map (fun child : Node => weight child) l))

Note that the difference with the definition of weight is that the second pattern is expanded from children to n0 :: l.

After proving that In head n.(children), I try to apply parent_weight_gt_child_weight, but Coq is unable to unify. I also try to fold, but it does not work.

Would it be possible to change the goal to weight head < weight n?

Full code to reproduce below.

From Coq Require Export Arith.
Require Import Bool.
Require Import List.
Require Import Program.Wf.

Inductive Correctness : Type :=
| yes : Correctness
| no : Correctness
| trusted : Correctness
| idk : Correctness.
Scheme Equality for Correctness.

Inductive Node : Type := mkNode
                           { correctness : Correctness
                           ; children : list Node
                           }.

Fixpoint weight (node : Node) : nat :=
  match node.(children) with
    nil => 1
  | children => S (list_sum (map (fun child => weight child) (children)))
  end.

Lemma weight_g_0: forall n:Node, 0 < weight n.
Proof. intros n. induction n. induction children0. simpl. intuition. simpl. intuition.
Qed.

Lemma nat_in_list_le_list_sum: forall (l:list nat) (element: nat), In element l -> element <= list_sum l.
Proof. intros l element H. induction l.
       - simpl. inversion H.
       - simpl. destruct H.
         + subst. apply Nat.le_add_r.
         + transitivity (list_sum l);auto.
           rewrite Nat.add_comm. apply Nat.le_add_r.
Qed.

Lemma child_weight_le_sum_children_weight: forall (l:list Node) (child: Node), In child l -> list_sum (map (fun child => weight child) l) >= weight child.
Proof. intros l child H. apply nat_in_list_le_list_sum. induction l.
       - simpl. inversion H.
       - simpl. destruct H.
         + subst. intuition.
         + subst. intuition.
Qed.

Lemma parent_weight_gt_child_weight: forall parent child:Node, In child (children parent) -> weight child < weight parent.
Proof. intros parent child H. induction parent. simpl. induction children0.
       + inversion H.
       + inversion H.
         - rewrite H0. intuition.
         -  intuition. assert (weight child <= list_sum (map (fun child0 : Node => weight child0) children0)). apply child_weight_le_sum_children_weight. assumption. intuition. assert (weight a > 0). apply weight_g_0. assert (weight child < (weight a + list_sum (map (fun child0 : Node => weight child0) children0))). inversion H2. rewrite Nat.add_comm. apply Nat.lt_add_pos_r. assumption. assert (weight child < S m). intuition. rewrite Nat.add_comm. intuition. intuition.
Qed.

Definition get_debugging_tree_from_tree (n : Node) : Node :=
  mkNode no (children n).

Program Fixpoint generic_debugging_algorithm (n : Node) {measure (weight n)}: Node :=
  match children n with
    nil => n
  | head::tail => generic_debugging_algorithm (get_debugging_tree_from_tree head)
  end.
Next Obligation.
  assert (In head (children n)). induction (children n). inversion Heq_anonymous.  simpl. left. injection Heq_anonymous. intuition. fold (match head.(children) with
  | [] => 1
  | n0 :: l =>
      S
        (weight n0 +
         list_sum
           (map (fun child : Node => weight child) l))
  end).

Answer 1

Your goal is not exactly weight head < weight n, but weight (get_debugging_tree_from_tree head) < weight n. I could have discovered this by paying a lot of attention, but that's hard. What I did instead was:

Obligation Tactic := intros.

This changes the default tactic used by Program. In particular it avoids simplifying the goal. It won't automatically solve the second obligation anymore, but it's useful for debugging.

---

fold is admittedly kind of useless here, but you can obtain that expression back with:

change (match _ with nil => _ | _ => _ end) with
  (weight (get_debugging_tree_from_tree head)).

If you believe that get_debugging_tree_from_tree head = head, then proving so will make the rest of the proof easy. But from my brief inspection I don't think that holds.

---

PS: You don't need to write (fun child : Node => weight child); it is enough to use weight in this case. The former is an eta-expansion of the latter.