Proving properties of an existential witness

Stream: new members

[Mark Fischer]

Is it possible to prove properties of an existential witness? This is a silly example, but say:

def foo (a b : ℕ) : Prop := ∃c, a + b = c

Is there a way to express that foo a b → a ≤ c where c is the witness to the truth of foo a b?

[Mark Fischer]

By inspecting this proof, you can see that it is possible to use the witness from the antecedent as a witness to the consequent

example (a b : ℕ): foo a b → ∃c, a ≤ c :=
  have hle := λ{c : ℕ}(h : a + b = c) ↦ le_iff_exists_add.mpr ⟨b, h.symm⟩
  λ⟨c, h⟩ ↦ ⟨c, hle h⟩

but of course, you don't need to. You can ignore the antecedent altogether:

example (a b : ℕ): foo a b → ∃c, a ≤ c :=
  λ_ ↦ ⟨a, Nat.le.refl⟩

[Matt Diamond]

Is there a way to express that foo a b → a ≤ c where c is the witness to the truth of foo a b?

sure: foo a b → a ≤ (foo a b).choose

[Mark Fischer]

That makes sense to me! Though foo is a proposition, not a proof, that's easy to fix

[Mark Fischer]

Been trying to prove this, but I'm not sure how to work it:

import Mathlib

def foo (a b : ℕ) : Prop := ∃c, a + b = c

example (a b : ℕ) : (h : foo a b) → a ≤ h.choose := by
  intro h₁
  match h₂ : h₁ with
  | ⟨x ,h₃⟩ =>
    have h₄ : h₁.choose = a + b := sorry
    simp only [h₄]
    exact Nat.le_add_right a b

[Paul Rowe]

I think what you need is h₁.choose_spec which tells you the property that is satisfied by h₁.choose

[Paul Rowe]

So, since your equality is the reverse order of the property, you can replace your sorry with h₁.choose_spec.symm to make Lean happy

[Mark Fischer]

Yup, that works :)

example (a b : ℕ) : (h : foo a b) → a ≤ h.choose := by
  intro h₁
  have h₂ : h₁.choose = a + b := h₁.choose_spec.symm
  simp only [h₂]
  exact Nat.le_add_right a b

Though, I have a followup question. It feels like intro returns both the value and the property, but it doesn't give me a way to connect it back to the output.

example (a b : ℕ) : (h : foo a b) → a ≤ h.choose := by
  intro ⟨x, heq⟩
  sorry

Here's it feels like x = h.choose should be true, but I don't really have access to this fact?

[Mark Fischer]

Ah, right, nevermind, I do get access to that fact using the match statement. Looks good.

[Eric Wieser]

Here's it feels like x = h.choose should be true, but I don't really have access to this fact?

In general it's unprovable, you can only prove it here because there is only one possible witness

[Matt Diamond]

good point... a proof about h.choose is going to be pointless in contexts where you've destructured the existential

in those contexts, all you need is a lemma of the form ∀ {x}, p x → q x... the fact that x is an existential witness is irrelevant

[Mark Fischer]

I would expect something like this to work.

let t₁ := foo.choose
let t₂ := foo.choose
have h : t₁ = t₂ := rfl

This isn't how it works, but I have a lingering intuition that when I destructure, I should somehow have access to how that value connects back to the value it was destructured from...

let ⟨t₁, _⟩ := foo
let t₂ := foo.choose
have h : t₁ = t₂ := rfl

but that doesn't work. That or I'm off base on what the destructuring even does here, I think it uses choice underneath as well.

[Eric Wieser]

Maybe it helps to realize that (Exists.intro x hx).choose = x is usually unprovable

[Eric Wieser]

(destructuring has some extra complications that are a distraction here; you need a different syntax to destruct things without forgetting what they are)

[Mark Fischer]

I think that makes sense. Choice doesn't give me back any particular element (for example, the witness I just used).

What I'm thinking is generally closer to (Exists.intro x hx).choose = (Exists.intro x hx).choose though sometimes lean doesn't see it that way right away. Esp, when destructuring since that information is lost.

But this has been a helpful exercise in wrapping my head around what's happening.

[Paul Rowe]

Treq said:

This isn't how it works, but I have a lingering intuition that when I destructure, I should somehow have access to how that value connects back to the value it was destructured from...

I wonder if you are looking for something like

set t₁ := h₁.choose with g₁

This adds two hypotheses: t₁ : ℕ := Exists.choose h₁ and g₁ : t₁ = Exists.choose h₁ Then you can use rw to substitute back and forth with t₁ and Exists.choose h₁ as necessary.

In other words, let is great if you just need to define a value of a certain type and it doesn't matter how you got it. set ... with is useful if you need to retain the defining equation of what you are declaring.

Please feel free to ignore if I have completely missed the mark.