Search code examples
coqcoq-tactic

Reduction in coq when the simpl or cbn tactics are not effective

I am trying to prove this:

Fixpoint max(a: nat)(b:nat): nat :=
if a <=? b then b
else a.
Example ex: forall n:nat, n = max n n.
Proof.
intros.
(...)

The simpl and cbn tactics do not produce anything. If I call cbv [max], then I get a redex and I don't know how to continue the proof after that. More precisely, I get:

n = (fix max (a b : nat) {struct a} : nat := if a <=? b then b else a) n n

How to get rid of this redex (fix max ....) n n ?

Solution

  • There is a Fixpoint even though the function is not recursive, and that is where fix comes from. Use Definition instead.

    A fix only reduces when the structurally decreasing argument (here n, the first one) starts with a constructor. So if your function were really meant to be recursive, you could use destruct n..