Coq的就地简化

Question

我想要这个目标：

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

由Coq自动证明。目前我必须写：

apply f_equal. omega.

但是总的来说，这可能会更加困难，例如，我可能需要断言m-0 = m，然后重写。是否可以像Isabelle一样就地重写术语？

Answer 1

我不确定您到底想要什么。也许replace策略可以为您提供帮助。

基本上你会写

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能够解决所需的相等性的情况下，替换才能成功。