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を書き直したいだけです。それはできますか？私は上記の2つの仮説から虚偽を証明したい。

Answer 1

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.