2017-12-31 16 views
0

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がすべきであるか分からない。

答えて

0

ああ、それは振り返ってかなり明らかです。私たちは聞かせている場合:

P = \x => S x = S (plus k 0) 

をその後、我々は、(反射性によって)x = (plus k 0)のためにそれを証明することができます。今、y = kreplaceとすると、私たちに必要なのはS k = S (plus k 0)という証明が得られます。つまり、

plusCommZ : (m : Nat) -> m = plus m 0 
plusCommZ Z = Refl 
plusCommZ (S k) = replace 
    {P = \x => S x = S (plus k 0)} 
    {x = plus k 0} 
    {y = k} 
    (sym (plusCommZ k)) 
    Refl 

証明書を完成させます。それ以外の方法でP = \x => S x = S kとすることができます。

+0

ここで、置き換えが正当化される方法は、私にとって謎です(はい、定義を見ました)。 – MaiaVictor

+1

'sym'は実際には必要ありません:' replace {P = \ x => S k = S x}(plusCommZ k)Refl'(これは本質的に 'cong(plusCommZ k)'です) –

関連する問題