Zulip Chat Archive

Stream: general

Topic: partial_order (with_bot X) is so unrflly


Kevin Buzzard (Mar 24 2019 at 11:00):

From order.bounded_lattice:

instance partial_order [partial_order α] : partial_order (with_bot α) :=
{ le          := λ o₁ o₂ : option α,  a  o₁,  b  o₂, a  b,
...

This definition of le on with_bot alpha means that stuff like a <= b iff some a <= some b is not proved by iff.rfl. If this proof had been done with pattern matching would this not have made life easier? Oh -- can one not pattern match in a structure field? Lean is complaining that my set_of is broken -- it thinks { ... | ... is a set.

Mario Carneiro (Mar 24 2019 at 11:02):

it is defined that way so that you don't have to deal with pattern matching on option all the time

Kevin Buzzard (Mar 24 2019 at 11:04):

import algebra.group order.bounded_lattice

variable {α : Type*}

instance meh [partial_order α] : partial_order (with_bot α) :=
{ le := λ o₁ o₂, match (o₁, o₂) with
         | (none, _) := true
         | (some x, none) := false
         | (some x, some y) := x  y
         end,
--:= λ o₁ o₂ : option α, ∀ a ∈ o₁, ∃ b ∈ o₂, a ≤ b,
  le_refl := sorry,
  le_trans := sorry,
  le_antisymm := sorry
}

example [partial_order α] (x y : α) : (x : with_bot α)  y  x  y := iff.rfl

Kevin Buzzard (Mar 24 2019 at 11:05):

But instead I'm having to deal with other things.

Kevin Buzzard (Mar 24 2019 at 11:06):

like having to use change then rw a lot


Last updated: Dec 20 2023 at 11:08 UTC