Stream: Beginner Questions

Topic: Proof obligation generated by obtain

Gergely Buday (Apr 25 2025 at 10:27):

My proof starts with

lemma example_obtain_elementary:
  assumes "∃x. P x ∧ Q x"
  shows "∃x. Q x"
proof -
  obtain a where "P a ∧ Q a" using assms by (rule exE)

here the obtain-where clause generates this proof obligation:

proof (prove)
goal (1 subgoal):
 1. (⋀a. P a ∧ Q a ⟹ thesis) ⟹ thesis

I do understand why using assms by (rule exE) proves this, but not why exactly this is the proof obligation. Shouldn't it be simply

∃x. P x ∧ Q x

as this is required for such an a to exist.

Mathias Fleury (Apr 25 2025 at 10:45):

obtain is on pure level, so there is no ∃

Mathias Fleury (Apr 25 2025 at 10:46):

but it boils down to the same: you want to use ⋀a. P a ∧ Q a ⟹ thesis to prove thesis

Mathias Fleury (Apr 25 2025 at 10:46):

and to prove that you need to show that such an a exists

Last updated: May 09 2025 at 12:41 UTC