existentielle Instanziierung und Verallgemeinerung in Coq

Question

Kann mir bitte jemand ein einfaches Beispiel für existentielle Instanziierung und existenzielle Generalisierung in Coq geben? Wenn ich exists x, P beweisen möchte, wo P ist einige Prop, die x verwendet, möchte ich oft x (wie x0 oder einige solcher) nennen, und manipulieren P. Kann dies eine in Coq sein?

Answer 1

Wenn Sie das Existential direkt und nicht durch ein Lemma beweisen möchten, können Sie eapply ex_intro verwenden. Dies führt eine existentielle Variable ein (geschrieben ?42). Sie können dann den Begriff manipulieren. Um den Beweis zu vervollständigen, müssen Sie eventuell einen Weg finden, einen Wert für diese Variable zu konstruieren. Sie können dies explizit mit der Taktik instantiate oder implizit durch Taktiken wie eauto tun.

Beachten Sie, dass es oft mühsam ist, mit existenziellen Variablen zu arbeiten. Viele Taktiken gehen davon aus, dass alle Begriffe instanziiert werden und möglicherweise Existenzen in Teilzielen verbergen. Sie werden nur herausfinden, wenn Qed Ihnen sagt "Fehler: Versuch, einen unvollständigen Beweis zu speichern". Sie sollten nur dann existentielle Variablen verwenden, wenn Sie einen Plan haben, sie in Kürze zu instanziieren.

Hier ist ein dummes Beispiel, das die Verwendung von eapply veranschaulicht.

Goal exists x, 1 + x = 3. 
Proof.      (* ⊢ exists x, 1 + x = 3 *) 
    eapply ex_intro.   (* ⊢ 1 + ?42 = 3 *) 
    simpl.      (* ⊢ S ?42 = 3 *) 
    apply f_equal.    (* ⊢ ?42 = 2 *) 
    reflexivity.    (* proof completed *) 
Qed.