coq：在陈述中替换真实假设的策略'and'

Question

Assumptions:
l: a < d
Goal: (s a / a < d) <-> s a

这里，我有一个带有假定语句的/。进球只需要我来配合，但我似乎搞不懂战术。应用、重写和替换都不起作用。

Answer 1

rewrite只有在a < d是等式或等价关系的表示法的情况下才有效，但这里我认为情况并非如此。

tauto和easy会自动解决你的目标，但我认为你要求的是一些不那么自动的东西。

这有点令人失望，但我能想出的最好的非自动证据是分割你的目标：

Goal forall a d s, a < d -> (s a / a < d) <-> s a.
Proof.
intros a d s l.
split.
- intros [sa _].
exact sa.
- intros sa.
split.
+ exact sa.
+ exact l.
Qed.

如果你有兴趣使用rewrite来做这类事情，MathComp库会以使rewrite成为最有用的策略的方式来定义事情，尤其是它可以在你的目标的翻译版本中工作。但可能最好的短期解决方案是利用一些自动化策略。

Answer 2

使用SSReflect/mathcomp，正如@ana borges所提到的，确实可以rewrite假设l(这就是->所做的(；这之后可以是split，其中true在连词中。

From mathcomp Require Import all_ssreflect.
Goal forall a d s, a < d -> (s a / a < d) <-> s a.
Proof. move=> a d s ->; split=> [[sa _] //|sa]; exact: conj. Qed.

不过，也许还有另一个较短的版本。

Answer 3

我想明白了——你只需要运行propositional，它就会自动评估这种同义反复逻辑。