type mismatch error

Stream: general

[Johan Commelin]

I don't have a good strategy for debugging errors like this:

type mismatch at application
  galois_connection.l_supr opens.gc
term
  opens.gc
has type
  galois_connection subtype.val opens.interior
but is expected to have type
  galois_connection ?m_5 ?m_6

My initial reaction is: Hey Lean, look, you just figured out what ?m_5 and ?m_6 are. Unify, and move on.
But apparently Lean thinks otherwise...

[Kenny Lau]

I would set_option pp.all true, but that's me

[Johan Commelin]

I'll try, but I fear that I get something extremely long and complicated.

[Kenny Lau]

I'm not afraid of that

[Rob Lewis]

This pattern shows up a lot when there's a type class argument to galois_connection.l_supr that opens.gc doesn't satisfy.

[Johan Commelin]

Hmmm, it's even reasonable short:

type mismatch at application
  @galois_connection.l_supr.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6 ?m_7 ?m_8 ?m_9 ?m_10
    (@topological_space.opens.gc.{?l_11} ?m_12 ?m_13)
term
  @topological_space.opens.gc.{?l_1} ?m_2 ?m_3
has type
  @galois_connection.{?l_1 ?l_1}
    (@subtype.{(max (?l_1+1) 1)} (set.{?l_1} ?m_2) (λ (s : set.{?l_1} ?m_2), @is_open.{?l_1} ?m_2 ?m_3 s))
    (set.{?l_1} ?m_2)
    (@subtype.preorder.{?l_1} (set.{?l_1} ?m_2)
       (@partial_order.to_preorder.{?l_1} (set.{?l_1} ?m_2)
          (@lattice.order_bot.to_partial_order.{?l_1} (set.{?l_1} ?m_2)
             (@lattice.bounded_lattice.to_order_bot.{?l_1} (set.{?l_1} ?m_2)
                (@lattice.complete_lattice.to_bounded_lattice.{?l_1} (set.{?l_1} ?m_2)
                   (@set.lattice_set.{?l_1} ?m_2)))))
       (λ (s : set.{?l_1} ?m_2), @is_open.{?l_1} ?m_2 ?m_3 s))
    (@partial_order.to_preorder.{?l_1} (set.{?l_1} ?m_2)
       (@lattice.order_bot.to_partial_order.{?l_1} (set.{?l_1} ?m_2)
          (@lattice.bounded_lattice.to_order_bot.{?l_1} (set.{?l_1} ?m_2)
             (@lattice.complete_lattice.to_bounded_lattice.{?l_1} (set.{?l_1} ?m_2) (@set.lattice_set.{?l_1} ?m_2)))))
    (@subtype.val.{(max (?l_1+1) 1)} (set.{?l_1} ?m_2) (λ (s : set.{?l_1} ?m_2), @is_open.{?l_1} ?m_2 ?m_3 s))
    (@topological_space.opens.interior.{?l_1} ?m_2 ?m_3)
but is expected to have type
  @galois_connection.{?l_1 ?l_2} ?m_3 ?m_4
    (@partial_order.to_preorder.{?l_1} ?m_3
       (@lattice.order_bot.to_partial_order.{?l_1} ?m_3
          (@lattice.bounded_lattice.to_order_bot.{?l_1} ?m_3
             (@lattice.complete_lattice.to_bounded_lattice.{?l_1} ?m_3 ?m_5))))
    (@partial_order.to_preorder.{?l_2} ?m_4
       (@lattice.order_bot.to_partial_order.{?l_2} ?m_4
          (@lattice.bounded_lattice.to_order_bot.{?l_2} ?m_4
             (@lattice.complete_lattice.to_bounded_lattice.{?l_2} ?m_4 ?m_6))))

[Johan Commelin]

@Rob Lewis That's probably what's going on here.

[Kenny Lau]

when I can't handle it, I use https://text-compare.com

[Kenny Lau]

and in some rare cases it's some universe issues

[Johan Commelin]

Otoh, I think all typeclass instances ought to be satisfied.

[Johan Commelin]

@Kenny Lau There are two sorrys in sheaf.lean. They are math-trivial, but I find them Lean-hard.

[Kenny Lau]

link?

[Johan Commelin]

If you have some time, I would be really happy if you could take a look.

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean#L262

[Kenny Lau]

I think you have a rather different definition of "math-trivial"

[Johan Commelin]

What this is saying is, you've got an open set V and a cover Us of an open set U. And V ⊆ U.

[Johan Commelin]

Now you intersect all the Ui in Us with V, and the result covers V.

[Kenny Lau]

can you show me the context?

[Johan Commelin]

You mean explain the context?

[Kenny Lau]

no, the context

[Johan Commelin]

Aaah

[Johan Commelin]

X : Type u,
_inst_1 : topological_space X,
U V : opens X,
i : V ⟶ U,
Us : covering_family U,
Us_cover : U = ⨆ (u : over U) (H : u ∈ Us), u.left
⊢ V.val ≤ (⨆ (Ui : over U) (H : Ui ∈ Us), ((over.comap i).obj Ui).left).val

[Johan Commelin]

So I want to show that V ⊆ ⨆ Ui, (V ∩ Ui).

[Johan Commelin]

That is the math version of the goal.

[Kenny Lau]

where is V on the right hand side?

[Johan Commelin]

V : opens X

[Johan Commelin]

Aah, it is hidden in comap i

[Johan Commelin]

Which in this setting just means: V ∩ _

[Johan Commelin]

Now I would think that opens.gc should let me transform the right hand side from
(⨆ (Ui : over U) (H : Ui ∈ Us), ((over.comap i).obj Ui).left).val into
⨆ (Ui : over U) (H : Ui ∈ Us), (((over.comap i).obj Ui).left).val.
(I moved a parentheses to before over.comap.)

[Kenny Lau]

do you know what it is definitionally equivalent to?

[Kenny Lau]

if not can you just unfold everything?

[Johan Commelin]

If this goal could be transformed into V.val ∩ Ui.left.val ≤ (over.comap i) blah).val for all Ui, then I could take it from there.

[Kenny Lau]

if you intro x, then i x says that x \in U right

[Kenny Lau]

then you rewrite Us_cover

[Johan Commelin]

Ok

[Kenny Lau]

so now it says x \in set.bUnion _

[Johan Commelin]

Make that an x

[Kenny Lau]

then set.mem_bUnion_iff or something should give you something useful

[Johan Commelin]

Now I want to extract a Ui that contains x

[Johan Commelin]

Aah, let me try to find that one.

[Johan Commelin]

Except that it is a supr instead of a bUnion.

[Kenny Lau]

aren't they defeq?

[Johan Commelin]

There should be a lattice.mem_supr_iff.

[Johan Commelin]

Aah, probably yes. I'll try.

[Kenny Lau]

you can't be the member of just any supremum

[Johan Commelin]

Yay! First use of erw in my Lean-life. Context is now

X : Type u,
_inst_1 : topological_space X,
U V : opens X,
i : V ⟶ U,
Us : covering_family U,
Us_cover : U = ⨆ (u : over U) (H : u ∈ Us), u.left,
x : X,
hx : x ∈ V.val,
this :
  ∃ (x_1 : order_dual (opens X)),
    x_1 ∈ {a : opens X | ∃ (i : over U), a = (λ (u : over U), ⨆ (H : u ∈ Us), u.left) i} ∧ x ∈ x_1.val
⊢ x ∈ (⨆ (Ui : over U) (H : Ui ∈ Us), ((over.comap i).obj Ui).left).val

[Johan Commelin]

That looks encouraging, right? Especially that order_dual that is leaking through.

[Johan Commelin]

Ok, need to go. But now I think I can complete this. Thanks a lot!