type class resolution fail

Stream: Is there code for X?

[Asei Inoue]

set_option autoImplicit false
set_option relaxedAutoImplicit false

class Base (α : Type) where
  base : α

class Left (α : Type) extends Base α where
  left : α

class Right (α : Type) extends Base α where
  right : α

class Both (α : Type) extends Left α, Right α

inductive Direction where
  | south
  | north
  | west
  | east

instance : Base Direction where
  base := Direction.south

instance : Left Direction where
  left := Direction.west

instance : Right Direction where
  right := Direction.east

-- question: why this fails? how can I fix this?
/--
error: failed to synthesize
  Both Direction
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#check (inferInstance : Both Direction)

[Asei Inoue]

I think this is caused by diamond problem...

[Asei Inoue]

impossible to solve?

[Daniel Weber]

You're simply missing an instance:

instance (α : Type) [Left α] [Right α] : Both α where
  left := Left.left
  right := Right.right

[Asei Inoue]

You're simply missing an instance:

my original code is here. why type mismatch occurs?

set_option autoImplicit false
set_option relaxedAutoImplicit false

class PartialOrder (α : Type) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := fun a b => a ≤ b ∧ ¬ b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a := by intros; rfl
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b

section Lattice

class Sup (α : Type) where

  sup : α → α → α

class Inf (α : Type) where
  inf : α → α → α

@[inherit_doc] infixl:68 " ⊔ " => Sup.sup

@[inherit_doc] infixl:69 " ⊓ " => Inf.inf

class SemilatticeSup (α : Type) extends Sup α, PartialOrder α where
  le_sup_left : ∀ a b : α, a ≤ a ⊔ b

  le_sup_right : ∀ a b : α, b ≤ a ⊔ b

  sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c

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

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

instance (α : Type) [Semilatticeinf α] [SemilatticeSup α] : Lattice α where
  /-
  type mismatch
    Semilatticeinf.inf_le_left
  has type
    ∀ (a b : α), a ⊓ b ≤ a : Prop
  but is expected to have type
    ∀ (a b : α), a ⊓ b ≤ a : Prop
  -/
  inf_le_left := Semilatticeinf.inf_le_left (α := α)

end Lattice

[Daniel Weber]

Oh, yeah, there's a diamond there, as the order given by the Semilatticeinf is unrelated to the one given by the SemilatticeSup.

[Asei Inoue]

as the order given by the Semilatticeinf is unrelated to the one given by the SemilatticeSup.

Oh... how to solve this?

[Asei Inoue]

.... Since I have copied Mathlib's definition of Lattice, does Mathlib's Lattice also have the diamond problem?

[Yaël Dillies]

There is no problem in mathlib because there is no SemilatticeInf -> SemilatticeSup -> Lattice instance

[Asei Inoue]

that’s interesting. how to show Lattice instance in mathlib?

[Yaël Dillies]

If you have a concrete type which is both a SemilatticeInf and a SemilatticeSup, then you are supposed to do to get

instance : Lattice MyType where
  __ := MyType.semilatticeSup
  __ := MyType.semilatticeInf

[Asei Inoue]

This fails.

instance : Lattice Prop where
  /-
  '__' is not a field of structure 'Lattice'
  -/
  __ := Prop.SemilatticeSup
  __ := Prop.Semilatticeinf

[Yaël Dillies]

Do import Mathlib.Tactic.Common

[Asei Inoue]

it still fails...

instance : Lattice Prop where
  /-
  expected structure
  -/
  /-
  unknown identifier 'Prop.SemilatticeSup'
  -/
  __ := Prop.SemilatticeSup
  __ := Prop.Semilatticeinf

[Yaël Dillies]

Well, have you looked up how the instances were called?

[Yaël Dillies]

In fact, there is no instance of SemilatticeSup Prop or SemilatticeInf Prop. They are derived from the DistribLattice Prop instance

[Asei Inoue]

is this the best way?

instance : Lattice Prop where
  le_sup_left := by
    intro a b
    exact Or.inl
  le_sup_right := by
    intro a b
    exact Or.inr
  sup_le := by
    intro a b c hac hbc
    exact fun h => h.elim hac hbc
  inf_le_left := by
    intro a b
    exact And.left
  inf_le_right := by
    intro a b
    exact And.right
  le_inf := by
    intro a b c hac hbc
    dsimp [LE.le, Inf.inf] at *
    exact fun a => ⟨hac a, hbc a⟩

[Ruben Van de Velde]

More reliable than trying to guess names of instances is

import Mathlib

noncomputable instance : Lattice Prop where
  __ := (inferInstance : SemilatticeSup Prop)
  __ := (inferInstance : SemilatticeInf Prop)