に平等の証明で部分式を置き換えます。私は、このプロパティを証明しようとしていますイドリスで練習としてイドリス
plusDouble : (a:Nat) -> (a + a) = a*2
plusDouble a =
rewrite multCommutative a 2 in
rewrite plusZeroRightNeutral a in Refl
は、だから私は、私は信じているbasicall:
lemma1 : {x:Nat} -> {y:Nat} -> {z:Nat} -> (x + x) + (x * z) = (y + y) + (y * z) -> (x * (S (S z))) = (y * (S (S z)))
lemma1 {x=x} {y=y} {z=z} prf = ?todo
もちろん、私はすでに証明されていることy (x + x)
を(x*2)
に置き換えて、lemma1
を証明するためにdistributivityを呼び出してください。私はこの交換方法を知らない。 は、私は単に
rewrite plusDouble x in ...
ような何かをしかし、私は交換したい部分式がprf
で、ゴールでであるため、明らかに動作しないことを考えていました。
一般的なアプローチはありますか?この特別なケースでお勧めするものは何ですか?
「展開する」という意味を説明してもらえますか?私も同様の問題があるので、より詳細な答えに興味があります。 – Markus
私は、書き換えルールとして使用される等価の左辺がある意味では「より複雑」であることを意味します。たとえば、someProofMatchingRight'で 'plusZeroRightNeutralを書き直すことができます(これは私が目標の簡素化と呼んでいます)ですが、someProofMatchingZeroPlusRight'でsym $ plusZeroRightNeutralを書き直すこともできます(これは私が目標の拡張と呼ぶものです)。おそらくもっと正確な用語があるかもしれません。 – user1747134