为什么后面的Coq重写不适用于假设的右侧？

我有以下Coq env。为什么后面的Coq重写不适用于假设的右侧？

1 subgoals 
m : nat 
IHm : forall n : nat, n + n = m + m -> n = m 
n : nat 
H : S (n + S n) = S (m + S m) 
ll := ll : forall k : nat, k + S k = S k + k

做rewrite ll in H，只改变了LHS S (n + S n)到S (S n + n)但不是RHS S (m + S m)。 ll应该适用于nat类型的所有变量。这里有什么问题？

来源

2017-09-02 abhishek

'重写H'只会使用'H'的一个实例，您需要使用'！'量词来强制更多的重写。例如：引理ex n m：n = m - > n + 0 = m + 0。现在重写< - ！plus_n_O。 Qed.' – ejgallego

@ejgallego，你应该发布这个答案！ –

我没有时间正确写出答案，对不起。我的评论缺少一些东西，其中包括对“重写”如何选择实例化模式的解释。 – ejgallego

扩展在埃米利奥的评论，rewrite H和rewrite H in H'会首先找到所有（依赖）的实例变量量化的H，然后全部替换*与RHS该实例LHS的。我相信它会在语法树中找到最顶层/最左边的实例。因此，举例来说，如果你这样做：

Goal forall a b, (forall x, x + 0 = x) -> (a + 0) * (a + 0) * (b + 0) = a * a * b. 
    intros a b H. 
    rewrite H.

的rewrite H会选择实例x与a，并将得到的目标将是a * a * (b + 0) = a * a * b。你可以用!（如rewrite !H）的前缀来表示“随处重写，选择尽可能多的实例化”，或者用?（如rewrite ?H）表示try rewrite !H，即可以选择多个实例，也可以选择如果找不到，就不会失败。

*实际上有更多的细微差别，这是更换是在一次通过与rewrite H和多次通过与rewrite ?H和rewrite !H完成。这只有在第一次更换时才会显示先前不可用的其他更换位置。例如，如果您在目标(a + 0) + 0 = a中用a + 0 = a重写; rewrite H离开球门a + 0 = 0。

来源

2017-09-11 15:48:58

为什么后面的Coq重写不适用于假设的右侧？

回答

相关问题