Zulip Chat Archive

Stream: mathlib4

Topic: Order.Hom.Lattice


Matej Penciak (Jan 24 2023 at 21:56):

I started this PR (https://github.com/leanprover-community/mathlib4/pull/1636) a bit ago, and I've been looking at the issues on and off over the last few days.

I think most of the errors are coming from a bunch of the instances of RelHomClass not being inferred (starting around line 188). I've tried debugging the best I can, but someone who understand this stuff better than I should probably take a look.

There are some totally unhelpful error messages like

type mismatch
  map_top
has type
  ∀ (f : F), ↑f ⊤ = ⊤ : Prop
but is expected to have type
  ∀ (f : F), ↑f ⊤ = ⊤ : Prop

where if I hover over any given sub-expression all the types match up.

This is one of the files in the direction of Data.Complex.Basic, but it doesn't have a lot of immediate descendants so it's not blocking all that much right now.

Kevin Buzzard (Jan 24 2023 at 22:06):

set_option synthInstance.maxHeartbeats 2000
set_option trace.Meta.synthInstance true
-- See note [lower instance priority]
instance (priority := 100) BoundedLatticeHomClass.toBoundedOrderHomClass [Lattice α] [Lattice β]
    [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : BoundedOrderHomClass F α β :=
  let foo : OrderHomClass F α β := inferInstance
  sorry

gives

...
[resume] propagating (x_0 : Type _abstMVar.0) 
        (x_1 : Type _abstMVar.1) 
          (x_2 : Type _abstMVar.2) 
            (x_3 : Type _abstMVar.3) 
              (x_4 : Type _abstMVar.4) 
                (x_5 : Type _abstMVar.5) 
                  (x_6 : Type _abstMVar.6) 
                    (x_7 : Type _abstMVar.7) 
                      (x_8 : Type _abstMVar.8) 
                        (x_9 : Type _abstMVar.9) 
                          (x_10 : Type _abstMVar.10) 
                            (x_11 : Type _abstMVar.11) 
                              (x_12 : Type _abstMVar.12) 
                                (x_13 : Type _abstMVar.13) 
                                  (x_14 : Type _abstMVar.14) 
                                    (x_15 : Type _abstMVar.15) 
                                      (x_16 : Type _abstMVar.16) 
                                        (x_17 : Type _abstMVar.17) 
                                          (x_18 : Type _abstMVar.18) 
                                            Bot
                                              ((WithTop x_0)ᵒᵈ ×
                                                (WithTop x_1)ᵒᵈ ×
                                                  (WithTop x_2)ᵒᵈ ×
                                                    (WithTop x_3)ᵒᵈ ×
                                                      (WithTop x_4)ᵒᵈ ×
                                                        (WithTop x_5)ᵒᵈ ×
                                                          (WithTop x_6)ᵒᵈ ×
                                                            (WithTop x_7)ᵒᵈ ×
                                                              (WithTop x_8)ᵒᵈ ×
                                                                (WithTop x_9)ᵒᵈ ×
                                                                  (WithTop x_10)ᵒᵈ ×
                                                                    (WithTop x_11)ᵒᵈ ×
                                                                      (WithTop x_12)ᵒᵈ ×
                                                                        (WithTop x_13)ᵒᵈ ×
                                                                          (WithTop x_14)ᵒᵈ ×
                                                                            (WithTop x_15)ᵒᵈ ×
                                                                              (WithTop x_16)ᵒᵈ ×
                                                                                (WithTop x_17)ᵒᵈ ×
                                                                                  (WithTop
                                                                                      x_18)ᵒᵈ) to subgoal Bot
        ((WithTop ?m.21896)ᵒᵈ ×
          (WithTop ?m.21897)ᵒᵈ ×
            (WithTop ?m.21898)ᵒᵈ ×
              (WithTop ?m.21899)ᵒᵈ ×
                (WithTop ?m.21900)ᵒᵈ ×
                  (WithTop ?m.21901)ᵒᵈ ×
                    (WithTop ?m.21902)ᵒᵈ ×
                      (WithTop ?m.21903)ᵒᵈ ×
                        (WithTop ?m.21904)ᵒᵈ ×
                          (WithTop ?m.21905)ᵒᵈ ×
                            (WithTop ?m.21906)ᵒᵈ ×
                              (WithTop ?m.21907)ᵒᵈ ×
                                (WithTop ?m.21908)ᵒᵈ ×
                                  (WithTop ?m.21909)ᵒᵈ ×
                                    (WithTop ?m.21910)ᵒᵈ ×
                                      (WithTop ?m.21911)ᵒᵈ ×
                                        (WithTop ?m.21912)ᵒᵈ ×
                                          (WithTop ?m.21913)ᵒᵈ ×
                                            (WithTop
                                                ?m.21914)ᵒᵈ) of Bot
        ((WithTop ?m.21154)ᵒᵈ ×
          (WithTop ?m.21896)ᵒᵈ ×
            (WithTop ?m.21897)ᵒᵈ ×
              (WithTop ?m.21898)ᵒᵈ ×
                (WithTop ?m.21899)ᵒᵈ ×
                  (WithTop ?m.21900)ᵒᵈ ×
                    (WithTop ?m.21901)ᵒᵈ ×
                      (WithTop ?m.21902)ᵒᵈ ×
                        (WithTop ?m.21903)ᵒᵈ ×
                          (WithTop ?m.21904)ᵒᵈ ×
                            (WithTop ?m.21905)ᵒᵈ ×
                              (WithTop ?m.21906)ᵒᵈ ×
                                (WithTop ?m.21907)ᵒᵈ ×
                                  (WithTop ?m.21908)ᵒᵈ ×
                                    (WithTop ?m.21909)ᵒᵈ ×
                                      (WithTop ?m.21910)ᵒᵈ ×
                                        (WithTop ?m.21911)ᵒᵈ ×
                                          (WithTop ?m.21912)ᵒᵈ × (WithTop ?m.21913)ᵒᵈ × (WithTop ?m.21914)ᵒᵈ) 
  [resume] propagating (x_0 : Type _abstMVar.0) 
        (x_1 : Type _abstMVar.1) 
          (x_2 : Type _abstMVar.2) 
            (x_3 : Type _abstMVar.3) 
...

Kevin Buzzard (Jan 24 2023 at 22:07):

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slow.20.60positivity.60/near/322871598

Kevin Buzzard (Jan 24 2023 at 22:13):

Just telling Lean how to do it works:

instance (priority := 100) BoundedLatticeHomClass.toBoundedOrderHomClass [Lattice α] [Lattice β]
    [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : BoundedOrderHomClass F α β :=
{ show OrderHomClass F α β from SupHomClass.toOrderHomClass, BoundedLatticeHomClass F α β with }

Kevin Buzzard (Jan 24 2023 at 22:16):

This isn't going to end well either:

  [resume] propagating Lattice α to subgoal Lattice α of Lattice (WithTop α) 
  [resume] propagating Lattice (WithTop α) to subgoal Lattice (WithTop α) of Lattice (WithTop (WithTop α)) 
  [resume] propagating Lattice
        (WithTop (WithTop α)) to subgoal Lattice (WithTop (WithTop α)) of Lattice (WithTop (WithTop (WithTop α))) 
  [resume] propagating Lattice
        (WithTop
          (WithTop
            (WithTop
              α))) to subgoal Lattice
        (WithTop (WithTop (WithTop α))) of Lattice (WithTop (WithTop (WithTop (WithTop α)))) 
  [resume] propagating Lattice
        (WithTop
          (WithTop
            (WithTop
              (WithTop
                α)))) to subgoal Lattice
        (WithTop (WithTop (WithTop (WithTop α)))) of Lattice (WithTop (WithTop (WithTop (WithTop (WithTop α))))) 
  [resume] propagating Lattice

Kevin Buzzard (Jan 24 2023 at 22:38):

Here's the behaviour on master:

import Mathlib.Order.Hom.Basic

class SupHomClass (F : Type _) (α β : outParam <| Type _) [HasSup α] [HasSup β] extends
  FunLike F α fun _ => β where
  map_sup (f : F) (a b : α) : f (a  b) = f a  f b

class LatticeHomClass (F : Type _) (α β : outParam <| Type _) [Lattice α] [Lattice β] extends
  SupHomClass F α β where
  map_inf (f : F) (a b : α) : f (a  b) = f a  f b

class BoundedLatticeHomClass (F : Type _) (α β : outParam <| Type _) [Lattice α] [Lattice β]
  [BoundedOrder α] [BoundedOrder β] extends LatticeHomClass F α β where
  map_top (f : F) : f  = 
  map_bot (f : F) : f  = 

instance (priority := 100) SupHomClass.toOrderHomClass [SemilatticeSup α] [SemilatticeSup β]
    [SupHomClass F α β] : OrderHomClass F α β :=
  { SupHomClass F α β with
    map_rel := fun f a b h => by rw [ sup_eq_right,  map_sup, sup_eq_right.2 h] }

example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    OrderHomClass F α β :=
SupHomClass.toOrderHomClass -- works

set_option synthInstance.maxHeartbeats 400 in -- to stop huge outputs crashing VS code
set_option trace.Meta.synthInstance true in
example [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
    OrderHomClass F α β :=
inferInstance -- loops

Kevin Buzzard (Jan 24 2023 at 22:41):

People who understand these traces better than me can usually stare at the output below and instantly go "it went wrong at precisely this point and that's your bad instance".

[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
  [] new goal RelHomClass F _tc.2 _tc.3 
  []  apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
  []  apply @WithTop.semilatticeSup to SemilatticeSup (WithTop ?m.2939) 
  []  apply Prod.semilatticeSup to SemilatticeSup (?m.2943 × ?m.2944) 
  []  apply @WithTop.semilatticeSup to SemilatticeSup (WithTop ?m.2956) 
  []  apply Prod.semilatticeSup to SemilatticeSup (?m.2960 × ?m.2961) 
  []  apply OrderDual.semilatticeSup to SemilatticeSup ?m.2965ᵒᵈ 
  []  apply @WithTop.semilatticeInf to SemilatticeInf (WithTop ?m.2976) 
  []  apply Prod.semilatticeInf to SemilatticeInf (?m.2980 × ?m.2981) 
  []  apply OrderDual.semilatticeInf to SemilatticeInf ?m.2985ᵒᵈ 
  []  apply @WithBot.semilatticeInf to SemilatticeInf (WithBot ?m.2988) 
  []  apply @Pi.semilatticeInf to SemilatticeInf ((i : ?m.2991)  ?m.2992 i) 
  []  apply @WithTop.semilatticeInf to (i : ?m.2991)  SemilatticeInf (WithTop (?m.3006 i)) 
  []  apply Prod.semilatticeInf to (i : ?m.2991)  SemilatticeInf (?m.3015 i × ?m.3016 i) 
  []  apply OrderDual.semilatticeInf to (i : ?m.2991)  SemilatticeInf (?m.3025 i)ᵒᵈ 
  []  apply @WithTop.semilatticeSup to (i : ?m.2991)  SemilatticeSup (WithTop (?m.3042 i)) 
  []  apply Prod.semilatticeSup to (i : ?m.2991)  SemilatticeSup (?m.3051 i × ?m.3052 i) 
  []  apply OrderDual.semilatticeSup to (i : ?m.2991)  SemilatticeSup (?m.3061 i)ᵒᵈ 
  []  apply @WithBot.semilatticeSup to (i : ?m.2991)  SemilatticeSup (WithBot (?m.3069 i)) 
  []  apply @Pi.semilatticeSup to (i : ?m.2991)  SemilatticeSup ((i_1 : ?m.3077 i)  ?m.3078 i i_1) 
  []  apply @WithTop.semilatticeSup to (i : ?m.2991)  (i_1 : ?m.3077 i)  SemilatticeSup (WithTop (?m.3098 i i_1)) 
  []  apply Prod.semilatticeSup to (i : ?m.2991)  (i_1 : ?m.3077 i)  SemilatticeSup (?m.3112 i i_1 × ?m.3113 i i_1) 
  []  apply OrderDual.semilatticeSup to (i : ?m.2991)  (i_1 : ?m.3077 i)  SemilatticeSup (?m.3127 i i_1)ᵒᵈ 
  []  apply @WithTop.semilatticeInf to (i : ?m.2991)  (i_1 : ?m.3077 i)  SemilatticeInf (WithTop (?m.3150 i i_1)) 
  []  apply Prod.semilatticeInf to (i : ?m.2991)  (i_1 : ?m.3077 i)  SemilatticeInf (?m.3164 i i_1 × ?m.3165 i i_1) 
  []  apply OrderDual.semilatticeInf to (i : ?m.2991)  (i_1 : ?m.3077 i)  SemilatticeInf (?m.3179 i i_1)ᵒᵈ 
  []  apply @WithBot.semilatticeInf to (i : ?m.2991)  (i_1 : ?m.3077 i)  SemilatticeInf (WithBot (?m.3192 i i_1)) 
  []  apply @Pi.semilatticeInf to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  SemilatticeInf ((i_2 : ?m.3205 i i_1)  ?m.3206 i i_1 i_2) 
  []  apply @WithTop.semilatticeInf to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeInf (WithTop (?m.3232 i i_1 i_2)) 
  []  apply Prod.semilatticeInf to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeInf (?m.3251 i i_1 i_2 × ?m.3252 i i_1 i_2) 
  []  apply OrderDual.semilatticeInf to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeInf (?m.3271 i i_1 i_2)ᵒᵈ 
  []  apply @WithTop.semilatticeSup to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeSup (WithTop (?m.3300 i i_1 i_2)) 
  []  apply Prod.semilatticeSup to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeSup (?m.3319 i i_1 i_2 × ?m.3320 i i_1 i_2) 
  []  apply OrderDual.semilatticeSup to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeSup (?m.3339 i i_1 i_2)ᵒᵈ 
  []  apply @WithBot.semilatticeSup to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeSup (WithBot (?m.3357 i i_1 i_2)) 
  []  apply @Pi.semilatticeSup to (i : ?m.2991) 
        (i_1 : ?m.3077 i)  (i_2 : ?m.3205 i i_1)  SemilatticeSup ((i_3 : ?m.3375 i i_1 i_2)  ?m.3376 i i_1 i_2 i_3) 
  []  apply @WithTop.semilatticeSup to (i : ?m.2991) 
        (i_1 : ?m.3077 i) 
          (i_2 : ?m.3205 i i_1)  (i_3 : ?m.3375 i i_1 i_2)  SemilatticeSup (WithTop (?m.3408 i i_1 i_2 i_3)) 

Kevin Buzzard (Jan 24 2023 at 22:42):

@Mario Carneiro you're one of those people ;-)

Kevin Buzzard (Jan 24 2023 at 22:43):

Is it this?

[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
  [] new goal RelHomClass F _tc.2 _tc.3 
    [instances] #[@OrderIsoClass.toOrderHomClass, @SupHomClass.toOrderHomClass]
  []  apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
    [tryResolve]  RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1  RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1
    [] new goal SemilatticeSup _tc.0 
      [instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]
  []  apply @WithTop.semilatticeSup to SemilatticeSup (WithTop ?m.2939) 
    [tryResolve]  SemilatticeSup (WithTop ?m.2939)  SemilatticeSup (WithTop ?m.2939)

Kevin Buzzard (Jan 24 2023 at 22:45):

/-- `RelHomClass F r s` asserts that `F` is a type of functions such that all `f : F`
satisfy `r a b → s (f a) (f b)`.

The relations `r` and `s` are `outParam`s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
-/
class RelHomClass (F : Type _) {α β : outParam <| Type _} (r : outParam <| α  α  Prop)
  (s : outParam <| β  β  Prop) extends FunLike F α fun _ => β where
  /-- A `RelHomClass` sends related elements to related elements -/
  map_rel :  (f : F) {a b}, r a b  s (f a) (f b)

Mario Carneiro (Jan 24 2023 at 22:45):

It looks like the SemilatticeSup α goal in SupHomClass.toOrderHomClass is not being treated like an out-param

Kevin Buzzard (Jan 24 2023 at 22:46):

@SupHomClass.toOrderHomClass : {α : Type u_1} 
  {β : Type u_2} 
    {F : Type u_3} 
      [inst : SemilatticeSup α]  [inst_1 : SemilatticeSup β]  [inst_2 : SupHomClass F α β]  OrderHomClass F α β

No mention of outparams there

Mario Carneiro (Jan 24 2023 at 22:47):

it looks like lean4#1852

Kevin Buzzard (Jan 24 2023 at 22:48):

Can you explain more precisely what this means? I only have the vaguest concept of what an out-param is.

Kevin Buzzard (Jan 24 2023 at 22:48):

this is all to do with when...unification?...tries to fill in a hole?

Mario Carneiro (Jan 24 2023 at 22:49):

Specifically, we have the goal OrderHomClass F ?α ?β (where ?α, ?β are forcibly made into metavariables because they are outparams) and want to find a solution to the typeclass problem which will determine ?α, ?β

Mario Carneiro (Jan 24 2023 at 22:50):

SemilatticeSup α does not have α as an outparam, so it would be a bad idea to do a typeclass search for SemilatticeSup ?α immediately, because that will enumerate all semilattices

Kevin Buzzard (Jan 24 2023 at 22:50):

which it's doing, right?

Mario Carneiro (Jan 24 2023 at 22:50):

right

Kevin Buzzard (Jan 24 2023 at 22:51):

instance (priority := 100) SupHomClass.toOrderHomClass [outparam (SemilatticeSup α)] [SemilatticeSup β]
    [SupHomClass F α β] : OrderHomClass F α β :=
  { SupHomClass F α β with
    map_rel := fun f a b h => by rw [ sup_eq_right,  map_sup, sup_eq_right.2 h] }
/-
invalid binder annotation, type is not a class instance
  ?m.1448
use the command `set_option checkBinderAnnotations false` to disable the check
-/

Mario Carneiro (Jan 24 2023 at 22:51):

The correct order of evaluation here is:

  1. SupHomClass F ?α ?β, which solves ?α := α and ?β := β
  2. SemilatticeSup α
  3. SemilatticeSup β

Mario Carneiro (Jan 24 2023 at 22:52):

you misspelled outParam

Mario Carneiro (Jan 24 2023 at 22:52):

it would be great if that worked, if only as a workaround, but I think that outparam annotations are ignored on instances

Kevin Buzzard (Jan 24 2023 at 22:54):

instance (priority := 100) SupHomClass.toOrderHomClass  {α β : outParam <| Type _} [outParam (SemilatticeSup α)] [outParam (SemilatticeSup β)]
    [outParam (SupHomClass F α β)] : OrderHomClass F α β :=
  { SupHomClass F α β with
    map_rel := fun f a b h => by rw [ sup_eq_right,  map_sup, sup_eq_right.2 h] }

This doesn't fix it

Mario Carneiro (Jan 24 2023 at 22:55):

Gabriel's workaround is to use {_ : SemilatticeSup α} in the instance, but I think that won't work here because SupHomClass requires HasSup instead of SemilatticeSup

Kevin Buzzard (Jan 24 2023 at 23:00):

I don't understand why this is happening

[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
  [] new goal RelHomClass F _tc.2 _tc.3 
    [instances] #[@OrderIsoClass.toOrderHomClass, @SupHomClass.toOrderHomClass]
  []  apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
    [tryResolve]  RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1  RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1
    [] new goal outParam (SemilatticeSup _tc.0) 
      [instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]

when we have this

RelHomClass : Type u_1 
  {α : outParam (Type u_2)} 
    {β : outParam (Type u_3)}  outParam (α  α  Prop)  outParam (β  β  Prop)  Type (max (max u_1 u_2) u_3)

Oh! The outParam falls off in this trace:

[Meta.synthInstance] 💥 RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
  [] new goal RelHomClass F _tc.2 _tc.3 
    [instances] #[@OrderIsoClass.toOrderHomClass, @SupHomClass.toOrderHomClass]
  []  apply @SupHomClass.toOrderHomClass to RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1 
    [tryResolve]  RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1  RelHomClass F (fun x x_1 => x  x_1) fun x x_1 => x  x_1
    [] new goal outParam (SemilatticeSup _tc.0) 
      [instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]
  []  apply @WithTop.semilatticeSup to outParam (SemilatticeSup (WithTop ?m.2962)) 
    [tryResolve]  outParam (SemilatticeSup (WithTop ?m.2962))  SemilatticeSup (WithTop ?m.2962)
    [] new goal SemilatticeSup _tc.0 
      [instances] #[@Lattice.toSemilatticeSup, @Pi.semilatticeSup, @WithBot.semilatticeSup, OrderDual.semilatticeSup, Prod.semilatticeSup, @WithTop.semilatticeSup]

The new goal was outParam (SemilatticeSup _tc.0) and then it became SemilatticeSup _tc.0

Mario Carneiro (Jan 24 2023 at 23:01):

outParam isn't really a tag on goals, it's a tag on arguments to a typeclass

Mario Carneiro (Jan 24 2023 at 23:01):

when it shows up elsewhere it's just a thing to be unfolded

Kevin Buzzard (Jan 24 2023 at 23:11):

What needs to be changed to make type class inference not try to solve SemilatticeSup _tc.0? Is this something which can be fixed in mathlib or does it need a change in core Lean? Do we need a new meme?

Kevin Buzzard (Jan 24 2023 at 23:27):

instance (priority := 100) SupHomClass.toOrderHomClass {α β : outParam <| Type _} [outParam (SemilatticeSup α)] [outParam (SemilatticeSup β)]
    [outParam (SupHomClass F α β)] : OrderHomClass F α β :=
  { SupHomClass F α β with
    map_rel := fun f a b h => by rw [ sup_eq_right,  map_sup, sup_eq_right.2 h] }

This doesn't fix it.

Mario Carneiro (Jan 24 2023 at 23:46):

It's a core lean issue. Maybe @Gabriel Ebner has some ideas?

Gabriel Ebner (Jan 24 2023 at 23:48):

I didn't look through the whole thread yet. Does using {} instead of [] on the out-params help? Note that SupHomClass should not be an outparam.

Kevin Buzzard (Jan 25 2023 at 12:09):

Aah, in fact

instance (priority := 100) SupHomClass.toOrderHomClass {α β : outParam <| Type _}
  {_ : outParam (SemilatticeSup α)} {_ : outParam (SemilatticeSup β)}
    [SupHomClass F α β] : OrderHomClass F α β :=
  { SupHomClass F α β with
    map_rel := fun f a b h => by rw [ sup_eq_right,  map_sup, sup_eq_right.2 h] }

does fix the problem. This is the "bandaid" approach as described in lean4#1901 right? @Matej Penciak this is at least a temporary fix.


Last updated: Dec 20 2023 at 11:08 UTC