# Zulip Chat Archive

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