Wie kann ich selektiv in Coq umschreiben?

Question

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

rewrite H in H1. tun, ersetzt sowohl die a s, während ich nur die eine auf der RHS umschreiben wollen. Kann es gemacht werden? Ich möchte mich aus den beiden obigen Hypothesen als falsch herausstellen.

Answer 1

Eine Option ist rewrite ... at <position>. wie so zu verwenden:

rewrite H in H1 at 2. 

Was Sie wollen, auch auf eine etwas andere Art und Weise durchgeführt werden kann. Beachten Sie, dass hier irrelevant ist - Sie können anstelle dieses Ausdrucks jede natürliche Zahl verwenden und Ihr Satz würde immer noch gelten. Das bedeutet, dass Sie die generalize Taktik verwenden können.

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.