爲什麼後面的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重寫不適用於假設的右側？

回答

相關問題