5
$\begingroup$

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).
$\endgroup$

1 Answer 1

4
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thank you, that worked wonders. I also had a Lemma that I ommited from the code because I thought was irrelevant. Lemma debugging_tree_of_tree_has_same_weight: forall n:Node, weight n = weight (get_debugging_tree_from_tree n). By using this and the other lemma I proved my result. $\endgroup$ Jun 10 at 7:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.