<p>As stated in <a href="http://coq.inria.fr/V8.2pl1/refman/Reference-Manual004.html" rel="nofollow">Coq Reference Manual</a> (2.3)</p>

<blockquote>
  <p>in Fixpoint, the decreasing argument must be given (unless the
  function is not recursive), but it must not necessary be <em>structurally</em>
  decreasing.</p>
</blockquote>

<p>Key word is <em>structurally</em>, Coq can't guess, which arguments is decreasing at each step of the recursion.</p>

<p>The reason for this is nicely described in <a href="http://www.cis.upenn.edu/~bcpierce/sf/Imp.html" rel="nofollow">Software Foundations</a></p>

<blockquote>
  <p>Since Coq is not just a functional programming language, but also a
  consistent logic, any potentially non-terminating function needs to be
  rejected. Here is an (invalid!) Coq program showing what would go
  wrong if Coq allowed non-terminating recursive functions:</p>

<pre><code> Fixpoint loop_false (n : nat) : False := loop_false n. 
</code></pre>
  
  <p>That is, propositions like False would become provable (e.g. loop_false 0 would
  be a proof of False), which would be a disaster for Coq's logical
  consistency.</p>
</blockquote>

CC BY-SA 3.0
2014-03-27T00:57:47.010Z
Regarding your comment: "Coq can't guess, which arguments is decreasing at each step of the recursion." Not yet :) Me too I have access to some insider information and apparently it's a work-in-progress.
NisaiVloot
CC BY-SA 3.0
2014-03-27T01:08:56.307Z
So it this behaviour will change in next versions?
romants
CC BY-SA 3.0
2014-03-27T01:12:02.080Z
Can't tell that, ask the dev team (http://coq.inria.fr/community).
NisaiVloot
CC BY-SA 3.0
2014-03-27T00:39:05.000Z
2014-03-27T00:39:05.000Z
romants
<p>This question is related to (but not the same as):</p>

<p><a href="https://cstheory.stackexchange.com/questions/1807/how-to-define-a-function-inductively-on-two-arguments-in-coq">How to define a function inductively on two arguments in Coq?</a></p>

<p>In particular, I used those techniques (defining a second fixed point function) and Coq still complains.</p>

<p>Consider the following formalization of regular expressions.</p>

<pre><code>Inductive symbol : Set := Zero | One.

Definition string := list symbol.

Fixpoint symbol_eq (a:symbol) (b:symbol) : bool :=
  match a with
    Zero =&gt;
    match b with
      Zero =&gt; true
    | One =&gt; false
    end
  | One =&gt;
    match b with
      Zero =&gt; false
    | One =&gt; true
    end
  end.


Inductive regexp : Set :=
    Symbol (s:symbol)
  | Concat (r1:regexp) (r2:regexp)
  | Union (u1:regexp) (u2:regexp)
  | Star (u1:regexp)
  .

Fixpoint rgm (r:regexp) (s:string) :=
  match r with
    Symbol ss =&gt;
      match s with
        nil =&gt; false
      | a::nil =&gt; (symbol_eq ss a)
      | a::b::tl =&gt; false
      end
   | Union r1 r2 =&gt; (orb (rgm r1 s) (rgm r2 s))
   | Concat r1 r2 =&gt;
       let fix f s1 s2 :=
         match s2 with
           nil =&gt; (andb (rgm r1 (rev s1)) (rgm r2 s2))
         | a::tl =&gt; (orb (andb (rgm r1 (rev s1)) (rgm r2 s2))
                         (f (a::s1) tl))
         end
       in (f nil s)
   | Star r1 =&gt;
       match s with
         nil =&gt; true
       | a::tl =&gt;
         let fix f s1 s2 :=
           match s2 with
             nil =&gt; (rgm r1 (rev s1))
           | a::tl =&gt; (orb (andb (rgm r1 (rev s1)) (rgm r s2))
                           (f (a::s1) tl))
           end
         in (f (a::nil) tl)
       end
  end.
</code></pre>

<p>Coq refuses to compile it for the following reason:</p>

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

<p>Question: how can we fix this?</p>

CC BY-SA 3.0
2013-02-19T09:29:11.247Z
Do you know about `{struct x}` in `Fixpoint`? It tells Coq which argument it is decreasing. But more importantly, the recursive call `rgm r s2` is suspect. How can Coq tell that it won't loop forever?
Andrej Bauer
CC BY-SA 3.0
2013-02-19T09:49:08.357Z
@AndrejBauer Neither argument is always decreasing. We only know that some argument decreases every step. The (rgm r s2) step is okay because in "Star", we run (f (a::nil) tl) -- thus the length of the string is decreasing every time.
theorems
CC BY-SA 3.0
2013-02-19T09:55:38.643Z
You don't have to explain this to me, but to Coq :-)
Andrej Bauer
CC BY-SA 3.0
2013-02-19T17:19:08.093Z
@AndrejBauer: I was hoping to use you as a English to Coq compiler.
theorems
CC BY-SA 3.0
2013-02-19T20:18:15.117Z
While Andrej always gives good advice, I really have to suggest you take your question to the coq_club mailing list. You can even try to find a suitable answer in the archives: https://sympa.inria.fr/sympa/arc/coq-club/2012-03/mail2.html
cody
CC BY-SA 3.0
2013-02-19T23:24:37.560Z
The Coq `Program` facility is probably what you are looking for.
Andrej Bauer
CC BY-SA 3.0
2013-07-16T15:58:27.697Z
I answered a similar question [here](http://stackoverflow.com/questions/17297165/).
Rui Baptista
<pl.programming-languages><coq>
Defining Mutually Recursive functions in Coq
theorems
# Defining Mutually Recursive functions in Coq

(Asked by: username_0 on 2013-02-19)

This question is related to (but not the same as):

[How to define a function inductively on two arguments in Coq?](https://cstheory.stackexchange.com/questions/1807/how-to-define-a-function-inductively-on-two-arguments-in-coq)

In particular, I used those techniques (defining a second fixed point function) and Coq still complains.

Consider the following formalization of regular expressions.

```
Inductive symbol : Set := Zero | One.

Definition string := list symbol.

Fixpoint symbol_eq (a:symbol) (b:symbol) : bool :=
  match a with
    Zero =>
    match b with
      Zero => true
    | One => false
    end
  | One =>
    match b with
      Zero => false
    | One => true
    end
  end.

Inductive regexp : Set :=
    Symbol (s:symbol)
  | Concat (r1:regexp) (r2:regexp)
  | Union (u1:regexp) (u2:regexp)
  | Star (u1:regexp)
  .

Fixpoint rgm (r:regexp) (s:string) :=
  match r with
    Symbol ss =>
      match s with
        nil => false
      | a::nil => (symbol_eq ss a)
      | a::b::tl => false
      end
   | Union r1 r2 => (orb (rgm r1 s) (rgm r2 s))
   | Concat r1 r2 =>
       let fix f s1 s2 :=
         match s2 with
           nil => (andb (rgm r1 (rev s1)) (rgm r2 s2))
         | a::tl => (orb (andb (rgm r1 (rev s1)) (rgm r2 s2))
                         (f (a::s1) tl))
         end
       in (f nil s)
   | Star r1 =>
       match s with
         nil => true
       | a::tl =>
         let fix f s1 s2 :=
           match s2 with
             nil => (rgm r1 (rev s1))
           | a::tl => (orb (andb (rgm r1 (rev s1)) (rgm r s2))
                           (f (a::s1) tl))
           end
         in (f (a::nil) tl)
       end
  end.

```

Coq refuses to compile it for the following reason:

```
Error: Cannot guess decreasing argument of fix.

```

Question: how can we fix this?

**Tags:** pl.programming-languages, coq

> **Comments:**
> **username_1**: Do you know about `{struct x}` in `Fixpoint`? It tells Coq which argument it is decreasing. But more importantly, the recursive call `rgm r s2` is suspect. How can Coq tell that it won't loop forever?  
> **username_0**: @username_1 Neither argument is always decreasing. We only know that some argument decreases every step. The (rgm r s2) step is okay because in "Star", we run (f (a::nil) tl) -- thus the length of the string is decreasing every time.  
> **username_1**: You don't have to explain this to me, but to Coq :-)  
> **username_0**: @username_1: I was hoping to use you as a English to Coq compiler.  
> **username_2**: While username_1 always gives good advice, I really have to suggest you take your question to the coq_club mailing list. You can even try to find a suitable answer in the archives: https://sympa.inria.fr/sympa/arc/coq-club/2012-03/mail2.html  
> **username_1**: The Coq `Program` facility is probably what you are looking for.  
> **username_3**: I answered a similar question [here](http://stackoverflow.com/questions/17297165/).  

---

## 1 answers

### Answer by username_4 on 2014-03-27. Score: 1

As stated in [Coq Reference Manual](http://coq.inria.fr/V8.2pl1/refman/Reference-Manual004.html) (2.3)

> in Fixpoint, the decreasing argument must be given (unless the
> function is not recursive), but it must not necessary be *structurally*
> decreasing.

Key word is *structurally*, Coq can't guess, which arguments is decreasing at each step of the recursion.

The reason for this is nicely described in [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/Imp.html)

> Since Coq is not just a functional programming language, but also a
> consistent logic, any potentially non-terminating function needs to be
> rejected. Here is an (invalid!) Coq program showing what would go
> wrong if Coq allowed non-terminating recursive functions:
>
> ```
>  Fixpoint loop_false (n : nat) : False := loop_false n. 
>
> ```
>
> That is, propositions like False would become provable (e.g. loop\_false 0 would
> be a proof of False), which would be a disaster for Coq's logical
> consistency.

> **Comments:**
> **username_5**: Regarding your comment: "Coq can't guess, which arguments is decreasing at each step of the recursion." Not yet :) Me too I have access to some insider information and apparently it's a work-in-progress.  
> **username_4**: So it this behaviour will change in next versions?  
> **username_5**: Can't tell that, ask the dev team (http://coq.inria.fr/community).  

---

