thisのドキュメントには、replace
を使用して証明を完成させる方法が記載されていますが、rewrite
が使用されています。これはreplace
という文章砂糖のようです。私はそれを明示的に使用する方法を理解することに興味があります。`replace`を使ってこの可換性の証拠を完成させるには?
私が正しく理解していれば、反射性によって証明可能となり、k = plus k 0
という証拠与えられ、S (plus k 0) = S (plus k 0)
としてS k = S (plus k 0)
を書き換えるために使用することができます。しかし、それをreplace {P = \x => S x = S (plus k 0)} {x = k} {y = plus k 0} rec
としてインスタンス化する場合は、今度は証明する必要があると証明したS k = S (plus k 0)
が必要になります。要するに、私は正確にP
がすべきであるか分からない。
ここで、置き換えが正当化される方法は、私にとって謎です(はい、定義を見ました)。 – MaiaVictor
'sym'は実際には必要ありません:' replace {P = \ x => S k = S x}(plusCommZ k)Refl'(これは本質的に 'cong(plusCommZ k)'です) –