Given the following Lean code snippet:
example : ( ∃ x : A, PP x) → ( ∀ y : A, PP y → QQ y) → ∃ z : A , QQ z :=
begin

assume p pq,
cases p with a pa,
existsi a,
apply pq,
exact pa,
end
Which of the following best describes the role of cases p with a pa in this proof?

Question

Given the following Lean code snippet:  
 example : ( ∃  x : A, PP x)  →  ( ∀  y : A, PP y  →  QQ y)  →   ∃  z : A , QQ z := 
 begin 
  
        assume p pq,  
        cases p with a pa,  
        existsi a,  
        apply pq,  
        exact pa,  
 end 
 Which of the following best describes the role of  cases p with a pa  in this proof?

Accepted Answer

It decomposes the assumption  p  of  ∃  x : A, PP x  into an element  a : A  and an assumption  pa : PP a , making  a  and  pa  available for use in the proof.

Answer

It applies the assumption  pq  to the goal.

Answer

It introduces a specific element  a  of  type A  and an assumption  pa : PP a , effectively proving the existential quantifier.

Answer

It constructs a term of type  ∃  z : A, QQ z  using  p  directly.

Crowdly

Given the following Lean code snippet: example : ( ∃ x : A, PP x) → ( ∀...

Want instant access to all verified answers on moodle.nottingham.ac.uk?