Skip proof arguments during unification, and try structure eta last #2210
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
I'm making this PR now because a large part of the mathlib port is getting blocked on the eta issue. Particularly leanprover-community/mathlib4#3708 seems impossible to work around. MWEs are forthcoming, but extracting them from mathlib takes some effort. |
|
This is a MWE that I extracted today from mathlib. Perhaps it would be suitable as a test? /-!
# An etaExperiment timeout
The purpose of this file is to demonstrate a typeclass search that
* times out with `etaExperiment`
* is fast on `lean-toolchain` `gebner/lean4:reenableeta230506`
* is realistic, i.e. is a minimisation of something appearing in mathlib.
I've taken the example Matthew Ballard showed me:
```
import Mathlib
#synth Zero ℤ
```
and minimised it.
I've used `sorry` liberally,
but not changed the typeclass inheritance structure at all relative to mathlib4.
(It could probably be minimized further, but I think this is not the point?)
This file is minimised in the sense that:
* removing any command should either cause a new error, or remove the timeout.
* removing any field of a structure, and sorrying a field of an instance, should do the same.
Section titles correspond to the files the material came from the mathlib4/std4.
-/
section Std.Classes.Cast
class NatCast (R : Type u) where
class IntCast (R : Type u) where
end Std.Classes.Cast
section Std.Data.Int.Lemmas
namespace Int
theorem add_zero : ∀ a : Int, a + 0 = a := sorry
theorem mul_one (a : Int) : a * 1 = a := sorry
end Int
end Std.Data.Int.Lemmas
section Std.Classes.RatCast
class RatCast (K : Type u) where
end Std.Classes.RatCast
section Mathlib.Init.ZeroOne
class Zero.{u} (α : Type u) where
zero : α
instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
ofNat := ‹Zero α›.1
class One (α : Type u) where
one : α
instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
ofNat := ‹One α›.1
end Mathlib.Init.ZeroOne
section Mathlib.Algebra.Group.Defs
class Inv (α : Type u) where
class Semigroup (G : Type u) extends Mul G where
class AddSemigroup (G : Type u) extends Add G where
class CommSemigroup (G : Type u) extends Semigroup G where
mul_comm : ∀ a b : G, a * b = b * a
class AddCommSemigroup (G : Type u) extends AddSemigroup G where
class MulOneClass (M : Type u) extends One M, Mul M where
mul_one : ∀ a : M, a * 1 = a
class AddZeroClass (M : Type u) extends Zero M, Add M where
add_zero : ∀ a : M, a + 0 = a
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
class Group (G : Type u) extends DivInvMonoid G where
class AddGroup (A : Type u) extends SubNegMonoid A where
class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
end Mathlib.Algebra.Group.Defs
section Mathlib.Logic.Nontrivial
class Nontrivial (α : Type _) : Prop where
end Mathlib.Logic.Nontrivial
section Mathlib.Algebra.GroupWithZero.Defs
class MulZeroClass (M₀ : Type u) extends Mul M₀, Zero M₀ where
class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀]
extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀ : Prop
class NoZeroDivisors (M₀ : Type _) [Mul M₀] [Zero M₀] : Prop where
class SemigroupWithZero (S₀ : Type u) extends Semigroup S₀, MulZeroClass S₀
class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀
class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀
class CommMonoidWithZero (M₀ : Type _) extends CommMonoid M₀, MonoidWithZero M₀
class CancelCommMonoidWithZero (M₀ : Type _) extends CommMonoidWithZero M₀, IsLeftCancelMulZero M₀
end Mathlib.Algebra.GroupWithZero.Defs
section Mathlib.Data.Nat.Cast.Defs
class AddMonoidWithOne (R : Type u) extends NatCast R, AddMonoid R, One R where
class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R
end Mathlib.Data.Nat.Cast.Defs
section Mathlib.Data.Int.Cast.Defs
class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R where
end Mathlib.Data.Int.Cast.Defs
section Mathlib.Algebra.Ring.Defs
class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, MulZeroClass α
class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α
class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
AddCommMonoidWithOne α
class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
class CommRing (α : Type u) extends Ring α, CommMonoid α
instance CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
{ s with }
class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop
end Mathlib.Algebra.Ring.Defs
section Mathlib.Data.Int.Basic
instance : CommRing Int where
mul_comm := sorry
mul_one := Int.mul_one -- Replacing this with `sorry` makes the timeout go away!
add_zero := Int.add_zero -- Similarly here.
end Mathlib.Data.Int.Basic
section Mathlib.Algebra.Ring.Regular
section IsDomain
instance IsDomain.toCancelCommMonoidWithZero [CommSemiring α] [IsDomain α] :
CancelCommMonoidWithZero α := { }
end IsDomain
end Mathlib.Algebra.Ring.Regular
section Mathlib.Algebra.Field.Defs
class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K, RatCast K where
class Field (K : Type u) extends CommRing K, DivisionRing K
end Mathlib.Algebra.Field.Defs
section Mathlib.Algebra.Field.Basic
instance Field.isDomain [Field K] : IsDomain K :=
sorry
end Mathlib.Algebra.Field.Basic
-- Finally, the example:
#synth Zero Int -- works fine
set_option synthInstance.etaExperiment true in
#synth Zero Int -- but times out under `etaExperiment`.
set_option synthInstance.etaExperiment true in
-- usual limit is 20000, and this takes even longer in real mathlib4
set_option synthInstance.maxHeartbeats 50000 in
#synth Zero Int -- still works with a higher timelimit. |
|
Cyril Cohen has long argued that we could be using unification hints for our algebra hierarchy (they are in Lean 4, after all!). How do they fit into this picture? |
|
@semorrison Thank you for the example! It was exactly what I was looking for and I've added it to the test suite. |
|
@gebner, I have another minimisation (from the It's here if you'd like it. |
|
A quick quantitative analysis of the MWE suggests that this is not a failure of defeq caching either - the unification problems are so varied that the only good option is to avoid generating them in the first place |
|
@Parcly-Taxel and I have redone the minimisation of the problem in It is better than my minimisation linked above because it actually succeeds with this PR, rather than failing with a type error. Parcly-Taxel did an initial minimisation that still relied on I think it would be good to include this one as a test case as well, as it doesn't get much more "realistic" than this --- it's exactly the current obstacle for porting. section Std.Classes.Cast
class NatCast (R : Type u) where
class IntCast (R : Type u) where
end Std.Classes.Cast
section Std.Classes.RatCast
class RatCast (K : Type u) where
end Std.Classes.RatCast
section Init.ZeroOne
class Zero.{u} (α : Type u) where
zero : α
instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
ofNat := ‹Zero α›.1
class One (α : Type u) where
one : α
instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
ofNat := ‹One α›.1
end Init.ZeroOne
section Init.Algebra.Order
class Preorder (α : Type u) extends LE α, LT α where
class PartialOrder (α : Type u) extends Preorder α :=
le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
variable [PartialOrder α]
theorem le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
PartialOrder.le_antisymm _ _
class LinearOrder (α : Type u) extends PartialOrder α where
end Init.Algebra.Order
section Init.Data.Nat.Lemmas
namespace Nat
instance linearOrder : LinearOrder Nat where
le := Nat.le
le_antisymm := @Nat.le_antisymm
lt := Nat.lt
end Nat
end Init.Data.Nat.Lemmas
section Init.Set
def Set (α : Type u) := α → Prop
def setOf {α : Type u} (p : α → Prop) : Set α := p
namespace Set
protected def Mem (a : α) (s : Set α) : Prop := s a
instance : Membership α (Set α) := ⟨Set.Mem⟩
end Set
end Init.Set
section Logic.Nontrivial
class Nontrivial (α : Type _) : Prop where
end Logic.Nontrivial
section Algebra.Group.Defs
class SMul (M : Type _) (α : Type _) where
smul : M → α → α
class Inv (α : Type u) where
inv : α → α
postfix:max "⁻¹" => Inv.inv
class Semigroup (G : Type u) extends Mul G where
mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
class AddSemigroup (G : Type u) extends Add G where
add_assoc : ∀ a b c : G, a + b + c = a + (b + c)
class CommSemigroup (G : Type u) extends Semigroup G where
mul_comm : ∀ a b : G, a * b = b * a
class AddCommSemigroup (G : Type u) extends AddSemigroup G where
add_comm : ∀ a b : G, a + b = b + a
section CommSemigroup
variable [AddCommSemigroup G]
theorem add_comm : ∀ a b : G, a + b = b + a :=
AddCommSemigroup.add_comm
end CommSemigroup
class AddZeroClass (M : Type u) extends Zero M, Add M where
zero_add : ∀ a : M, 0 + a = a
add_zero : ∀ a : M, a + 0 = a
class MulOneClass (M : Type u) extends One M, Mul M where
one_mul : ∀ a : M, 1 * a = a
mul_one : ∀ a : M, a * 1 = a
variable {M : Type u}
def npowRec [One M] [Mul M] : Nat → M → M
| 0, _ => 1
| n + 1, a => a * npowRec n a
def nsmulRec [Zero M] [Add M] : Nat → M → M
| 0, _ => 0
| n + 1, a => a + nsmulRec n a
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
nsmul : Nat → M → M := nsmulRec
nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
nsmul_succ : ∀ (n : Nat) (x), nsmul (n + 1) x = x + nsmul n x := by intros; rfl
class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
npow : Nat → M → M := npowRec
npow_zero : ∀ x, npow 0 x = 1 := by intros; rfl
npow_succ : ∀ (n : Nat) (x), npow (n + 1) x = x * npow n x := by intros; rfl
class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
def zsmulRec {M : Type _} [Zero M] [Add M] [Neg M] : Int → M → M
| Int.ofNat n, a => nsmulRec n a
| Int.negSucc n, a => -nsmulRec n.succ a
class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
def SubNegMonoid.sub' {G : Type u} [AddMonoid G] [Neg G] (a b : G) : G := a + -b
class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
sub := SubNegMonoid.sub'
sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl
zsmul : Int → G → G := zsmulRec
zsmul_zero' : ∀ a : G, zsmul 0 a = 0
zsmul_succ' (n : Nat) (a : G) : zsmul (Int.ofNat n.succ) a = a + zsmul (Int.ofNat n) a
zsmul_neg' (n : Nat) (a : G) : zsmul (Int.negSucc n) a = -zsmul n.succ a
class AddGroup (A : Type u) extends SubNegMonoid A where
add_left_neg : ∀ a : A, -a + a = 0
class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
end Algebra.Group.Defs
section Algebra.GroupWithZero.Defs
class MulZeroClass (M₀ : Type u) extends Mul M₀, Zero M₀ where
class SemigroupWithZero (S₀ : Type u) extends Semigroup S₀, MulZeroClass S₀
class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀
class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀
end Algebra.GroupWithZero.Defs
section Mathlib.Data.Nat.Cast.Defs
class AddMonoidWithOne (R : Type u) extends NatCast R, AddMonoid R, One R where
class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R
end Mathlib.Data.Nat.Cast.Defs
section Mathlib.Data.FunLike.Basic
class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
coe : F → ∀ a : α, β a
variable {F α : Sort _} {β : α → Sort _} [i : FunLike F α β]
instance hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe
end Mathlib.Data.FunLike.Basic
section Algebra.Hom.Group
structure ZeroHom (M : Type _) (N : Type _) [Zero M] [Zero N] where
toFun : M → N
map_zero' : toFun 0 = 0
class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N]
extends FunLike F M fun _ => N where
structure AddHom (M : Type _) (N : Type _) [Add M] [Add N] where
toFun : M → N
map_add' : ∀ x y, toFun (x + y) = toFun x + toFun y
class AddHomClass (F : Type _) (M N : outParam (Type _)) [Add M] [Add N]
extends FunLike F M fun _ => N where
structure AddMonoidHom (M : Type _) (N : Type _) [AddZeroClass M] [AddZeroClass N] extends
ZeroHom M N, AddHom M N
infixr:25 " →+ " => AddMonoidHom
structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
infixr:25 " →ₙ* " => MulHom
structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
OneHom M N, M →ₙ* N
infixr:25 " →* " => MonoidHom
structure MonoidWithZeroHom (M : Type _) (N : Type _)
[MulZeroOneClass M] [MulZeroOneClass N] extends ZeroHom M N, MonoidHom M N
infixr:25 " →*₀ " => MonoidWithZeroHom
end Algebra.Hom.Group
section Mathlib.GroupTheory.GroupAction.Defs
class MulAction (α : Type _) (β : Type _) [Monoid α] extends SMul α β where
class DistribMulAction (M A : Type _) [Monoid M] [AddMonoid A] extends MulAction M A where
end Mathlib.GroupTheory.GroupAction.Defs
section Mathlib.Order.Basic
class Sup (α : Type u) where
class Inf (α : Type u) where
end Mathlib.Order.Basic
section Order.Lattice
class SemilatticeSup (α : Type u) extends Sup α, PartialOrder α where
class SemilatticeInf (α : Type u) extends Inf α, PartialOrder α where
class Lattice (α : Type u) extends SemilatticeSup α, SemilatticeInf α
end Order.Lattice
section Order.BoundedOrder
class Bot (α : Type u) where
end Order.BoundedOrder
section Mathlib.Algebra.Order.Monoid.Defs
class OrderedAddCommMonoid (α : Type _) extends AddCommMonoid α, PartialOrder α where
class LinearOrderedAddCommMonoid (α : Type _) extends LinearOrder α, OrderedAddCommMonoid α
end Mathlib.Algebra.Order.Monoid.Defs
section Mathlib.Data.Int.Cast.Defs
class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R where
end Mathlib.Data.Int.Cast.Defs
section Algebra.Ring.Defs
class Distrib (R : Type _) extends Mul R, Add R where
class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α
class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α
class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
AddCommMonoidWithOne α
class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
class CommRing (α : Type u) extends Ring α, CommMonoid α
end Algebra.Ring.Defs
section Algebra.Order.Monoid.Cancel.Defs
class OrderedCancelAddCommMonoid (α : Type u) extends AddCommMonoid α, PartialOrder α where
end Algebra.Order.Monoid.Cancel.Defs
section Data.Pi.Algebra
variable {I : Type u} {f : I → Type v₁}
instance instAdd [∀ i, Add <| f i] : Add (∀ i : I, f i) := sorry
end Data.Pi.Algebra
section Mathlib.Algebra.Order.Ring.Defs
class StrictOrderedSemiring (α : Type u) extends Semiring α, OrderedCancelAddCommMonoid α,
Nontrivial α where
class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring α,
LinearOrderedAddCommMonoid α
end Mathlib.Algebra.Order.Ring.Defs
section Data.Nat.Basic
namespace Nat
instance semiring : Semiring Nat where
add := Nat.add
add_assoc := Nat.add_assoc
zero := Nat.zero
zero_add := Nat.zero_add
add_zero := Nat.add_zero
add_comm := Nat.add_comm
mul := Nat.mul
mul_assoc := Nat.mul_assoc
one := Nat.succ Nat.zero
one_mul := Nat.one_mul
mul_one := Nat.mul_one
end Nat
end Data.Nat.Basic
section Data.Set.Basic
namespace Set
protected def Nonempty (s : Set α) : Prop := ∃ x, x ∈ s
end Set
end Data.Set.Basic
section Data.Nat.Order.Basic
instance linearOrderedSemiring : LinearOrderedSemiring Nat :=
{ Nat.semiring, Nat.linearOrder with
lt := Nat.lt }
end Data.Nat.Order.Basic
section Algebra.Hom.Ring
variable {α β : Type _}
structure NonUnitalRingHom (α β : Type _) [NonUnitalNonAssocSemiring α]
[NonUnitalNonAssocSemiring β] extends α →ₙ* β, α →+ β
infixr:25 " →ₙ+* " => NonUnitalRingHom
structure RingHom (α : Type _) (β : Type _) [NonAssocSemiring α] [NonAssocSemiring β] extends
α →* β, α →+ β, α →ₙ+* β, α →*₀ β
infixr:25 " →+* " => RingHom
end Algebra.Hom.Ring
section Algebra.Field.Defs
class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K, RatCast K where
class Field (K : Type u) extends CommRing K, DivisionRing K
end Algebra.Field.Defs
section Order.CompleteLattice
class InfSet (α : Type _) where
sInf : Set α → α
export InfSet (sInf)
end Order.CompleteLattice
section Algebra.Order.Hom.Basic
class SubadditiveHomClass (F : Type _) (α β : outParam (Type _)) [Add α] [Add β] [LE β] extends
FunLike F α fun _ => β where
class AddGroupSeminormClass (F : Type _) (α β : outParam <| Type _) [AddGroup α]
[OrderedAddCommMonoid β] extends SubadditiveHomClass F α β where
end Algebra.Order.Hom.Basic
section Order.ConditionallyCompleteLattice.Basic
variable {α : Type _}
variable [LE α] [InfSet α] {s t : Set α} {a b : α}
theorem le_csInf (h₁ : s.Nonempty) (h₂ : ∀ {b} (h : b ∈ s), a ≤ b) : a ≤ sInf s := sorry
end Order.ConditionallyCompleteLattice.Basic
section Data.Nat.Lattice
noncomputable instance : InfSet Nat :=
{ sInf := sorry }
end Data.Nat.Lattice
section Mathlib.Algebra.Module.Basic
class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends
DistribMulAction R M where
end Mathlib.Algebra.Module.Basic
section Algebra.Module.LinearMap
structure LinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type _)
(M₂ : Type _) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends
AddHom M M₂ where
notation:25 M " →ₛₗ[" σ:25 "] " M₂:0 => LinearMap σ M M₂
class SemilinearMapClass (F : Type _) {R S : outParam (Type _)} [Semiring R] [Semiring S]
(σ : outParam (R →+* S)) (M M₂ : outParam (Type _)) [AddCommMonoid M] [AddCommMonoid M₂]
[Module R M] [Module S M₂] extends AddHomClass F M M₂ where
end Algebra.Module.LinearMap
section Topology.Basic
class TopologicalSpace (α : Type u) where
end Topology.Basic
section Mathlib.Topology.ContinuousFunction.Basic
structure ContinuousMap (α β : Type _) [TopologicalSpace α] [TopologicalSpace β] where
class ContinuousMapClass (F : Type _) (α β : outParam <| Type _) [TopologicalSpace α]
[TopologicalSpace β] extends FunLike F α fun _ => β where
end Mathlib.Topology.ContinuousFunction.Basic
section Topology.Algebra.Monoid
class ContinuousAdd (M : Type u) [TopologicalSpace M] [Add M] : Prop where
end Topology.Algebra.Monoid
section Topology.Algebra.Group.Basic
class ContinuousNeg (G : Type u) [TopologicalSpace G] [Neg G] : Prop where
class TopologicalAddGroup (G : Type u) [TopologicalSpace G] [AddGroup G] extends
ContinuousAdd G, ContinuousNeg G : Prop
end Topology.Algebra.Group.Basic
section Topology.Algebra.Module.Basic
structure ContinuousLinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R →+* S)
(M : Type _) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type _) [TopologicalSpace M₂]
[AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₛₗ[σ] M₂ where
notation:25 M " →SL[" σ "] " M₂ => ContinuousLinearMap σ M M₂
class ContinuousSemilinearMapClass (F : Type _) {R S : outParam (Type _)} [Semiring R] [Semiring S]
(σ : outParam <| R →+* S) (M : outParam (Type _)) [TopologicalSpace M] [AddCommMonoid M]
(M₂ : outParam (Type _)) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M]
[Module S M₂] extends SemilinearMapClass F σ M M₂, ContinuousMapClass F M M₂
namespace ContinuousLinearMap
variable {R₁ : Type _} {R₂ : Type _} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂}
{M₁ : Type _} [TopologicalSpace M₁] [AddCommMonoid M₁]
{M₂ : Type _} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂]
instance LinearMap.coe : Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂) := ⟨toLinearMap⟩
instance continuousSemilinearMapClass :
ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂ where
coe := sorry
variable [ContinuousAdd M₂]
instance add : Add (M₁ →SL[σ₁₂] M₂) :=
⟨fun f g => ⟨f + g, sorry⟩⟩
instance addCommMonoid : AddCommMonoid (M₁ →SL[σ₁₂] M₂) where
zero := sorry
add := (· + ·)
zero_add := sorry
add_zero := sorry
add_comm := sorry
add_assoc := sorry
variable {R : Type _} [Ring R] {R₂ : Type _} [Ring R₂] {M : Type _}
[TopologicalSpace M] [AddCommGroup M] {M₂ : Type _} [TopologicalSpace M₂] [AddCommGroup M₂]
[Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂]
instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂) := by
refine'
{ ContinuousLinearMap.addCommMonoid with
zero := sorry
add := (· + ·)
neg := sorry
sub := sorry
.. } <;> sorry
end ContinuousLinearMap
end Topology.Algebra.Module.Basic
section Topology.UniformSpace.Basic
variable {α : Type ua} {β : Type ub}
structure UniformSpace.Core (α : Type u) where
class UniformSpace (α : Type u) extends TopologicalSpace α, UniformSpace.Core α where
@[reducible]
def UniformSpace.ofCore {α : Type u} (u : UniformSpace.Core α) : UniformSpace α where
toCore := u
toTopologicalSpace := sorry
def UniformSpace.ofFun {α : Type u} {β : Type v} [OrderedAddCommMonoid β]
(_ : α → α → β) : UniformSpace α := .ofCore { }
end Topology.UniformSpace.Basic
section Topology.Algebra.UniformGroup
class UniformAddGroup (α : Type _) [UniformSpace α] [AddGroup α] : Prop where
end Topology.Algebra.UniformGroup
section Analysis.Normed.Group.Seminorm
variable {E G : Type _}
structure AddGroupSeminorm (G : Type _) [AddGroup G] where
protected toFun : G → Nat
protected map_zero' : toFun 0 = 0
protected add_le' : ∀ r s, toFun (r + s) ≤ toFun r + toFun s
protected neg' : ∀ r, toFun (-r) = toFun r
variable [AddGroup E]
instance addGroupSeminormClass : AddGroupSeminormClass (AddGroupSeminorm E) E Nat where
coe f := f.toFun
end Analysis.Normed.Group.Seminorm
section Topology.MetricSpace.EMetricSpace
variable {α : Type u}
class EDist (α : Type _) where
edist : α → α → Nat
class PseudoEMetricSpace (α : Type u) extends EDist α : Type u where
toUniformSpace : UniformSpace α := sorry
attribute [instance] PseudoEMetricSpace.toUniformSpace
end Topology.MetricSpace.EMetricSpace
section Topology.MetricSpace.Basic
variable {α : Type u}
class Dist (α : Type _) where
dist : α → α → Nat
class PseudoMetricSpace (α : Type u) extends Dist α : Type u where
toUniformSpace : UniformSpace α := .ofFun dist
instance PseudoMetricSpace.toPseudoEMetricSpace : PseudoEMetricSpace α := sorry
class MetricSpace (α : Type u) extends PseudoMetricSpace α : Type u where
end Topology.MetricSpace.Basic
section Analysis.Normed.Group.Basic
variable {E F : Type _}
class Norm (E : Type _) where
norm : E → Nat
export Norm (norm)
notation "‖" e "‖" => norm e
class SeminormedAddGroup (E : Type _) extends Norm E, AddGroup E, PseudoMetricSpace E where
dist := fun x y => ‖x - y‖
dist_eq : ∀ x y, dist x y = ‖x - y‖ := sorry
class SeminormedAddCommGroup (E : Type _) extends Norm E, AddCommGroup E, PseudoMetricSpace E where
dist := fun x y => ‖x - y‖
dist_eq : ∀ x y, dist x y = ‖x - y‖ := sorry
def AddGroupSeminorm.toSeminormedAddGroup [AddGroup E] (f : AddGroupSeminorm E) :
SeminormedAddGroup E where
dist := sorry
norm := f
dist_eq := sorry
def AddGroupSeminorm.toSeminormedAddCommGroup [AddCommGroup E] (f : AddGroupSeminorm E) :
SeminormedAddCommGroup E :=
{ f.toSeminormedAddGroup with
add_comm := add_comm }
end Analysis.Normed.Group.Basic
section Analysis.Normed.Field.Basic
class NormedField (α : Type _) extends Norm α, Field α, MetricSpace α where
class NontriviallyNormedField (α : Type _) extends NormedField α where
class RingHomIsometric [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] (σ : R₁ →+* R₂) : Prop where
end Analysis.Normed.Field.Basic
section Mathlib.Analysis.NormedSpace.Basic
class NormedSpace (α : Type _) (β : Type _) [NormedField α] [SeminormedAddCommGroup β] extends
Module α β where
end Mathlib.Analysis.NormedSpace.Basic
section Topology.Algebra.Module.StrongTopology
variable {𝕜₁ 𝕜₂ : Type _} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E F : Type _}
[AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E]
instance [UniformSpace F] [UniformAddGroup F] : UniformSpace (E →SL[σ] F) := sorry
end Topology.Algebra.Module.StrongTopology
noncomputable section Analysis.NormedSpace.OperatorNorm
variable {𝕜 𝕜₂ E F : Type _}
variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}
def opNorm (f : E →SL[σ₁₂] F) := sInf (setOf fun c => 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖ )
instance hasOpNorm : Norm (E →SL[σ₁₂] F) := ⟨opNorm⟩
theorem bounds_nonempty [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} :
∃ c, c ∈ (setOf fun c => 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖) := sorry
variable [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
theorem op_norm_nonneg : 0 ≤ ‖f‖ := le_csInf bounds_nonempty sorry
def tmpSeminormedAddCommGroup : SeminormedAddCommGroup (E →SL[σ₁₂] F) :=
AddGroupSeminorm.toSeminormedAddCommGroup
{ map_zero' := le_antisymm sorry (op_norm_nonneg _)
add_le' := sorry
neg' := sorry }
def tmpPseudoMetricSpace : PseudoMetricSpace (E →SL[σ₁₂] F) :=
tmpSeminormedAddCommGroup.toPseudoMetricSpace
-- Final instance; times out without lean4#2210, passes with it
instance toSeminormedAddCommGroup : SeminormedAddCommGroup (E →SL[σ₁₂] F) where
dist_eq := tmpSeminormedAddCommGroup.dist_eq
end Analysis.NormedSpace.OperatorNorm |
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 16, 2023
Now that leanprover/lean4#2210 has been merged, this PR: * removes all the `set_option synthInstance.etaExperiment true` commands (and some `etaExperiment%` term elaborators) * removes many but not quite all `set_option maxHeartbeats` commands * makes various other changes required to cope with leanprover/lean4#2210. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Matthew Ballard <matt@mrb.email>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Summary
This PR contains two minimal changes to unification, allowing us to (1) re-enable eta for instances during typeclass search while (2) not breaking mathlib.
hinSubtype.mk a h =?= Subtype.mk b h').The performance impact on mathlib is favorable, resulting in a 23% decrease on wall-clock build time.
Context
Mathlib has instances like the following:
When synthesizing a
NoZeroDivisors Natinstance we apply the instance above and get the unification problemNoZeroDivisors ?R =?= NoZeroDivisors Nat. This unification problem is obviously unsolvable (sinceNatis not a ring), but we spend an enormous amount of time trying to see that.This is not a problem caused by eta for instances or limited to type-class synthesis. Structure eta merely makes unification slower incrementally. And it's possible to hit the same unification performance issues in term-mode as well. What makes type-class synthesis special is that it is used pervasively, it is impossible to work around it if it's used inside another module, and it applies hundreds of instances.
The resulting problematic unification problems are failing problems of the form
?x * ?y =?= x * y, or looking at the instance argument,LinearOrderedRing.toMul ?ring =?= instMul. Succeeding problems don't trigger this issue because they do not lead to backtracking.Several unification rules are responsible for the expensive backtracking:
NonAssocSemiring.toMul inst1 =?= NonAssocSemiring.toMul inst2creates two subproblems:inst1 =?= inst2and the one where both sides are reduced, e.g. toNonUnitalNonAssocRing.toMul inst1' =?= NonUnitalNonAssocRing.toMul inst2'. And lazy delta can apply to both subgoals again.mul_comm : ∀ x y, x * y = y * x, whose types contain multiple copies of the other fields.inst1 =?= NonAssocSemiring.mk .., and then backtrack. After backtracking, lazy delta reduction may decide to reduceinst1toinst1'and we apply structure eta again.ad (2). This is a big problem because
isDefEqAppunifies explicit arguments first. And references to parent structures (likeMul R) are instance-implicit.This PR only attacks (2) and (3) because changing these causes little regression. Skipping the proof arguments is easily seen to be correct (because the types are known to be defeq), the main potential concern is that we might assign fewer proof metavariables. I haven't seen any regressions from moving structure eta to the end.
Downsides of this PR
Unification is still slow. This is not the ultimate fix.
The proof arguments to
Quotient.lift₂are sometimes no longer filled in by unification. This could be because they're lambdas, but I didn't investigate this too much as this only happens in a handful of cases in mathlib.Attempted alternatives
Special handling for type-class instances in the unifier
I have tried adding a special unification procedure for type-class instances in https://github.com/leanprover/lean4/compare/master...gebner:lean4:szdlkj?expand=1, which basically does full WHNF first and then compares the fields and does eta if necessary. The prototype implementation puts this in a separate function so that it is easier to disable backtracking.
The main takeaway is that we probably do not want this for all type classes.
GetElemclass has HO out-params which can only be filled in by doing lazy delta reduction on instances. (Though we could conceivably put the domain into a field instead of an out-param).Fintypeclass has simp lemmas that match on instances, e.g.@Fintype.card p (ofFinset s H) = s.card. Here we shouldn't unfoldofFinset.Flat structures
That is, do not use subobjects for class inheritance in the algebraic hierarchy. @eric-wieser tried this in leanprover-community/mathlib4#3171
While using flat structures removes the need for eta for instances, this ultimately ran into very similar unification issues.
Short-circuit failures in nested TC synthesis
The reason we backtrack so much when unifying
LinearOrderedRing.toMul ?ring =?= instMulis because we cannot synthesize?ring. Otherwise we would succeed quickly. On the other hand, we cannot expect to solve this unification problem without synthesizing?ringeither, so it makes sense to abort unification when nested TC synthesis fails. @Kha tried this in Kha@8f887fdSurprisingly, this didn't break anything in mathlib. The change improves performance by 5%.
Generalizing instance subterms during TC synthesis
This adds an inprocessing step during TC synthesis, replacing
@NoZeroDivisors T instMul instZeroby@NoZeroDivisors T ?m ?n. That generalization is not only great for speeding up unification, but also for caching since it normalizes the terms.There are some problems with this approach:
Module R (NormedAddGroupHom V₁ V₂)with big type-class instances inside the arguments.Prototype.
Generalizing instance subterms when matching
This is similar in spirit to the above, but we generalize all type-class instance subterms in the head of the instance when we apply it to a subgoal. That is we turn
NoZeroDivisors ?R (LinearOrderedRing.toMul ?inst) (LinearOrderedRing.toZero ?inst)intoNoZeroDivisors ?R ?m ?njust before matching.Like the above, this is only a partial fix since we'd need to do the same in simp/aesop/etc. as well.
Prototype.
Generalizing instance subterms (userspace edition)
Instead of generalizing the instance subterms during TC synthesis, we can also preprocess the instances themselves. For example by turning
[inst : LinearOrderedRing R] → NoZeroDivisors R (LinearOrderedRing.toMul inst) (LinearOrderedRing.toZero inst)into[inst : LinearOrderedRing R] → [inst2 : Mul R] → [inst3 : Zero R] → [Commutes inst2 (LinearOrderedRing.toMul inst)] → [Commutes inst3 (LinearOrderedRing.toZero inst)] → NoZeroDivisors R inst2 inst3. (WhereCommutesis the type-class version ofEq).The main downside is that this only really works for type-classes in
Propsince it adds anEq.recto the instance. So it is not enough to enable eta, as it doesn't help withSemiring { x // 0 ≤ x }, which still times out.leanprover-community/mathlib4#3042
Hot air alternatives
Postponed type class equality constraints
We only get into this issue in the first place because we need to unify type class instance terms before filling in the other metavariables. So what if we don't unify them, or at least later?
Concretely, whenever we encounter a unification problem like
LinearOrderedRing.toMul ?ring =?= instMul, we put it in a list and proceed as if it was defeq (instances are supposed to be defeq after all!).The calling module could then handle the postponed constraints at an appropriate time. Type-class synthesis would check them after the other subgoals have been finished (effectively it would turn most nested TC calls into regular TC subgoals). The term elaborator could postpone them alongside the other synthetic metavariables. Simp would check them after synthesizing the arguments to the simp lemma.
The eager unification also causes some user-visible issues right now. For example you cannot combine some lemmas if the types are not known:
No lazy delta reduction for projections / instances / reducible definitions
The key ingredient for the performance issue is lazy delta and the resulting exponential number of subproblems. If we eagerly reduce all the type-class indirections, then there's obviously no more blowup.
By only doing this for reducible definitions, we give a bit of control to the user. Functions like
Fintype.ofFinsetwhich should be matched using lazy delta can then simply be markeddefinstead ofabbrev.Unification hints
Some of these failing unification problems actually have (nonanalytic) solutions; e.g.
CommMonoid.toMul ?a =?= Group.toMul ?bcan be solved by assigning?a := CommGroup.toCommMonoid ?cand?b := CommGroup.toGroup ?c. We could conceivably encode these blanket solutions using unification hints.There are several issues here from what I can tell:
Group).LinearOrderedRing.toMul ?inst =?= instNatMulhas no solutions.CommGroup.toGroup ?c, which messes with the "skip already assigned subgoals" heuristic in TC search.