The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

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