mutual theorems

Stream: lean4

[Arthur Paulino]

What's the simplest example of mutually recursive theorems you can think of?
Thanks in advance!

[Arthur Paulino]

There's an example on these slides, but if anyone can craft something simpler, it would be super helpful :pray:

[Eric Wieser]

I would guess that some of the Lean3 proofs about docs#pgame.has_le would make sense as a mutual theorem

[Eric Wieser]

Such as https://github.com/leanprover-community/mathlib/blob/f9c339ecf5efb4cf0d911bb3501bd57ca2ef2507/src/set_theory/game/pgame.lean#L306-L313

[Arthur Paulino]

Actually let me remove #xy noise. We're trying to compile Lean environment to a content-addressed version (more on the topic here) and we want to validate our method to compile mutual theorems.

The issue we found is that we cannot find mutual theorems in the environment! So we're wondering what's happening. Does Lean elaborate mutual theorems to a single theorem? What's the resulting name of the theorem? We're not finding it after running Lean's frontend

[Reid Barton]

I assume the answers are the same as in Lean 3:
Arthur Paulino said:

Does Lean elaborate mutual theorems to a single theorem?

Yes.

What's the resulting name of the theorem? We're not finding it after running Lean's frontend

Implementation-defined by the elaborator. The original names will be defined as applications of the internally generated single theorem.

[Reid Barton]

Mutual declarations don't exist in the kernel or at the level of expr.

[Sebastian Ullrich]

Basically, see also comment at https://github.com/leanprover/lean4/blob/b6f251bcd33e3941cd653777068bd0bb2919a6a4/src/Lean/Declaration.lean#L153

[Reid Barton]

Lean 3 example

mutual theorem a, b
  with a : ∀ (n : ℕ), n = n
  | 0 := rfl
  | (n + 1) := @congr_arg _ _ _ _ (λ i, i + 1) (b n)
  with b : ∀ (n : ℕ), n = n
  | 0 := rfl
  | (n + 1) := @congr_arg _ _ _ _ (λ i, i + 1) (a n)

#print a        --  theorem a : ∀ (n : ℕ), n = n := a._main
#print a._main  --  theorem a._main : ∀ (n : ℕ), n = n := λ (n : ℕ), a.b._mutual (psum.inl n)
#print a.b._mutual
-- theorem a.b._mutual : ∀ (_x : psum ℕ ℕ), (λ (_x : psum ℕ ℕ), psum.cases_on _x (λ (_s : ℕ), _s = _s) (λ (_s : ℕ), _s = _s)) _x :=
-- [big term]

[Reid Barton]

Fun fact--mathlib contains exactly one non-meta mutually inductive set of definitions

[Arthur Paulino]

Thanks!