## Stream: maths

### Topic: unnecessary suffering in galois insertion

#### 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?

#### Mario Carneiro (Apr 05 2020 at 14:31):

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

#### 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

#### Mario Carneiro (Apr 05 2020 at 14:32):

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

#### 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