У меня есть следующая теорема в Coq: Theorem T : exists x:A, P x. Я хочу иметь возможность использовать это значение в последующем доказательстве. I.E. Я хочу сказать что-то вроде: «пусть o представляет такое значение, что P o. Я знаю, что o существует по теореме _5 _...»
Как мне это сделать? Заранее спасибо!
С математической точки зрения, вам нужно применить правило исключения для конструктора ∃. Общая тактика исключения elim работает.
elim T; intro o.
Глупый пример:
Parameter A : Prop.
Parameter P : A -> Prop.
Axiom T : exists x:A, P x.
Parameter G : Prop.
Axiom U : forall x:A, P x -> G.
Goal G.
Proof.
elim T; intro o.
apply U.
Qed.
