Сокращение coq, когда тактика simple или cbn не эффективна

Question

Я пытаюсь доказать это:

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

Тактика упрощенная и cbn ничего не дает.Если я позвоню cbv [max], то получу переопределение и не знаю, как продолжить доказательство после этого.Точнее я получаю:

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

Как избавиться от этого переопределения (fix max ....) n n?

Answer 1

Существует Fixpoint, хотя функция не является рекурсивной, и именно отсюда fix. Вместо этого используйте Definition.

A fix уменьшается только тогда, когда структурно убывающий аргумент (здесь n, первый) начинается с конструктора. Так что, если ваша функция действительно предназначена для рекурсии, вы можете использовать destruct n..