obtain acrobatics

Stream: lean4

[Darij Grinberg]

I've recently been working (with a few others) on a Lean formalization of some basic combinatorial objects (perfect matchings of a finite set; the eventual goal is Pfaffians). Today I've at last tried out aristotle, which suggested a short but rather strange obtain command. I wonder if someone can explain it to me.

This is in the proof of PerfectMatching.partner_block in https://github.com/ghseeli/lean-club/blob/4743c35b97573a2305458bec30fd9822564f75a1/LeanClub/Pfaffian.lean (second-to-last theorem; note that only the last two proofs are aristotle's handiwork). A PerfectMatching \alpha is defined as a Finset of ordered pairs that are furthermore disjoint and contain each element of \alpha among them (thus a structure with four fields: edges, ordered, disjoint, union; we'll probably refactor this eventually, but this is very much a babby's first implementation). The function set transforms a pair (a, b) into the finset {a, b}. The function M.block sends an element of \alpha to the unique edge of M that contains this element. The theorem partner_block says:

theorem PerfectMatching.partner_block (M : PerfectMatching α) (i : α) :
    set (M.block i) = {i, M.partner i}

Aristotle (after a first strange but completely unnecessary restatement via ext and intro) does the following:

obtain ⟨a, b, hab, hi⟩ : ∃ a b : α, a < b ∧ i ∈ ({a, b} : Finset α) ∧ M.block i = (a, b) := by
      have := M.block_spec i;
      exact ⟨ _, _, M.ordered _ this.1, this.2, rfl ⟩;

Note that M.block_spec i results in (M.block i ∈ M.edges) ∧ (i ∈ _root_.set (M.block i)). But what happens on the exact line? Why does the existence quantifier appear out of thin air?

And is this a style I should imitate? It's significantly shorter than my code...

[Yan Yablonovskiy 🇺🇦]

This works due to the anonymous constructor syntax:
https://lean-lang.org/theorem_proving_in_lean4/Quantifiers-and-Equality/?terms=anonymous%C2%A0#the-existential-quantifier

It works for more than existential, roughly if there is enough info to guess the type of a term that's a structure, you can use that syntax as shorthand for every field the structure has.

https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/?terms=anonymous#anonymous-constructor-syntax

[Darij Grinberg]

Wow, so the typechecker can solve this kind of sudoku!

[Darij Grinberg]

I guess rfl being the last field, it knows what a and b are...

[Darij Grinberg]

Oh, so this works just as well:
    exact ⟨ (M.block i).1, (M.block i).2, M.ordered (M.block i) this.1, this.2, rfl ⟩;
meaning that it understands that M.block i = ((M.block i).1, (M.block i).2) by rfl. So the sudoku is not as hard as I thought...

[Darij Grinberg]

Thanks @Yan Yablonovskiy 🇺🇦 !