Expanding Recursive Functions In Coq

Question

Background

I understand that Iota reduction is used to reduce/expand recursive functions. For instance, given the following application of a simple recursive function (factorial over natural numbers):

((fix fact (n : nat) : nat :=
    match n with
    | O => 1
    | S m => n * fact m end) 2)

Iota reduction expands the recursive call, effectively iterating over the recursive function once:

Eval lazy iota in ((fix fact (n : nat) : nat :=
                      match n with
                      | O => 1
                      | S m => n * fact m end) 2).= (fun n : nat =>
   match n with
   | 0 => 1
   | S m =>
       n *
       (fix fact (n0 : nat) : nat :=
          match n0 with
          | 0 => 1
          | S m0 => n0 * fact m0
          end) m
   end) 2
: nat

This behaviour generalizes nicely to mutually recursive functions. For example, given the following mutually recursive function definitions:

Fixpoint even (n : nat) : Prop := match n with | O => True | S m => odd m end
with odd (n : nat) : Prop := match n with | O => False | S m => even m end.

Iota reduction will correctly expand over recursive calls to even or odd respectively. To see this consider:

Theorem even_2 : even 2.even 2
  lazy delta.(with even (n : nat) : Prop :=
   match n with
   | 0 => True
   | S m => odd m
   end
 with odd (n : nat) : Prop :=
   match n with
   | 0 => False
   | S m => even m
   end
 for
 even) 2
  lazy iota.(fun n : nat =>
 match n with
 | 0 => True
 | S m =>
     (with even (n0 : nat) : Prop :=
        match n0 with
        | 0 => True
        | S m0 => odd m0
        end
      with odd (n0 : nat) : Prop :=
        match n0 with
        | 0 => False
        | S m0 => even m0
        end
      for
      odd) m
 end) 2

Problem

This is obviously the correct behaviour. Unfortunately, and apparently inexplicably, Coq wont apply Iota reduction in cases where a recursive function is either not applied to an argument or the argument is universally quantified. For example the following does not work:

Theorem even_n : forall n : nat, even n.forall n : nat, even n
  intro n.n: nat
even n
  lazy delta.n: nat
(with even (n : nat) : Prop :=
   match n with
   | 0 => True
   | S m => odd m
   end
 with odd (n : nat) : Prop :=
   match n with
   | 0 => False
   | S m => even m
   end
 for
 even) n
  lazy iota. (* FAILS TO REDUCE! *)n: nat
(with even (n : nat) : Prop :=
   match n with
   | 0 => True
   | S m => odd m
   end
 with odd (n : nat) : Prop :=
   match n with
   | 0 => False
   | S m => even m
   end
 for
 even) n

I do not see any reason why Iota reduction should depend on the surrounding context and have tried multiple variations to the above trying to get Coq to Iota reduce recursive functions. Unfortunately nothing worked.

How do I get Coq to apply Iota reduction to recursive functions that are either not applied to any arguments or that are applied to universally quantified arguments?

Answer

The problem here is that the iota rule is restricted for fixpoints: the Coq manual explicitly states that iota can only be applied to a fixpoint if the decreasing argument starts with a constructor.

This is done to ensure that the calculus of inductive constructions is strongly normalizing as a rewriting system: if we could always apply iota, then it would be possible to expand the recursive occurrences of the function being defined infinitely.

In practice, if you want to simplify such a fixpoint, there are two things you can do:

Destruct the recursive argument (n, in your case) manually and then reduce. This is simpler to do in some cases, but requires you to consider many cases.
Prove a simplification lemma and do a rewrite instead of a reduction. For instance, you could have proved a lemma of the form odd n <-> ~ even n, which might help you in some cases. You can also prove the unfolding explicitly as a lemma (this time, using your original definition of even):
```
Goal forall n, even n = match n with | O => True | S m => odd m end.forall n : nat,
even n = match n with
         | 0 => True
         | S m => odd m
         end
  now destruct n.
Qed.
```