I'm attempting the last exercise in section 'The Existential Quantifier' from Chapter 4 of "Theorem Proving in Lean 4" -- the equivalence:
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) := sorry.
Looks like I have the forward direction Ok. My problem is going the other way. I show below 3 different versions I tried as solution to the backward direction (the first version shows both directions). My main concern is to understand why these do not work; comments at the code spell out my difficulty.
Version 1:
theorem Er_rE_Equiv : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
Iff.intro
(λh1: (∃ x, r → p x) => -- This direction works
match h1 with
| ⟨z, rpz⟩ =>
λr1:r =>
have pz:(p z) := rpz r1
show (∃ z, p z) from ⟨z, pz⟩
)
(λk1: (r → ∃ x, p x) => -- This direction fails.
λr1:r => --<< Error flags here:
have pzE: (∃ x, p x) := k1 r1 -- "Expecting Type: '∃ x, r → p x'
match pzE with
| ⟨z, pz⟩ =>
show (∃ x, r → p x) from ⟨z, λr1 => pz⟩
)
The error msg above seems to make clear that Lean expects the proof to immediately start with construction of the expression to be proved. Specifically, I started w/ λr1 in order to extract the existential (∃ x, p x) via k1 r1. I conclude that Lean considers this 'detour' (i.e. starting w/ λr1) unacceptable (yet, for the forward direction, Lean did allow match as the start of proof, despite that this does not immediately begin construction of the implication r → to be proved, and amounts to a detour; why is match allowed, but λx => is not?). I conclude that Lean looks for the proof to begin directly w/ construction of the Existential. Hence my next attempt:
Version 2:
(λk1: (r → ∃ x, p x) =>
⟨z, λr1:r => --<< Error flagged: unknown identifier 'z'
have pzE:(∃ x, p x) := (k1 r1)
show (p z) from (pzE z)
⟩
)
The Exist.intro here (⟨z, etc...⟩) does not recognize the variable 'z'. Adding a label, as z1:z, does not help (Lean rejects the ':'). Nor does using the already-defined 'x' instead of 'z'. To remedy this, I tried doing a match on the existential -- as below:
Version 3:
theorem Er_rE_Bkwd2 : (r → ∃ x, p x) → (∃ x, r → p x) :=
(λk1: (r → ∃ x, p x) =>
⟨z, λr1:r => --this 'z' still gives err: 'undefined'
have pzE:(∃ x, p x) := (k1 r1)
match pzE with
| ⟨z, pz⟩ => --even as this one is considered 'defined',
show (p z) from (pzE z) --and is referenced by the 'z's in this line.
⟩
)
The 'match' seems to work -- in the sense that subsequent references to 'z' are not flagged as 'undefined'. But the first 'z' -- the one needed for the ∃.intro -- remains undefined. Of course, this is not surprising -- since the first 'z' appears before the match. Bottom line -- how does one introduce the variable for an ∃.intro, when no prior ref is available from the context? And why is a 'detour' allowed via match, but is not allowed for λx =>?
match doesn't really care about which type is expected, whatever type is after the => is the type the match ends up being. This is because match isn't meant to construct anything but destruct something like an exists.
However, λ x => _ is specifically about constructing terms of type a → b or ∀ a, p a, similar to how Exists.intro is for constructing terms of type ∃ a, p a. In your example, the expected type is ∃ x, (r → p x) but you try to use λ x => _ which is for a → b or ∀ a, p a, so really you need Exists.intro (or ⟨a, b⟩) but obviously we don't have the value we need to put in here. Right above the exercises it gives a useful hint though:
We also leave it to you to determine which are nonconstructive, and hence require some form of classical reasoning.
In this case, constructive reasoning is not enough and we need classical logic, e.g. byContradiction or byCases. This gives us enough to work with to solve the goal:
example {r : Prop} {p : α → Prop} (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
Iff.intro
...
(fun h : r → ∃ x, p x =>
byCases
(fun hr : r =>
have h' : ∃ x, p x := h hr
match h' with
| ⟨b, hb⟩ => ⟨b, fun _ : r => hb⟩)
(fun hr : ¬r => ⟨a, fun hr' : r => absurd hr' hr⟩))
If r is true, we can simply use the h to get a b and use that to solve the goal.
If r is false, we can use any a (e.g. the one given to us) and we solve the goal using the two contradictory hypotheses hr : ¬r and hr' : r.