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?egzystencja i uogólnienie egzystencjalne w coq
Odpowiedz
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.
W bagażniku Coq możesz zamienić niepotrzebne egzystencjalnie w podpunkty na końcu dowodu - czego pragnę od dawna. –
Dodatek do [poprzedniego komentarza] (https://stackoverflow.com/questions/10686164/existential-instantiation-and-generalization-in-coq#comment13933112_10693631): można to zrobić za pomocą [Grab Existential Variables.] (https://coq.inria.fr/refman/Reference-Manual009.html#GrabEvars) –
wiem doszło Coq pytania tu w przeszłości, ale podejrzewam, że więcej stron są wprowadzane najlepsze miejsce na pytania Coq jest teraz http://cs.stackexchange.com/ (nie tak zadowolony z sama fragmentacja, ale to fakt życia ...) –
@andrewcooke [To nie zostało ustalone jednoznacznie.] (http://meta.cs.stackexchange.com/questions/52/scope-limits-on- asystenci-eg-coq) Mam przeczucie, że pytania Coq są bardziej na temat tematu, jeśli celem jest uzyskanie dowodu, i na [cs.se] jeśli celem jest zrozumienie, dlaczego technika sprawdzająca działa albo nie działa, ale jest to bardzo cienka linia. Ekspertyza jest rozłożona na [so], [cs.se] i [cstheory.se]. – Gilles