lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

feat: new variable command

Open Kha opened this issue 1 year ago • 10 comments

Resolves #2452. For theorems, section variables are now conditionally included when elaborating the theorem body and sending the result to the kernel based on their use in the header; elaboration of the header is unchanged. Definitions as well are unchanged for now because it looks like adapting them will take more follow-up work: changing their behavior broke more than 30 tests while changing theorems' behavior broke one.

Specifically, section variables are included if they

  • are directly referenced by the theorem header,
  • are included via the new include command in the current section,
  • are directly referenced by any variable included by these rules, OR
  • are instance-implicit variables that reference any variable included by these rules.

For porting, a new option deprecated.oldSectionVars is included to locally switch back to the old behavior.

TODO: testing, docs, possibly more conveniences

Kha avatar Jul 23 '24 17:07 Kha

are instance-implicit variables that reference any variable included by these rules.

Should this be "are instance-implicit variables and all referenced variables are included by these rules."? For example, if I have

variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]

If only one of R/M is referenced, Module R M should not be included.

(I would also love it if include supports binder updates)

fpvandoorn avatar Jul 25 '24 10:07 fpvandoorn

are instance-implicit variables that reference any variable included by these rules.

Should this be "are instance-implicit variables and all referenced variables are included by these rules."? For example, if I have

Makes sense to me, updated.

(I would also love it if include supports binder updates)

Would include {v} be equivalent to variable {v} include v? I'm not sure yet what to think about such overloading of semantics

Kha avatar Jul 26 '24 08:07 Kha

Yes, those would be equivalent.

In Mathlib we are striving towards using variable {v} and include v only using in (i.e. variable {v} or include v is banned, you should solely use variable {v} in and include v in). If we follow that rule, then the ability to write include {v} means that we don't need variable {v} anymore in Mathlib, since all its uses can be replaced by include.

fpvandoorn avatar Jul 27 '24 09:07 fpvandoorn

Yes, those would be equivalent.

In Mathlib we are striving towards using variable {v} and include v only using in (i.e. variable {v} or include v is banned, you should solely use variable {v} in and include v in). If we follow that rule, then the ability to write include {v} means that we don't need variable {v} anymore in Mathlib, since all its uses can be replaced by include.

@fpvandoorn, I've finally started looking at Mathlib under this PR (the lean-pr-testing-4814 branch). (It is going to be epic! :-)

I've already encountered a few places where is seems rather inconvenient for only using include ... in, rather than bounded by a section. Please see https://github.com/leanprover-community/mathlib4/commit/c3ec6bedfaddc035e24f86a44099089854a7d13c for the first two examples I encountered.

kim-em avatar Jul 29 '24 00:07 kim-em

Mathlib CI status (docs):

leanprover-community-mathlib4-bot avatar Jul 29 '24 00:07 leanprover-community-mathlib4-bot

Re: looking at Mathlib on this PR. So far there are two classes of problems: typeclasses hypothesis being included which should not be (for which the new linter is really helpful), and variables with need an include.

Fixing the first class of problems requires either adding sections to bound variable [...] scopes, using variable ... in, or reordering results.

I propose that for anyone working on the Mathlib branch for this PR, we try to backport all the changes of the first form.

A reasonable workflow seems to be:

  • As you make changes on lean-pr-testing-4814, any changes that use include (i.e. which will not work on master), you immediately stage.
  • But any changes for excluding typeclasses hypotheses you leave unstage.
  • At suitable intervals, make a commit of the stages changes on lean-pr-testing-4814
  • Then stash the remaining changes, make a new branch off master, make a PR from it, and then ~~merge that branch~~ cherry-pick that commit back to lean-pr-testing-4814. (See first example of such a PR at https://github.com/leanprover-community/mathlib4/pull/15245.)

(We have have following a similar workflow for the byAsSorry branch, c.f. zulip discusssion.)

This is going to be a massive adaptation exercise to get this working, and I will need help to get it done.

kim-em avatar Jul 29 '24 00:07 kim-em

are instance-implicit variables that reference any variable included by these rules.

Should this be "are instance-implicit variables and all referenced variables are included by these rules."? For example, if I have

Makes sense to me, updated.

@Kha, I think this change may have not worked as intended. In Mathlib on lean-pr-testing-4814 I am seeing:

section Trans

variable [IsTrans N r] (m n : M) {a b c d : N}

--  Lemmas with 3 elements.
theorem act_rel_of_rel_of_act_rel (ab : r a b) (rl : r (μ m b) c) : r (μ m a) c :=
  _root_.trans (act_rel_act_of_rel m ab) rl

theorem rel_act_of_rel_of_rel_act (ab : r a b) (rr : r c (μ m a)) : r c (μ m b) :=
  _root_.trans rr (act_rel_act_of_rel _ ab)

end Trans

failing with failed to synthesize IsTrans N r, despite both the arguments of IsTrans being mentioned in the theorem statement.

(I have no idea why in Mathlib the first argument of IsTrans is explicit rather than implicit -- I'll investigate that too...)

Let me know if you'd like a minimization of this.

kim-em avatar Jul 29 '24 00:07 kim-em

@Kha, another bug, where typeclass arguments that are included transitively can be included with multiplicity, apparently!

Again on lean-pr-testing-4814, in Mathlib.Order.Monotone, we see:

variable (α) [Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α]

/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
monotone function `f : ℤ → α`. -/
theorem exists_strictMono : ∃ f : ℤ → α, StrictMono f := by
  inhabit α
  rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
  rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
  refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
  rintro (n | _ | n)
  · exact hf n.lt_succ_self
  · show g 1 < f 0
    rw [hf₀, ← hg₀]
    exact hg Nat.zero_lt_one
  · exact hg (Nat.lt_succ_self _)

resulting in the signature

Int.exists_strictMono.{u} (α : Type u) [Preorder α] [Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α] :
  ∃ f, StrictMono f

where apparently [Preorder α] has been added twice, once because [NoMinOrder α] needs it and again because [NoMaxOrder α] needs it.

Again, please let me know if you'd like an minimisation.

kim-em avatar Jul 29 '24 01:07 kim-em

And another problem, @Kha! We have places in Mathlib where people have add implicit arguments that could otherwise be automatically included instance arguments, on the principle that it is faster/better to find these by unification from later arguments that to redo typeclass search.

Here's an example from Mathlib in Mathlib.Algebra.GroupWithZero:

@[simp]
lemma coe_copy {_ : MulZeroOneClass α} {_ : MulZeroOneClass β} (f : α →*₀ β) (f' : α → β) (h) :
    (f.copy f' h) = f' := rfl

lemma copy_eq {_ : MulZeroOneClass α} {_ : MulZeroOneClass β} (f : α →*₀ β) (f' : α → β) (h) :
    f.copy f' h = f := DFunLike.ext' h

It's perfectly okay on master to just omit these, and instead we get corresponding instance arguments included.

However on lean-pr-testing-4814, we get warning, because the signature becomes:

MonoidWithZeroHom.coe_copy.{u_2, u_3} {α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] :
  ∀ {x : MulZeroOneClass α} {x_1 : MulZeroOneClass β} (f : α →*₀ β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'

I'm uncertain the best way to proceed here. Probably we ought to make the variable inclusion mechanism robust to this, and decline to include instance arguments if there are already there as implicit arguments. In this particular case it's fine to just remove them, but I don't think that is always going to be true.

Again, let me know if you want a minimization.

kim-em avatar Jul 29 '24 01:07 kim-em

And more. :-)

We may need to pull in typeclass arguments because they mention the type of an included argument, not just the argument itself.

For example in Mathlib we have in Mathlib.Algebra.Ring.Divisibility.Basic:

variable [Semigroup α] [Semigroup β] {F : Type*} [EquivLike F α β] [MulEquivClass F α β] (f : F)

theorem map_dvd_iff {a b} : f a ∣ f b ↔ a ∣ b :=
  let f := MulEquivClass.toMulEquiv f
  ⟨fun h ↦ by rw [← f.left_inv a, ← f.left_inv b]; exact map_dvd f.symm h, map_dvd f⟩

theorem MulEquiv.decompositionMonoid [DecompositionMonoid β] : DecompositionMonoid α where
  primal a b c h := by
    rw [← map_dvd_iff f, map_mul] at h
    obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h
    refine ⟨symm f a₁, symm f a₂, ?_⟩
    simp_rw [← map_dvd_iff f, ← map_mul, eq_symm_apply]
    iterate 2 erw [(f : α ≃* β).apply_symm_apply]
    exact h

Here include f on MulEquiv.decompositionMonoid (or just writing it as an explicit argument) doesn't suffice to pull in [MulEquivClass F α β].

Making matters worse, if we just change the theorem statement to

theorem MulEquiv.decompositionMonoid 
    [MulEquivClass F α β] (f : F) [DecompositionMonoid β] : DecompositionMonoid α where

then we get the incorrect warning:

included section variable '[MulEquivClass F α β]' is not used in 'MulEquiv.decompositionMonoid', consider excluding it

I can work around this by just not making it a section variable at all and instead including it directly in both theorems here.

(As above with minimization. :-)

kim-em avatar Jul 29 '24 01:07 kim-em

Yes, those would be equivalent. In Mathlib we are striving towards using variable {v} and include v only using in (i.e. variable {v} or include v is banned, you should solely use variable {v} in and include v in). If we follow that rule, then the ability to write include {v} means that we don't need variable {v} anymore in Mathlib, since all its uses can be replaced by include.

@fpvandoorn, I've finally started looking at Mathlib under this PR (the lean-pr-testing-4814 branch). (It is going to be epic! :-)

I've already encountered a few places where is seems rather inconvenient for only using include ... in, rather than bounded by a section. Please see leanprover-community/mathlib4@c3ec6be for the first two examples I encountered.

We should probably not strive to do this immediately. Another thing we can consider is to have (in the long-term) no explicit variables, instead repeating those in each theorem statement. That should also reduce the number of includes. But given your example we maybe want to allow having a global include directly after the corresponding variable statement. Then whenever that variable is visible it will have the include statement.

fpvandoorn avatar Jul 29 '24 07:07 fpvandoorn

@Kha, another bug, where typeclass arguments that are included transitively can be included with multiplicity, apparently!

Again on lean-pr-testing-4814, in Mathlib.Order.Monotone, we see:

variable (α) [Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α]

/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
monotone function `f : ℤ → α`. -/
theorem exists_strictMono : ∃ f : ℤ → α, StrictMono f := by
  inhabit α
  rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
  rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
  refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
  rintro (n | _ | n)
  · exact hf n.lt_succ_self
  · show g 1 < f 0
    rw [hf₀, ← hg₀]
    exact hg Nat.zero_lt_one
  · exact hg (Nat.lt_succ_self _)

resulting in the signature

Int.exists_strictMono.{u} (α : Type u) [Preorder α] [Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α] :
  ∃ f, StrictMono f

where apparently [Preorder α] has been added twice, once because [NoMinOrder α] needs it and again because [NoMaxOrder α] needs it.

Again, please let me know if you'd like an minimisation.

This looks correct in that there is already a [Preorder \a] in context. But also #2789 comes in and prevents us from removing the duplicate assumption unless broken into two lines.

variable (α)
variable [Nonempty α] [NoMinOrder α] [NoMaxOrder α]

Kha avatar Jul 30 '24 08:07 Kha

Probably we ought to make the variable inclusion mechanism robust to this, and decline to include instance arguments if there are already there as implicit arguments.

I'm a bit wary of comparing parameter types by equality (which one?). I assume one alternative would be to name the instances and use binder updates instead?

Kha avatar Jul 30 '24 09:07 Kha

failing with failed to synthesize IsTrans N r, despite both the arguments of IsTrans being mentioned in the theorem statement.

Fixed

Here include f on MulEquiv.decompositionMonoid (or just writing it as an explicit argument) doesn't suffice to pull in [MulEquivClass F α β].

Fixed

Kha avatar Jul 30 '24 09:07 Kha

I am rebasing on nightly-with-mathlib (regenerating update-stage0 commits), in order to keep the Mathlib adaptation branch viable.

kim-em avatar Jul 31 '24 02:07 kim-em

Sigh, the merge conflict with master occurs after nightly-with-mathlib. I will see if Mathlib's nightly-testing is compatible with master, and if so rebase this onto master.

Edit: nope! We'll need to wait until the next nightly release and try again then.

kim-em avatar Jul 31 '24 02:07 kim-em