Confusion about matching on exists

Stream: lean4

[Anna Williams]

Sometimes I can match on exists and sometimes I cannot, resulting in an error "Case tag 'rhs' not found.", I'm a bit confused as to how and when this occurs.

image.png

Is there some way I can get the witness of the exists in this instance?

[Kenny Lau]

i don't know what the error means because you didn't provide an #mwe , but you can't eliminate from Prop into data, so there is no way to get the witness computably from an exists

[Aaron Liu]

that's weird

[Kenny Lau]

there are ways around this, but i'm refraining from saying them, because usually it means you're in the wrong situation and "eliminating prop into data" is not the right step to take in this instance

[Aaron Liu]

consider using docs#Exists.choose instead

[Kenny Lau]

that's the workaround i was deliberately omitting

[Aaron Liu]

your theorem lubUnique probably does not mean what you think it does

[Aaron Liu]

Lean has proof irrelevance so any two proofs of the same thing are automatically equal

[Kenny Lau]

oh yeah, that too

[Anna Williams]

When you say "proof irrelevance" do you mean that the entire thing is forgotten or that just the proof corresponding to one witness is forgotten? I think this is where I'm getting confused

[Anna Williams]

I've tried using Σ'which I know keeps the data, but then I run into problems with certain structures being Types instead of Props

[Kenny Lau]

the problem is that you're trying to translate some natural language directly into symbol without considering the logic behind

[Anna Williams]

I don't think that's very helpful?

[Aaron Liu]

Anna Williams said:

When you say "proof irrelevance" do you mean that the entire thing is forgotten or that just the proof corresponding to one witness is forgotten? I think this is where I'm getting confused

Proof irrelevance means that any two proofs of the same theorem are always considered equal

[Aaron Liu]

so for example, any two proofs of ∃ a : D, LeastUpperBound p a S will be definitionally equal

[Kenny Lau]

Anna Williams said:

I don't think that's very helpful?

To someone who has had little contact with formal logic, they might think about "there exists x such that p(x)" vaguely, and to them this might be already equivalent to having that x already, but when you're doing formal logic (especially in a verification system such as Lean), the expression "there exists x such that p(x)" is a proposition (i.e. a true/false statement), while the witness x itself "contains data" (i.e. is an object of some set), and it cannot be compared to a proposition

[Siddhartha Gadgil]

To clarify, a longish example. Here we have an existence theorem but cannot resolve without proving a non-trivial theorem:

Noncomputable exists proof

A Noncomputable function

An interesting example of a non-constructive proof is the following:
Theorem: There exist irrational numbers $a$ and $b$ such that $a^b$ is rational.
Proof: Let b = √2. If b^b is rational, then we can take a = b. Otherwise, we can take a = √2^{√2}, so a^b=2.

We can prove this in Lean. But a function that returns such a pair of numbers has to be defined as noncomputable in Lean.

noncomputable abbrev sqrt2 : ℝ := Real.sqrt 2

theorem sq_sq_sq_sqrt2_rational : (sqrt2^sqrt2)^sqrt2 = 2 := by
  rw [← Real.rpow_mul, Real.mul_self_sqrt] <;> simp

example : (sqrt2^sqrt2)^sqrt2 = 2 := by
   rw [← Real.rpow_mul, Real.mul_self_sqrt] <;> simp

/--
There exists an irrational numbers `a` and `b` such that `a^b` is rational.
-/
theorem irrational_power_irrational_rational : ∃ (a b : ℝ), Irrational (a) ∧ Irrational b ∧
    ¬ Irrational (a^b)  := by
  by_cases h : Irrational (sqrt2^sqrt2)
  case pos =>
    use sqrt2 ^ sqrt2, sqrt2
    simp [h, sq_sq_sq_sqrt2_rational, irrational_sqrt_two]
  case neg =>
    use sqrt2, sqrt2
    simp [irrational_sqrt_two]
    assumption

[Wrenna Robson]

You could use Subtype.

[Wrenna Robson]

That is often a good way to hold "this is a term, that satisfies a given predicate"

[Wrenna Robson]

to say that there exists some x with p x is to say that there exists a term of type Subtype p

[Aaron Liu]

often a better way is to construct the term first and only afterwards prove it satisfies the predicate in a separate theorem

[Aaron Liu]

this doesn't always work for recursive definitions