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 (m : nat) : nat :=
           match m with
           | 0 => 1
           | S m0 => m * fact m0
           end) m
    end) 2.

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.
1 subgoal
==========
even 2
> lazy delta.

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) 2
> lazy iota.

1 subgoal
==========
(fun n:nat =>
  match n with
    | O => True
    | S m => (fix even (o:nat):Prop := match o with ... end
              with odd (o:nat):Prop := match o with ... 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.
1 subgoal
==========
forall n:nat, even n
> intro n.

1 subgoal
n : nat
==========
even n
> lazy delta.

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) n
> lazy iota. (* FAILS TO REDUCE! *)

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... 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?

Any help will be appreciated. Thanks, - Larry

Answer 1

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:

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

2. 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 => False | S m => odd m end.
   now destruct n.
   Qed.