<p>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 <a href="http://coq.inria.fr/refman/Reference-Manual006.html#htoc101">definition of structurally smaller</a> includes higher-order types, which is extremely powerful.</p>

<p>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.</p>

<pre><code>Fixpoint pair l := fix pair1 (r : Tree) :=
  match l with
    | Tip =&gt; match r with
              | Tip =&gt; TipTip
              | Bin rl rr =&gt; TipBin rl rr
            end
    | Bin ll lr =&gt; match r with
                    | Tip =&gt; BinTip ll lr
                    | Bin rl rr =&gt; BinBin (pair1 rl) (pair lr r)
                   end
  end.
</code></pre>

<p>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 <a href="http://coq.inria.fr/stdlib/Coq.Init.Wf.html">well-foundedness argument</a>, often using an <a href="http://coq.inria.fr/stdlib/Coq.Arith.Wf_nat.html">integer measure</a>. You can also make your definition look more like a classical program in a non-total language with a separate termination using the <a href="http://coq.inria.fr/refman/Reference-Manual028.html"><code>Program</code> vernacular</a>.</p>

CC BY-SA 2.5
2010-09-30T22:37:57.483Z
Now I know this is what I asked for!
yhirai
CC BY-SA 2.5
2011-02-28T09:36:36.060Z
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)?
day
CC BY-SA 2.5
2011-02-28T23:33:33.010Z
@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).
Gilles 'SO- stop being evil'
CC BY-SA 2.5
2010-09-30T20:14:36.350Z
2010-09-30T20:14:36.350Z
Gilles 'SO- stop being evil'
<p>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.</p>

<p>Specifically, the function takes two trees as input.</p>

<pre><code>Inductive Tree :=
| Tip: Tree
| Bin: Tree -&gt; Tree -&gt; Tree.
</code></pre>

<p>On Trees, I like to do the following style of induction.</p>

<pre><code>Inductive TreePair :=
| TipTip : TreePair
| TipBin : Tree -&gt; Tree -&gt; TreePair
| BinTip : Tree -&gt; Tree -&gt; TreePair
| BinBin : TreePair -&gt; TreePair -&gt; TreePair.

Fixpoint pair (l r: Tree): TreePair :=
  match l with
    | Tip =&gt;
      match r with
        | Tip =&gt; TipTip
        | Bin rl rr =&gt; TipBin rl rr
      end
    | Bin ll lr =&gt;
      match r with
        | Tip =&gt; BinTip ll lr
        | Bin rl rr =&gt; BinBin (pair l rl) (pair lr r)
      end
  end.
</code></pre>

<p>The definition of TreePair is accepted, but the definition of the function pair yields the error message:</p>

<pre><code>Error: Cannot guess decreasing argument of fix.
</code></pre>

<p>So I am interested in how to convince Coq of the termination.</p>

CC BY-SA 2.5
2010-09-30T10:11:28.283Z
Have you tried passing l and r together as a product rather than using currying? That should help it along.
Per Vognsen
CC BY-SA 2.5
2010-09-30T13:43:05.920Z
[Some people](http://meta.cstheory.stackexchange.com/questions/425/questions-about-compilation-errors-in-coq) 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.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-30T14:04:07.403Z
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.
Dave Clarke
<interactive-proofs><proof-assistants><coq>
How to define a function inductively on two arguments in Coq?
yhirai
# How to define a function inductively on two arguments in Coq?

(Asked by: username_0 on 2010-09-30)

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.

**Tags:** interactive-proofs, proof-assistants, coq

> **Comments:**
> **username_1**: Have you tried passing l and r together as a product rather than using currying? That should help it along.  
> **username_2**: [Some people](http://meta.cstheory.stackexchange.com/questions/425/questions-about-compilation-errors-in-coq) 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.  
> **username_3**: 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.  

---

## 1 answers

### Answer by username_4 on 2010-09-30. Score: 13 | Accepted answer

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.

> **Comments:**
> **username_0**: Now I know this is what I asked for!  
> **username_5**: 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)?  
> **username_4**: @plmusername_5: 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).  

---

