Упрощение на месте для Coq

Question

Я хочу, чтобы эта цель:

f (S j') = f (j' + 1)

была автоматически подтверждена Coq. В настоящее время я должен написать:

apply f_equal. omega.

Но в целом это может быть сложнее, и мне, возможно, придется утверждать, например, что m-0 = m, а затем переписать. Есть ли способ переписать термин на месте, как у Изабель?

Answer 1

Я не уверен, что именно вы хотите. Возможно, вам может помочь replace tacti c.

В основном вы написали бы

replace (S j') with (j' + 1).
- (* f (j' + 1) = f (j' + 1) *)
  reflexivity.
- (* j' + 1 = S j' *)
  lia.

(Обратите внимание, что я использую lia, а не omega поскольку omega устарела в пользу lia.)

Вы можете даже выгрузить замену напрямую, lia:

replace (S j') with (j' + 1) by lia.
reflexivity.

Таким образом, замена будет успешной, только если lia способен решить необходимое равенство.

Answer 2

Coq имеет autorewrite tacti c, который похож на упрощители Изабель (хотя в целом у меня сложилось впечатление, что он не будет столь высокопроизводительным, и пользователи Coq склонны не полагаться на него так сильно). Ваш пример можно сделать так:

Require Import Arith.

Hint Rewrite Nat.add_1_r : myhints.

Theorem blah : forall (f: nat->nat) j',
    f (S j') = f (j' + 1).
Proof.
  intros.
  autorewrite with myhints.
  reflexivity.
Qed.