Type mismatch with spread/where notation

Stream: mathlib4

[Yaël Dillies]

Here is an (almost mathlib-free) minimisation of the error I am hitting at #10560. I would greatly appreciate some help.

[Yaël Dillies]

import Mathlib.Tactic.Common
import Mathlib.Init.Set
import Mathlib.Order.Notation
import Mathlib.Init.Order.Defs

open Function

variable {α : Type*}

def OrderDual (α : Type*) : Type _ := α

notation:max α "ᵒᵈ" => OrderDual α

namespace OrderDual

instance [LE α] : LE αᵒᵈ := ⟨fun x y : α ↦ y ≤ x⟩
instance [LT α] : LT αᵒᵈ := ⟨fun x y : α ↦ y < x⟩

instance instPreorder [Preorder α] : Preorder αᵒᵈ where
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_le := sorry

instance instPartialOrder [PartialOrder α] : PartialOrder αᵒᵈ where
  __ := inferInstanceAs (Preorder αᵒᵈ)
  le_antisymm := sorry

instance instLinearOrder [LinearOrder α] : LinearOrder αᵒᵈ where
  __ := inferInstanceAs (PartialOrder αᵒᵈ)
  max := fun a b ↦ (min a b : α)
  min := fun a b ↦ (max a b : α)
  le_total := sorry
  min_def := sorry
  max_def := sorry
  decidableLE := sorry
  decidableLT := sorry

end OrderDual

variable {α : Type*}

namespace OrderDual

def toDual : α → αᵒᵈ := id
def ofDual : αᵒᵈ → α := id

end OrderDual

variable {α : Type}

class SemilatticeSup (α : Type) extends Sup α, PartialOrder α where
  protected le_sup_left : ∀ a b : α, a ≤ a ⊔ b
  protected le_sup_right : ∀ a b : α, b ≤ a ⊔ b
  protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c

instance OrderDual.instSup (α : Type) [Inf α] : Sup αᵒᵈ := ⟨((· ⊓ ·) : α → α → α)⟩
instance OrderDual.instInf (α : Type) [Sup α] : Inf αᵒᵈ := ⟨((· ⊔ ·) : α → α → α)⟩

class SemilatticeInf (α : Type) extends Inf α, PartialOrder α where
  protected inf_le_left : ∀ a b : α, a ⊓ b ≤ a
  protected inf_le_right : ∀ a b : α, a ⊓ b ≤ b
  protected le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c

instance OrderDual.instSemilatticeSup [SemilatticeInf α] : SemilatticeSup αᵒᵈ where
  __ := inferInstanceAs (PartialOrder αᵒᵈ)
  __ := inferInstanceAs (Sup αᵒᵈ)
  le_sup_left := sorry
  le_sup_right := sorry
  sup_le := sorry

instance OrderDual.instSemilatticeInf [SemilatticeSup α] : SemilatticeInf αᵒᵈ where
  __ := inferInstanceAs (PartialOrder αᵒᵈ)
  __ := inferInstanceAs (Inf αᵒᵈ)
  inf_le_left := sorry
  inf_le_right := sorry
  le_inf := sorry

[Yaël Dillies]

class Lattice (α : Type) extends SemilatticeSup α, SemilatticeInf α

instance OrderDual.instLattice [Lattice α] : Lattice αᵒᵈ where
  __ := instSemilatticeSup
  __ := instSemilatticeInf

class DistribLattice (α) extends Lattice α where
  protected le_sup_inf : ∀ x y z : α, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

instance OrderDual.instDistribLattice [DistribLattice α] : DistribLattice αᵒᵈ where
  __ := inferInstanceAs (Lattice αᵒᵈ)
  le_sup_inf := sorry

abbrev DistribLattice.ofInfSupLe [Lattice α]
    (inf_sup_le : ∀ a b c : α, a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c) : DistribLattice α where
  le_sup_inf := sorry

instance (priority := 100) LinearOrder.toLattice {α : Type} [o : LinearOrder α] : Lattice α where
  __ := o
  sup := max
  inf := min
  le_sup_left := sorry
  le_sup_right := sorry
  sup_le := sorry
  inf_le_left := sorry
  inf_le_right := sorry
  le_inf := sorry

class OrderTop (α : Type) [LE α] extends Top α where
  le_top : ∀ a : α, a ≤ ⊤

class OrderBot (α : Type) [LE α] extends Bot α where
  bot_le : ∀ a : α, ⊥ ≤ a

instance OrderDual.instTop [Bot α] : Top αᵒᵈ := ⟨(⊥ : α)⟩
instance OrderDual.instBot [Top α] : Bot αᵒᵈ := ⟨(⊤ : α)⟩

instance OrderDual.instOrderTop [LE α] [OrderBot α] : OrderTop αᵒᵈ where
  __ := inferInstanceAs (Top αᵒᵈ)
  le_top := sorry

instance OrderDual.instOrderBot [LE α] [OrderTop α] : OrderBot αᵒᵈ where
  __ := inferInstanceAs (Bot αᵒᵈ)
  bot_le := sorry

class BoundedOrder (α : Type) [LE α] extends OrderTop α, OrderBot α

instance OrderDual.instBoundedOrder (α : Type) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ where
  __ := inferInstanceAs (OrderTop αᵒᵈ)
  __ := inferInstanceAs (OrderBot αᵒᵈ)

open Function OrderDual

variable {ι α β : Type}

class GeneralizedHeytingAlgebra (α : Type) extends Lattice α, OrderTop α, HImp α where
  le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
#align generalized_heyting_algebra GeneralizedHeytingAlgebra
#align generalized_heyting_algebra.to_order_top GeneralizedHeytingAlgebra.toOrderTop

class GeneralizedCoheytingAlgebra (α : Type) extends Lattice α, OrderBot α, SDiff α where
  sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c
#align generalized_coheyting_algebra GeneralizedCoheytingAlgebra
#align generalized_coheyting_algebra.to_order_bot GeneralizedCoheytingAlgebra.toOrderBot

class HeytingAlgebra (α : Type) extends GeneralizedHeytingAlgebra α, OrderBot α, HasCompl α where
  himp_bot (a : α) : a ⇨ ⊥ = aᶜ
#align heyting_algebra HeytingAlgebra

class CoheytingAlgebra (α : Type) extends GeneralizedCoheytingAlgebra α, OrderTop α, HNot α where
  top_sdiff (a : α) : ⊤ \ a = ￢a
#align coheyting_algebra CoheytingAlgebra

class BiheytingAlgebra (α : Type) extends HeytingAlgebra α, SDiff α, HNot α where
  sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c
  top_sdiff (a : α) : ⊤ \ a = ￢a

attribute [instance 100] GeneralizedHeytingAlgebra.toOrderTop
attribute [instance 100] GeneralizedCoheytingAlgebra.toOrderBot

instance (priority := 100) HeytingAlgebra.toBoundedOrder [HeytingAlgebra α] : BoundedOrder α :=
  { bot_le := ‹HeytingAlgebra α›.bot_le }

instance (priority := 100) CoheytingAlgebra.toBoundedOrder [CoheytingAlgebra α] : BoundedOrder α :=
  { ‹CoheytingAlgebra α› with }
#align coheyting_algebra.to_bounded_order CoheytingAlgebra.toBoundedOrder

instance (priority := 100) BiheytingAlgebra.toCoheytingAlgebra [BiheytingAlgebra α] :
    CoheytingAlgebra α :=
  { ‹BiheytingAlgebra α› with }

instance (priority := 100) GeneralizedHeytingAlgebra.toDistribLattice
    [GeneralizedHeytingAlgebra α] : DistribLattice α := DistribLattice.ofInfSupLe sorry

instance OrderDual.instGeneralizedCoheytingAlgebra [GeneralizedHeytingAlgebra α] :
    GeneralizedCoheytingAlgebra αᵒᵈ where
  sdiff a b := toDual (ofDual b ⇨ ofDual a)
  sdiff_le_iff a := sorry

instance (priority := 100) GeneralizedCoheytingAlgebra.toDistribLattice
    [GeneralizedCoheytingAlgebra α] : DistribLattice α where
  __ := ‹GeneralizedCoheytingAlgebra α›
  le_sup_inf := sorry

instance OrderDual.instGeneralizedHeytingAlgebra [GeneralizedCoheytingAlgebra α] :
    GeneralizedHeytingAlgebra αᵒᵈ where
  himp := sorry
  le_himp_iff := sorry

instance OrderDual.instCoheytingAlgebra [HeytingAlgebra α] : CoheytingAlgebra αᵒᵈ where
  hnot := toDual ∘ compl ∘ ofDual
  sdiff a b := toDual (ofDual b ⇨ ofDual a)
  sdiff_le_iff := sorry
  top_sdiff := sorry

instance (priority := 100) CoheytingAlgebra.toDistribLattice [CoheytingAlgebra α] :
    DistribLattice α where
  __ := ‹CoheytingAlgebra α›
  le_sup_inf := sorry

instance OrderDual.instHeytingAlgebra [CoheytingAlgebra α] : HeytingAlgebra αᵒᵈ where
  compl := toDual ∘ hnot ∘ ofDual
  himp := sorry
  le_himp_iff := sorry
  himp_bot := sorry

instance OrderDual.instBiheytingAlgebra [BiheytingAlgebra α] : BiheytingAlgebra αᵒᵈ where
  __ := instHeytingAlgebra
  __ := instCoheytingAlgebra

class GeneralizedBooleanAlgebra (α : Type) extends DistribLattice α, SDiff α, Bot α where
  sup_inf_sdiff : ∀ a b : α, a ⊓ b ⊔ a \ b = a
  inf_inf_sdiff : ∀ a b : α, a ⊓ b ⊓ a \ b = ⊥

instance (priority := 100) GeneralizedBooleanAlgebra.toOrderBot [GeneralizedBooleanAlgebra α] :
    OrderBot α where
  __ := GeneralizedBooleanAlgebra.toBot
  bot_le := sorry

instance (priority := 100) GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
    [GeneralizedBooleanAlgebra α] : GeneralizedCoheytingAlgebra α where
  __ := ‹GeneralizedBooleanAlgebra α›
  __ := GeneralizedBooleanAlgebra.toOrderBot
  sdiff := (· \ ·)
  sdiff_le_iff := sorry

class BooleanAlgebra (α : Type) extends
    DistribLattice α, HasCompl α, SDiff α, HImp α, Top α, Bot α where
  inf_compl_le_bot : ∀ x : α, x ⊓ xᶜ ≤ ⊥
  top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ
  le_top : ∀ a : α, a ≤ ⊤
  bot_le : ∀ a : α, ⊥ ≤ a
  sdiff := fun x y => x ⊓ yᶜ
  himp := fun x y => y ⊔ xᶜ
  sdiff_eq : ∀ x y : α, x \ y = x ⊓ yᶜ := by aesop
  himp_eq : ∀ x y : α, x ⇨ y = y ⊔ xᶜ := by aesop

instance (priority := 100) BooleanAlgebra.toGeneralizedBooleanAlgebra [BooleanAlgebra α] :
    GeneralizedBooleanAlgebra α where
  __ := ‹BooleanAlgebra α›
  sup_inf_sdiff := sorry
  inf_inf_sdiff := sorry
#align boolean_algebra.to_generalized_boolean_algebra BooleanAlgebra.toGeneralizedBooleanAlgebra

instance (priority := 100) BooleanAlgebra.toBiheytingAlgebra [BooleanAlgebra α] :
    BiheytingAlgebra α where
  __ := ‹BooleanAlgebra α›
  __ := GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
  hnot := compl
  le_himp_iff := sorry
  himp_bot := sorry
  top_sdiff a := sorry
#align boolean_algebra.to_biheyting_algebra BooleanAlgebra.toBiheytingAlgebra

instance OrderDual.instBooleanAlgebra [BooleanAlgebra α] : BooleanAlgebra αᵒᵈ where
  __ := instDistribLattice
  __ := instHeytingAlgebra
  sdiff_eq := sorry
  himp_eq := sorry
  inf_compl_le_bot a := sorry
  top_le_sup_compl a := sorry

open OrderDual

class CompleteSemilatticeSup (α : Type) extends PartialOrder α where
  le_sSup : True

class CompleteSemilatticeInf (α : Type) extends PartialOrder α where
  sInf_le : True

class CompleteLattice (α : Type) extends Lattice α, CompleteSemilatticeSup α,
  CompleteSemilatticeInf α, Top α, Bot α where
  protected le_top : ∀ x : α, x ≤ ⊤
  protected bot_le : ∀ x : α, ⊥ ≤ x

instance (priority := 100) CompleteLattice.toBoundedOrder [h : CompleteLattice α] :
    BoundedOrder α :=
  { h with }

class CompleteLinearOrder (α : Type) extends CompleteLattice α, BiheytingAlgebra α where
  le_total (a b : α) : a ≤ b ∨ b ≤ a
  decidableLE : DecidableRel (· ≤ · : α → α → Prop)
  decidableEq : DecidableEq α := @decidableEqOfDecidableLE _ _ decidableLE
  decidableLT : DecidableRel (· < · : α → α → Prop) := @decidableLTOfDecidableLE _ _ decidableLE

class Frame (α : Type) extends CompleteLattice α, HeytingAlgebra α where
  inf_sSup_le_iSup_inf (a : α) (s : Set α) : True

class Coframe (α : Type) extends CompleteLattice α, CoheytingAlgebra α where
  iInf_sup_le_sup_sInf (a : α) (s : Set α) : True

class CompleteDistribLattice (α) extends Frame α, Coframe α
class CompleteBooleanAlgebra (α) extends BooleanAlgebra α, CompleteDistribLattice α

instance OrderDual.instCompleteLattice [CompleteLattice α] : CompleteLattice αᵒᵈ where
  __ := instBoundedOrder α
  le_sSup := @CompleteLattice.sInf_le α _
  sInf_le := @CompleteLattice.le_sSup α _

instance OrderDual.instCoframe [Frame α] : Coframe αᵒᵈ where
  __ := instCompleteLattice
  __ := instCoheytingAlgebra
  iInf_sup_le_sup_sInf := @Frame.inf_sSup_le_iSup_inf α _

instance OrderDual.instFrame [Coframe α] : Frame αᵒᵈ where
  __ := instCompleteLattice
  __ := instHeytingAlgebra
  inf_sSup_le_iSup_inf := @Coframe.iInf_sup_le_sup_sInf α _

instance OrderDual.instCompleteDistribLattice [CompleteDistribLattice α] :
    CompleteDistribLattice αᵒᵈ where
  __ := instFrame
  __ := instCoframe

instance OrderDual.instCompleteBooleanAlgebra [CompleteBooleanAlgebra α] :
    CompleteBooleanAlgebra αᵒᵈ where
  __ := instBooleanAlgebra
  __ := instCompleteDistribLattice
/-
type mismatch
  Frame.himp_bot
has type
  ∀ (a : αᵒᵈ), a ⇨ ⊥ = aᶜ : Prop
but is expected to have type
  ∀ (a : αᵒᵈ), a ⇨ ⊥ = aᶜ : Prop
-/

[Yaël Dillies]

The terms Lean is complaining about are definitionally equal, as can be shown by explicitly constructing each field one by one rom the instances, so the errors has to be some metavariable mishandling in the spread notation

[Yaël Dillies]

... except that replacing the where/spread notation with { ... }/with notation results in the same error

[Yaël Dillies]

So I am a bit lost

[Kyle Miller]

Mathlib's spread syntax right now has a hack where each __ value is first defined using a custom let binding that makes them be "implementation detail" local variables, since these kinds of variable are automatically unfolded by simp. It's also done in such a way that these implementation detail local variables can be instances, unlike normal.

The reason for doing this is that it turns out mathlib was accidentally making use of the fact that terms before the with were being made available as instances (completely by accident), and this was discovered when the docs#Lean.Meta.Simp.Config.zetaDelta feature was introduced.

[Kyle Miller]

Some guesses:

• if a later term using spread notation could make use of a previous one as an instance (rather than synthesizing one from global instances), that could potentially cause an issue
• treat spread notation like something that uses a let: writing instBooleanAlgebra without specifying any of its implicit arguments could potentially cause an issue too

[Kyle Miller]

The transformation to keep in mind is that {__ := foo} is like let a := foo; {x := a.x, y := a.y}, so if you're relying on unification you have to hope that these a.x and a.y are considered in the correct order to unify metavariables and to unstick typeclass inference.

The fact that using with notation leads to the same error points to this sort of problem rather than details about how spread syntax works in mathlib — I thought I'd mention it just in case.

[Yaël Dillies]

Okay I see. Then my question becomes: Is this a bug?

[Yaël Dillies]

It's certainly unexpected that doing some (not so trivial, but still not super complicated) surgery on a typeclass hierarchy results in such super hard to fix unification failures. Genuinely, the only way I found to reliably fix the above was to specify each field by hand.

[Yaël Dillies]

It seems that using with over __ makes some bugs disappear but not all of them (which is consistent with your explanation)

[Kyle Miller]

Like I was saying, it could lead to an issue if you try to rely purely on unification. This works fine:

instance OrderDual.instCompleteBooleanAlgebra [CompleteBooleanAlgebra α] :
    CompleteBooleanAlgebra αᵒᵈ where
  __ := instBooleanAlgebra (α := αᵒᵈ)
  __ := instCompleteDistribLattice (α := αᵒᵈ)

[Kyle Miller]

Maybe the type argument for these instances should be explicit?

[Yaël Dillies]

Uh, that is annoying given that I've been campaigning for years to have implicit arguments for instances

[Yaël Dillies]

What about __ : BooleanAlgebra α := inferInstance?

[Kyle Miller]

Yaël Dillies said:

Uh, that is annoying given that I've been campaigning for years to have implicit arguments for instances

Why is that? I'm not sure I've ever known the reason.

[Kyle Miller]

(__ : ty := val should be relatively easy to implement)

[Kevin Buzzard]

I have never known the convention for implicit/explicit for instances, and I'm pretty convinced that my choices in my mathlib PRs in the past will have been random (and I'm not sure anyone ever pointed this out in review either). Do we / should we have a convention?

[Eric Wieser]

Kyle Miller said:

(__ : ty := val should be relatively easy to implement)

Especially since it already works, right?

[Kyle Miller]

Feel free to test it, but that's not implemented.

Worse, that's not valid syntax, so it's not actually easy since it would take core changes. The next best thing is __ := (instBooleanAlgebra : BooleanAlgebra αᵒᵈ), but at that point I'm wondering again why not have this argument be explicit. It seems to me that typeclass instances are the sorts of things where you would rather not rely on the expected type (and spread notation is really indirect for expected types and hard on Lean). With Lean 4 you can write instBooleanAlgebra .. for example if you want Yaël's version.

[Eric Wieser]

Kyle Miller said:

Feel free to test it, but that's not implemented.

import Mathlib.Tactic

instance : Semigroup Nat where
  __ : Mul Nat := inferInstance
  mul_assoc _ _ _ := sorry

works in the web editor

[Kyle Miller]

Ah, this doesn't:

instance : Semigroup Nat :=
  { __ : Mul Nat := inferInstance, mul_assoc _ _ _ := sorry }

[Eric Wieser]

Oh, I didn't realize __ was legal in {} at all

[Eric Wieser]

@Yaël Dillies, I think there is an instance diamond in your original?

instance OrderDual.instCompleteBooleanAlgebra [inst : CompleteBooleanAlgebra α] :
    CompleteBooleanAlgebra αᵒᵈ :=
  { instBooleanAlgebra (α := α),
    instCompleteDistribLattice (α := α) with
    himp_bot := fun a => by
      have := @himp_bot αᵒᵈ _ a
      convert this
      dsimp [instHeytingAlgebra, instBooleanAlgebra]
      congr! 3
      change inst.compl = inst.hnot
      rfl -- fails

      }

It looks like you accidentally added an unwanted field to CompleteBooleanAlgebra

[Kyle Miller]

__ is defined for {...} notation

[Kyle Miller]

According to Lean.Elab.Term.expandWhereStructInst, your example works because the letDecl __ : Mul Nat := inferInstance is transformed into __ := (inferInstance : Mul Nat) when creating the {} version.

[Kyle Miller]

(That's the function that also does the f x y z := v -> f := fun x y z => v transformation)

[Eric Wieser]

Kyle Miller said:

This works fine:

instance OrderDual.instCompleteBooleanAlgebra [CompleteBooleanAlgebra α] :
    CompleteBooleanAlgebra αᵒᵈ where
  __ := instBooleanAlgebra (α := αᵒᵈ)
  __ := instCompleteDistribLattice (α := αᵒᵈ)

These are the wrong argument values! They make terms of the form BooleanAlgebra αᵒᵈᵒᵈ.

[Yaël Dillies]

Eric Wieser said:

Yaël Dillies, I think there is an instance diamond in your original?

instance OrderDual.instCompleteBooleanAlgebra [inst : CompleteBooleanAlgebra α] :
    CompleteBooleanAlgebra αᵒᵈ :=
  { instBooleanAlgebra (α := α),
    instCompleteDistribLattice (α := α) with
    himp_bot := fun a => by
      have := @himp_bot αᵒᵈ _ a
      convert this
      dsimp [instHeytingAlgebra, instBooleanAlgebra]
      congr! 3
      change inst.compl = inst.hnot
      rfl -- fails

      }

It looks like you accidentally added an unwanted field to CompleteBooleanAlgebra

Yep, well spotted. My current design is to not ask for hnot when we know it is equal to compl (this happens in boolean algebras). However this means that forgetful inheritance instances out of boolean algebras must create the hnot field out of the compl one, which now seems problematic. Maybe, just maybe, someone has a type out there which is a biheyting algebra more generally than when it is a boolean algebra, and therefore wants to give different defeqs to compl and hnot.

[Yaël Dillies]

What do you think?

[Yaël Dillies]

If we push my reasoning, this means that boolean algebras must have a redundant hnot field

[Yaël Dillies]

Another funny issue is that linear orders are (mathematically) biheyting algebras, so we should also have LinearOrder extend BiheytingAlgebra, which would introduce a ton of fields most people don't care about

[Kim Morrison]

Please let's not make LinearOrder worse than it already is for now. :-)

[Eric Wieser]

Yaël Dillies said:

However this means that forgetful inheritance instances out of boolean algebras must create the hnot field out of the compl one, which now seems problematic

I think this is fine. I think this problem is like the sup/min thing for linear orders, where in Lean 3 we had to use renaming to ensure the fields got merged

[Eric Wieser]

So the solution here is either to:

• ask very nicely for renaming to return
• not use the extends keyword and perform the inheritance manually by copying all the fields (except hnot)

[Yaël Dillies]

Eric Wieser said:

this problem is like the sup/min thing for linear orders, where in Lean 3 we had to use renaming to ensure the fields got merged

Is it? In the case of linear orders, you still have the same amount of fields when going to a more specific class. In the case of going from biheyting algebras to boolean algebras, you lose a field

[Eric Wieser]

Remind me which of those two is the stronger typeclass?

[Yaël Dillies]

Boolean algebras. See docs#BooleanAlgebra.toBiheytingAlgebra

[Yaël Dillies]

Mathematically, a boolean algebra is a biheyting algebra where compl = hnot

[Eric Wieser]

I think this is only an issue if you have [BooleanAlgebra A] : BooleanAlgebra (F A) and [BiheytingAlgebra A] : BiheytingAlgebra (F A), and somehow these end up with different hnots on F A when the hnots on A are defeq

[Eric Wieser]

Certainly the problem in your PR can be solved by just not inheriting the hnot field

[Eric Wieser]

And I think today there is no such F in mathlib, and so a TODO speculating about issues if one were to exist is probably sufficient

[Yaël Dillies]

Okay then I'll adapt the PR to that