1

我试图了解组合的 ssreflect 策略应该如何“分解”（或者它们首先是如何组合的）。我遇到的问题之一是了解战术的顺序和关联性。

有时，我觉得顺序是从右到左。例如

apply : AiB.

似乎相当于

move : AiB; apply.

忽略 no-op move，就好像我们AiB在按顺序应用函数一样，apply : AiB.可以看作 apply (: AiB).. 也就是说，我们首先将 AiB 移动到目标中，然后apply在其中调用目标AiB。

但是，我在其他场合感到困惑：

case: (EM (P y)) => // notPy.

根据教程，这个对 进行案例分析(EM (P y))，然后//尝试解决琐碎的子目标。然后？？move =>将其余的引入上下文？这里的操作顺序是什么？

让，是EM_吗？我读对了吗，战术应用的“正确顺序”是什么？(EM (P y))(move=> notPy (// ( case (:EM_) ) ) )

顺序有点扭曲，一般来说notPy不一致。有没有办法在合法的 ssreflect 中从右到左写上面的内容？

4

1 回答 1

2

我建议您阅读手册以获取更多详细信息。https://hal.inria.fr/inria-00258384

在您的示例中，请回想一下，移动始终是无操作的，因此它“融合”了。因此，对于结肠，它在左侧融合。

move: H; case <=> case: H

并=>在右侧融合：

case: H; move => U <=> case: H => U.

因此，对于您的特定示例，

case: (EM (P y)) => // notPy.

可以看作

move: (EM (P y)); case; move=> // notPy.

问候！

于 2016-01-28T00:44:14.207 回答