나는이 속성을 증명하기 위해 노력하고 이드리스의 연습으로 이드리스

Question

평등 증거에 표현식을 바꾸기 :

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을 증명하기 위해 배포 가능성을 호출하면됩니다. 나는이 대체 방법을 모른다. 나는 단순히

rewrite plusDouble x in ... 

처럼 뭔가를 할 수하지만 교체 할 표현식이 목표에 prf과에 있기 때문에 그것은 분명히 작동하지 않습니다 생각했다.

일반적인 접근 방법이 있습니까? 또는이 특별한 경우에 권장할만한 것이 있습니까?

Answer 1

좋아, 그래서 내가 항상 목표를 재 작성 규칙을 사용하여 단순화 할 필요가 없다는 것을 알았지 만, 나는 인수로서 얻는 증거와 일치하도록 그것을 확장 할 수있다.

Answer 2

재 작성 기능은 후드 아래에서 replace : (x = y) -> P x -> P y을 사용합니다. P이 (내가 이해하는 한) 무엇인지 파악하고 있습니다.

x + x을 x*2으로 대체하려면 x + x = x*2을 그대로 사용할 수 있습니다. x*2을 x + x으로 대체하려면 x*2 = x + x 동등성을 사용할 수 있습니다. 귀하의 경우에는 sym prf입니다. 두 가지를 모두 수행하려면 두 가지 교체가 필요합니다.

재 작성 도구 (또는 추론)에서 알아낼 수없는 경우 replace {P = \x' => x' + (x * z) = (y + y) + (y * z)} (plusDouble x) prf과 같이 명시 적으로 P을 제공 할 수 있습니다. 이는 특히 x + x의 일부 사이트를 다시 작성해야하지만 전체 사이트가 아닌 경우에 특히 유용합니다.