How can I say "there exist unique a, b such that..."?

Stream: new members

[Adam Dingle]

I'd like to translate this statement into Lean: "There is a unique pair of natural numbers (a, b) such that a * b = 1."

I can write

  example: ∃! (p : Nat × Nat), p.1 * p.2 = 1 := ...

But p.1 and p.2 are a bit ugly. Really I'd like to write

  example: ∃! ((a, b) : Nat × Nat), a * b = 1 := ...

but Lean won't accept this syntax. Is there any way to write this nicely?

[Ruben Van de Velde]

This could work: example: ∃! (a : Nat) (b : Nat), a * b = 1 := ...

[Adam Dingle]

I believe that Lean interprets that as meaning ∃! (a : Nat), ∃! (b : Nat), a * b = 1, which is not semantically the same.

[Josha Dekker]

So perhaps take (a, b) to be an element of Nat x Nat?

[Adam Dingle]

I realized that this works:

example: ∃!(p : Nat × Nat), let (x, y) := p;
  x * y = 1 := ...

This isn't too bad. I'd still be happy to know about a nicer syntax if it exists.

[Adam Dingle]

Josha: I don't understand your comment. Are you suggesting a particular syntax that will work?

[Ruben Van de Velde]

They are provably the same though, no?

[Josha Dekker]

Adam Dingle said:

I realized that this works:

example: ∃!(p : Nat × Nat), let (x, y) := p;
  x * y = 1 := ...

This isn't too bad. I'd still be happy to know about a nicer syntax if it exists.

This is basically what I was suggesting indeed: you want to say that there is a unique pair of integers, so you consider the set of all pairs of integers, i.e. Nat x Nat

[Josha Dekker]

I think there’s a way of doing the ‘let’ part immediately, but I’m not sure about that.

[Edward van de Meent]

i believe you can do ((x,y): Nat \x Nat)

[Adam Dingle]

Lean won't accept that syntax. If I write

example: ∃! ((x, y) : Nat × Nat), x * y = 1 := sorry

Lean reports

unexpected token '('; expected '_' or identifier

at the left parenthesis in (x, y).

[Edward van de Meent]

oh...

[Edward van de Meent]

in that case, maybe just \exists! (x y : Nat),...?

[Johan Commelin]

Note that \exists! x, \exists! y, foo(x, y) does not mean the same thing as \exists! (x, y), foo(x, y).

[Edward van de Meent]

ah right... and i'm guessing that what i suggested expands to the first?

[Eric Wieser]

example : ExistsUnique fun (a, b) => a * b = 1 := _ works, but not with notation

[Dan Velleman]

You could also say: ∃ (a b : Nat), a * b = 1 ∧ ∀ (a' b' : Nat), a' * b' = 1 → a' = a ∧ b' = b.

[Kevin Buzzard]

They are provably the same though, no?

@Adam Dingle @Ruben Van de Velde they are provably different! This is a fabulous gotcha. Saying "there's a unique a such that there's a unique b which works" allows the possibility that there's an a for which only one b works, but for all the other a's, more than one b works (as opposed to no b working)

import Mathlib.Tactic

example : ∃ (P : ℕ → ℕ → Prop),
    ¬ ((∃! (a : ℕ) (b : ℕ), P a b) ↔ (∃! ab : ℕ × ℕ, P ab.1 ab.2)) := by
  use fun a b => (a = 0) → (b = 0)
  rintro ⟨h1, -⟩ -- left->right is the problem
  specialize h1 ⟨0, ⟨0, id, by aesop⟩, fun c ⟨d, hd1, hd2⟩ => ?_⟩
  · specialize hd2 (d+1)
    aesop
  · rcases h1 with ⟨⟨a, b⟩, -, hab⟩
    specialize hab (a+1, b+1)
    aesop

[Kyle Miller]

Here are some concrete examples:

example : ∃! (y x : Int), y = x^2 := by
  use 0
  constructor
  · use 0
    simp
    intro _ h
    exact pow_eq_zero h.symm
  · simp
    rintro y ⟨x, h⟩
    simp at h
    cases h.1
    simp at h
    specialize h (-x)
    simpa using h

example : ¬ ∃! (x y : Int), y = x^2 := by
  rintro ⟨x, h⟩
  simp at h
  specialize h (x + 1)
  simp at h

example : ¬ ∃! p : Int × Int, p.1 = p.2^2 := by
  rintro ⟨⟨y, x⟩, h⟩
  simp at h
  cases h.1
  simp at h
  specialize h ((x+1)^2) (x+1)
  simp at h

[Junyan Xu]

cross link

[Ruben Van de Velde]

Thanks for the explanation, Kevin! Now I understand why I didn't manage to prove the equivalence :)

[Eric Wieser]

In lean 3 we were stuck with this behavior because notation was inflexible; can we just make ∃! (x y : Int), an error now?

[Kyle Miller]

@Eric Wieser mathlib4#12218

[Kyle Miller]

If anyone wants to help with the errors, all you need to do is turn expressions like ∃! (b : _) (_ : b ∈ c), a ∈ b into ∃! b, ∃! _ : b ∈ c, a ∈ b. Notice the lack of parentheses, the ability to drop : _, and, furthermore, the fact that this isn't being re-stated more reasonably. (It would be more simple as ∃! b, b ∈ c ∧ a ∈ b.)

I figure a follow-up PR could review all uses of ∃! and clean them up.

[Eric Wieser]

I guess ExistsUnique could allow chained prop binders?

[Kyle Miller]

I think rather it would be good to have extended binder syntax so that ∃! b ∈ c, a ∈ b is ∃! b, b ∈ c ∧ a ∈ b, just like for Exists. That could be in that follow-up PR.

[Mark Fischer]

Is there a technical reason Lean doesn't allow destructuring in the parameter position?
Does it get weird with dependent types?

[Kyle Miller]

Lean allows it in fun, but there's some inconsistency between various notations that accept binders. The main issue is that if you allow destructuring, you get a match expression in the body of your quantifier.

[Kyle Miller]

Is docs#NumberField.Units.exist_unique_eq_mul_prod (the Dirichlet unit theorem) stated correctly?

[Kevin Buzzard]

My guess is no, and that the assertion is too weak

[Kyle Miller]

@Eric Wieser #12237

[Kyle Miller]

@Kevin Buzzard Thanks — here's a fix #12240