How to merge two trees in coq?

Question

The trees mentioned here have the property that on all subtrees (including the whole tree), the contents of the root has the highest priority; but no order is specified on sibling nodes.

The definition of the tree is as following:

Inductive tree : Set :=
| nil : tree
| cons : tree->nat->tree->tree.

I want to merge two trees using coq. Suppose two tree are (cons l1 n1 r1) and (cons l2 n2 r2), if n1 <= n2 then I merge l1 and r1 as a subtree and create the new tree ((merge l1 r1) n1 (cons l2 n2 r2)). And similar treatment can be used when n2 <= n1.

Here is the definition of merge:

Fixpoint merge (t1 t2 : tree) : tree.
  destruct t1 as [ | l1 n1 r1].
  apply t2.
  destruct t2 as [ | l2 n2 r2].
    apply (cons l1 n1 r1).
    destruct (le_le_dec n1 n2).
      apply (cons (merge l1 r1) n1 (cons l2 n2 r2)).
      apply (cons (cons l1 n1 r1) n2 (merge l2 r2)).
Defined.

The problem is that coq thinks the definition above is ill-formed. But indeed the merge function can finally terminate.

I know that coq requires a decreasing argument for fixpoint. But how to deal with the function with two decreasing arguments?

The lemma le_le_dec is just defined for case analysis:

Lemma le_le_dec : forall x y, {x <= y}+{y <= x}.
Proof.
  intros x y.
  destruct (nat_delta x y) as [xy | yx].
    destruct xy as [n e]. left. apply le_delta. exists n. assumption.
    destruct yx as [n e]. right. apply le_delta. exists n. assumption.
Qed.

The lemma le_delta and nat_delta is as following:

Lemma le_delta: forall n m, n <= m <-> exists x, (x + n = m).
Proof.
  intros n m.
  split.
  intros e. induction e as [ |m les IHe].
    exists 0. simpl. reflexivity.
    destruct IHe as [x  e]. exists (S x). simpl. rewrite e. reflexivity.
  intros e. destruct e as [x e]. revert e. revert m.
  induction x as [ | x IHx].
    intros m e. simpl in e. rewrite e. apply le_n.
    intros m e. destruct m as [ | m].
      discriminate e.
      apply (le_S n m).
      apply (IHx m).
      inversion e. reflexivity.
Qed.

Lemma nat_delta : forall x y, {n | n+x=y} + {n | n+y=x}.
Proof.
  intros x y. induction x as [ | x IHx].
    left. exists y. simpl. rewrite <- (plus_n_O y). reflexivity.
    destruct IHx as [xy | yx].
    destruct xy as [n e]. destruct n as [ | n].
      right. exists (S 0). rewrite <- e. simpl. reflexivity.
      left. exists n. rewrite <- plus_n_Sm. rewrite <- e. simpl. reflexivity.
    destruct yx as [n e].    
    right. exists (S n). simpl. rewrite e. reflexivity.
Qed.

The error message of the fixpoint is :

Error:
Recursive definition of merge is ill-formed.
In environment
merge : tree -> tree -> tree
t1 : tree
t2 : tree
l1 : tree
n1 : nat
r1 : tree
l2 : tree
n2 : nat
r2 : tree
l : n2 <= n1
Recursive call to merge has principal argument equal to "l2" instead of
one of the following variables: "l1" "r1".
Recursive definition is:
"fun t1 t2 : tree =>
 match t1 with
| nil => t2
| cons l1 n1 r1 =>
     match t2 with
     | nil => cons l1 n1 r1
     | cons l2 n2 r2 =>
         let s := le_le_dec n1 n2 in
         if s
         then cons (merge l1 r1) n1 (cons l2 n2 r2)
         else cons (cons l1 n1 r1) n2 (merge l2 r2)
     end
 end".

I have never seen anyone try to define a Fixpoint using L_{tac}. Is that even possible? — ReyCharles
Our teacher taught us two forms defining a fixpoint. But I don't know how to destruct {x <= y}+{y <= x} in a normal definition of the fixpoint — cachuanghu
Could you provide the definitions of le_delta and nat_delta to make it easier to help you please? -- or/and, give an accurate error message — Ptival

Unknown Unknown · Accepted Answer · 2012-12-02T13:33:47

You must use the same sole decreasing argument on any recursive call. Try this:

Fixpoint merge (t1 t2 : tree) : tree.
  destruct t1 as [ | l1 n1 r1].
  apply t2.
  destruct t2 as [ | l2 n2 r2].
    apply (cons l1 n1 r1).
    destruct (le_le_dec n1 n2).
      apply (cons (cons l2 n2 r2) n1 (merge l1 r1)).
      apply (cons (merge l1 r1) n2 (cons l2 n1 r2)).
Defined.

I'm not sure if this way the properties of your program are preserved, but if your not sure either you could try to prove they are.

If instead of proving your function exists you simply wrote it, you would be able to use Function instead of Fixpoint to prove your function terminates without changing it's structure.

Also, I get an error trying to extract le_le_dec. I think that's because le_le_dec is more on the logic side. Why don't you compare n1 and n2 with a function that returns a bool and do case analysis on the result?

You could also try this:

Fixpoint meas (t1: tree): nat :=
  match t1 with
  | nil => O
  | cons t2 _ t3 => S ((meas t2) + (meas t3))
  end.

Fixpoint less_eq (n1 n2: nat): bool :=
  match n1, n2 with
  | O, O => true
  | O, S _ => true
  | S _, O => false
  | S n3, S n4 => less_eq n3 n4
  end.

Program Fixpoint merge (t1 t2: tree) {measure ((meas t1) + (meas t2))}: tree :=
  match t1 with
  | nil => t2
  | cons l1 n1 r1 =>
    match t2 with
    | nil => cons l1 n1 r1
    | cons l2 n2 r2 =>
      match less_eq n1 n2 with
      | false => cons (cons l1 n1 r1) n2 (merge l2 r2)
      | true => cons (merge l1 r1) n1 (cons l2 n2 r2)
      end
    end
  end.

Then you need to type Next Obligation., and prove some stuff.

How to merge two trees in coq?

2 Answers