The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

to workaround this (justified) limitation of reduction, we usually use rewriting. First prove the recusive equation of the function.

Lemma rec_eq : forall y,

    ((fix f (x : nat) := if eq_nat_dec x 0 then true else false) y)

    = (fun (x : nat) => if eq_nat_dec x 0 then true else false) y.

Proof.

  intros y.

  destruct y;simpl;auto.

Qed.

And then use "rewrite rec_eq." in your scripts. For the same reasons as for reduction.

Best regards,

Pierre

Le Mon Jan 05 2015 at 1:05:02 PM, Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr> a écrit :

> On 31 Dec 2014, at 22:08, Larry Lee <llee454 AT gmail.com> wrote:
>
> Is it possible to simplify fixed point expressions over non-constant arguments?
euhhh nope. Your enemy is called strong reduction
>
>     Eval lazy iota in ((fix f (x : nat) := if eq_nat_dec x 0 then true else false) y).
>
> should evaluate to
>
>     (fun (x : nat) => if eq_nat_dec x 0 then true else false) y
>
> but does not simplify at all.
>
> Is there something that I'm missing?
Indeed, you miss the fact that you’re discussing over a very special kind of fixpoints: the one that always reach a normal form in 1 unfolding !

Because Coq is doing strong reduction, I’m glad that it unfold fixpoints only if the recursive argument starts by a constructor. I would be annoyed that
(fix pl x := match x with | 0 => y | S m => S (pl m) end) n unfolds to
(fun x := match x with | 0 => y | S m => S ((fix pl x := match x with | 0 => y | S m => S (pl m) end) m) end) n that unfolds to
(fun x := match x with | 0 => y | S m => S ((fun x := match x with | 0 => y | S m => S ((fix pl x := match x with | 0 => y | S m => S (pl m) end) m) end) m) end) n that unfolds to
… you’ve understood my point :-)

>
> Thanks,
> Larry
All the best,
Pierre B.