<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?
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**: @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.  
> **username_1**: You don't have to explain this to me, but to Coq :-)  
> **username_0**: @AndrejBauer: I was hoping to use you as a English to Coq compiler.  
> **username_2**: 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  
> **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 (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

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).  

---

