存在實例化和coq中的泛化

有人能給我一個簡單的存在實例化和存在性泛化的例子嗎？當我想證明exists x, P，其中P是一些Prop，它使用x，我經常想要命名x（如x0或某些這樣的），並操縱體育這可能是一個在Coq？存在實例化和coq中的泛化

來源

2012-05-21 Mayer Goldberg

我知道過去有這樣的coq問題，但我懷疑隨着更多網站的推出，coq問題的最佳位置現在是http://cs.stackexchange.com/（不太滿意我自己的分裂，但它是生活的一個事實...） –

@andrewcooke [這還沒有得到確鑿的證實。]（http://meta.cs.stackexchange.com/questions/52/scope-limits-on-證明助手 - 例如coq）我的感覺是，如果目標是要完成一個證明，Coq問題更關注於SO，如果目標是理解證明技術爲什麼工作，[cs.se]或不工作，但它是一條很細的線。專業知識遍佈於[so]，[cs.se]和[cstheory.se]。 – Gilles

如果你打算直接證明存在，而不是通過引理，你可以使用eapply ex_intro。這引入了一個存在變量（編寫?42）。然後你可以操縱這個詞。爲了完成證明，您需要最終提供一種方法來構建該變量的值。您可以使用instantiate策略明確執行此操作，也可以隱式執行諸如eauto之類的策略。

請注意，使用存在變量通常很麻煩。許多策略都假定所有術語都被實例化並可能隱藏存在於子目標中的存在;你只會在Qed告訴你「Error：嘗試保存一個不完整的證明」時纔會發現。當你計劃很快例化它們時，你只應該使用存在變量。

下面是一個愚蠢的例子，說明使用eapply。

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.

來源

2012-05-21 22:46:14 Gilles

憑藉Coq後備箱，您可以在證明結束時將未經證實的存在變爲子目標 - 這是我長期以來的願望。 –

除[以前的評論]（https://stackoverflow.com/questions/10686164/existential-instantiation-and-generalization-in-coq#comment13933112_10693631）：這可以用[抓取存在變量。]來完成。（https://coq.inria.fr/refman/Reference-Manual009.html#GrabEvars） –

存在實例化和coq中的泛化

回答

相關問題