Zulip Chat Archive

Stream: maths

Topic: unnecessary suffering in galois insertion


view this post on Zulip Kevin Buzzard (Apr 05 2020 at 13:54):

/-- A Galois insertion is a Galois connection where `l ∘ u = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. -/
structure galois_insertion {α β : Type*} [preorder α] [preorder β] (l : α  β) (u : β  α) :=
(choice : Πx:α, u (l x)  x  β)
(gc : galois_connection l u)
(le_l_u : x, x  l (u x))
(choice_eq : a h, choice a h = l a)

Why not choice : Πx:α, u (l x) ≤ x → β := lam a h, l a and choice_eq : ∀a h, choice a h = l a := rfl like in

set_option auto_param.check_exists false
/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl :  a : α, a  a)
(le_trans :  a b c : α, a  b  b  c  a  c)
(lt := λ a b, a  b  ¬ b  a)
(lt_iff_le_not_le :  a b : α, a < b  (a  b  ¬ b  a) . order_laws_tac)

? Looking through mathlib this seems to be a common situation and it would save users from having to write these two extra lines. Is this worth a PR or are there subtleties I'm missing? Do I need a . refl_tac or something?

view this post on Zulip Mario Carneiro (Apr 05 2020 at 14:31):

order_laws_tac is just a simple tactic that does try {refl}

view this post on Zulip Mario Carneiro (Apr 05 2020 at 14:32):

unfortunately you can't pass a tactic expression there, only the name of a previously defined tactic, so that's why it's order_laws_tac

view this post on Zulip Mario Carneiro (Apr 05 2020 at 14:32):

You can't put := rfl because that doesn't typecheck

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 15:13):

Oh of course. But if I use order_laws_tac then is there anything particularly wrong with this? I'm just teaching someone about closures and told them to make a Galois insertion and it was just more complicated than I'd expected.


Last updated: May 11 2021 at 16:22 UTC