Coq에서 선택적으로 재 작성하는 방법은 무엇입니까?

Question

a : nat 
fvs : list nat 
H : a = max (maxNum fvs) a + 1 
H1 : max (maxNum fvs) a >= a 

Doing rewrite H in H1.은 a을 모두 대체하는 반면, 나는 RHS에서만 a를 다시 쓰려고합니다. 할 수 있습니까? 나는 위의 두 가지 가설들로부터 거짓을 증명하고 싶다.

Answer 1

하나의 옵션과 같이 rewrite ... at <position>.을 사용하는 것입니다

rewrite H in H1 at 2. 

은 당신이 원하는 것은 또한 약간 다른 방법으로 수행 할 수 있습니다. 여기서 max (maxNum fvs) a은 부적절하다는 것을 관찰하십시오 - 그 표현식 대신 자연수를 사용할 수 있고 정리는 계속됩니다. 즉, generalize 전술을 사용할 수 있습니다.

Require Import Coq.Arith.Arith. 

Section foo. 

    Variable a : nat. 
    Variable fvs : list nat. 
    Variable maxNum : list nat -> nat. 
    Hypothesis H : a = max (maxNum fvs) a + 1. 
    Hypothesis H1 : max (maxNum fvs) a >= a. 

    Goal False. 
    revert H H1; generalize (max (maxNum fvs) a) as n. 
    intros n ->; rewrite Nat.add_1_r. 
    apply Nat.nle_succ_diag_l. 
    Qed. 

End foo.