order_iso woes

Stream: new members

[Bryan Gin-ge Chen]

I'm trying to generalize this function (there's a typo, that should be a def not a lemma; nonetheless it works...). I want to prove that an order_isogives rise to a galois_insertion but I'm stuck on what seems to me to be simple:

import order.galois_connection order.order_iso

namespace order_iso
variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
{r : β → β → Prop} {s : γ → γ → Prop} (oi : order_iso r s)

set_option pp.implicit true

theorem to_galois_connection :
  galois_connection (oi.to_fun) (oi.inv_fun) :=
by unfold galois_connection;
exact λ {b g}, calc (oi.to_fun b) ≤ g ↔
  (oi.to_fun b) ≤ (oi.to_fun (oi.inv_fun g)) : by rw oi.right_inv
... ↔ b ≤ (oi.inv_fun g) : by { -- rw oi.ord
  have : r b (oi.inv_fun g) ↔
    s (oi.to_fun b) (oi.to_fun (oi.inv_fun g)) := (@order_iso.ord β γ r s oi b (oi.inv_fun g)),
  change oi.to_fun b ≤ oi.to_fun (oi.inv_fun g) ↔ b ≤ oi.inv_fun g,
  sorry }

protected def to_galois_insertion [preorder β] [preorder γ] : @galois_insertion β γ _ _
  (oi.to_fun) (oi.inv_fun) :=
{ choice := λ b h, oi.to_fun b,
  gc := to_galois_connection oi,
  le_l_u := λ g, le_of_eq (oi.right_inv g).symm,
  choice_eq := λ b h, rfl }

end order_iso

In the tactic state near where I gave up, the only difference I see between the goal and this is that the goal uses ≤ and this uses r and s.

[Kevin Buzzard]

This is a job for @Kenny Lau

[Mario Carneiro]

You should be able to use function coercion instead of to_fun and inv_fun everywhere

[Kenny Lau]

This is ridiculous.

[Kenny Lau]

variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
{r : β → β → Prop} {s : γ → γ → Prop} (oi : order_iso r s)

[Kenny Lau]

game: spot the error

[Mario Carneiro]

no error?

[Kenny Lau]

even Mario missed it

[Kenny Lau]

the correct declaration should be

variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
(oi : @order_iso β γ (≤) (≤))

[Johan Commelin]

In particular, this means that order_iso is not what we want it to be.

[Kenny Lau]

import order.galois_connection order.order_iso

namespace order_iso
variables {β : Type*} {γ : Type*} [preorder β] [preorder γ]
(oi : @order_iso β γ (≤) (≤))

theorem to_galois_connection : galois_connection oi oi.symm :=
λ b g, by rw [ord' oi, apply_inverse_apply]

protected def to_galois_insertion :
  @galois_insertion β γ _ _ oi oi.symm :=
{ choice := λ b h, oi b,
  gc := to_galois_connection oi,
  le_l_u := λ g, le_of_eq (oi.right_inv g).symm,
  choice_eq := λ b h, rfl }

end order_iso

[Kenny Lau]

@Mario Carneiro how many of this error do you think are in mathlib?

[Mario Carneiro]

Oh, I missed the context

[Mario Carneiro]

I thought you meant those variables don't typecheck

[Mario Carneiro]

are you saying that this is in mathlib?

[Mario Carneiro]

I guess there is a tension here between order_iso, which works with explicit relations, and galois_connection, which works with types with a preorder instance

[Kenny Lau]

I'm saying that there are errors like this in mathlib

[Mario Carneiro]

I'm sure there are, but someone has to notice them first

[Mario Carneiro]

if no one notices them then they aren't doing anyone harm

[Johan Commelin]

if no one notices them then they aren't doing anyone harm

Except that you might think you have formalised something, but it turns out to be something else.

[Mario Carneiro]

that's where the fun is

[Johan Commelin]

Isn't this exactly related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/stacks.20project.20.2F.20schemes/near/123090992

[Kevin Buzzard]

@Kenny Lau , now all the people who bothered to click and investigate are in on the joke, can you paste one line of explanation for those of us that are so busy preparing 1st year lectures that we don't even understand the issue at hand here and would hence prefer it if your comments were less cryptic?

[Kenny Lau]

@Kevin Buzzard basically there are two orders on each type when there should only be one order

[Bryan Gin-ge Chen]

Thanks Kenny! I'm glad it turned out to be something simple.