egzystencja i uogólnienie egzystencjalne w coq

Question

Czy ktoś mógłby podać mi prosty przykład egzystencjalnego tworzenia i generalizacji egzystencjalnej w Coq? Kiedy chcę udowodnić, że exists x, P, gdzie P jest jakiś , który używa x, często chcę nazwać x (jako x0 lub niektóre takie) i manipulować P. Czy to może być jeden w Coq?

Answer 1

Jeśli zamierzasz udowodnić egzystencjalną bezpośrednio, a nie przez lemat, możesz użyć eapply ex_intro. Wprowadza to zmienną egzystencjalną (napisaną ?42). Następnie możesz manipulować tym terminem. Aby uzupełnić dowód, musisz w końcu zapewnić sposób na skonstruowanie wartości dla tej zmiennej. Możesz to zrobić jawnie za pomocą taktyki instantiate lub domyślnie poprzez taktyki, takie jak eauto.

Należy pamiętać, że często praca z zmiennymi egzystencjalnymi jest uciążliwa. Wiele taktyk zakłada, że ​​wszystkie terminy są tworzone i mogą ukrywać egzystencje w subgałach; dowiesz się tylko, kiedy Qed powie Ci "Błąd: próba zapisania niepełnego dowodu". Powinieneś używać zmiennych egzystencjalnych tylko wtedy, gdy masz plan ich utworzenia.

Oto głupi przykład, który ilustruje użycie 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.