14
$\begingroup$

How can I convince Coq that the recursive function given below terminates? The function takes two inductive arguments. Intuitively, the recursion terminates because either argument is decomposed.

Specifically, the function takes two trees as input.

Inductive Tree :=
| Tip: Tree
| Bin: Tree -> Tree -> Tree.

On Trees, I like to do the following style of induction.

Inductive TreePair :=
| TipTip : TreePair
| TipBin : Tree -> Tree -> TreePair
| BinTip : Tree -> Tree -> TreePair
| BinBin : TreePair -> TreePair -> TreePair.

Fixpoint pair (l r: Tree): TreePair :=
  match l with
    | Tip =>
      match r with
        | Tip => TipTip
        | Bin rl rr => TipBin rl rr
      end
    | Bin ll lr =>
      match r with
        | Tip => BinTip ll lr
        | Bin rl rr => BinBin (pair l rl) (pair lr r)
      end
  end.

The definition of TreePair is accepted, but the definition of the function pair yields the error message:

Error: Cannot guess decreasing argument of fix.

So I am interested in how to convince Coq of the termination.

$\endgroup$
  • 1
    $\begingroup$ Have you tried passing l and r together as a product rather than using currying? That should help it along. $\endgroup$ – Per Vognsen Sep 30 '10 at 10:11
  • 1
    $\begingroup$ Some people think that this question is about programming and out of scope of this website. While I am not sure if I agree, you might want to know about the potential issue. If anyone has something to say about the appropriateness, please write on the meta discussion I linked to. $\endgroup$ – Tsuyoshi Ito Sep 30 '10 at 13:43
  • 3
    $\begingroup$ This question is really about specifying monotonically decreasing bounds on data structures in order to ensure that the operation pair is well-defined. Coq is merely the vehicle. $\endgroup$ – Dave Clarke Sep 30 '10 at 14:04
12
$\begingroup$

Coq's fixpoint definitions require that inductive calls receive a structurally smaller argument. Deep down, a fixpoint construct takes a single argument: there's no built-in concept of a recursive definition over two arguments. Fortunately, Coq's definition of structurally smaller includes higher-order types, which is extremely powerful.

Your two-argument fixpoint definition follows a simple pattern: either the first argument becomes smaller, or the first argument remains identical and the second argument becomes smaller. This fairly common pattern can be handled by a simple fix-in-fix.

Fixpoint pair l := fix pair1 (r : Tree) :=
  match l with
    | Tip => match r with
              | Tip => TipTip
              | Bin rl rr => TipBin rl rr
            end
    | Bin ll lr => match r with
                    | Tip => BinTip ll lr
                    | Bin rl rr => BinBin (pair1 rl) (pair lr r)
                   end
  end.

For more complex cases, or if your tastes run that way, you can use recursion closer to the way it's taught in math courses, building the fixpoint from a step computation and a separate well-foundedness argument, often using an integer measure. You can also make your definition look more like a classical program in a non-total language with a separate termination using the Program vernacular.

$\endgroup$
  • $\begingroup$ Now I know this is what I asked for! $\endgroup$ – yhirai Sep 30 '10 at 22:37
  • $\begingroup$ will it make any difference if I push fix pair1 r into the second branch of the top-level match (and of course adapt the first branch to return a function type accordingly)? $\endgroup$ – day Feb 28 '11 at 9:36
  • $\begingroup$ @plmday: Both way work. They're extensionally equivalent for some reasonable definition of extensionality, and more importantly they're both well-typed (the extensional rewriting doesn't change any of the relevant covariance (positivity) properties). $\endgroup$ – Gilles 'SO- stop being evil' Feb 28 '11 at 23:33

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.