dummy/lexicographical LinearOrder

Stream: mathlib4

[Robert Maxton]

What's the easiest way to register a second order on a (finite, enumerable) inductive type? The new order has no special mathematical content, and could reasonably be expressed by "derive Fintype and use the order from enumList"; it exists purely so that I can more easily talk about symmetries of maps into the type (so e.g. if I have a map f : Bool → MyType, I can express that the proof treats f and f ∘ (¬ ·) the same as wlog hf : toLex (f true) ≥ toLex (f false).)

What I have is this, but it's pretty verbose:

inductive O3C2 : Type u where | left | zero | mid | one | right
  deriving Fintype, DecidableEq, Inhabited, Repr

namespace O3C2

@[simps]
instance : Preorder O3C2 := sorry

namespace Lex

def idx
  | O3C2.left => 0
  | O3C2.zero => 1
  | O3C2.mid => 2
  | O3C2.one => 3
  | O3C2.right => 4

@[simp]
lemma idx_inj {x y : O3C2} : (Lex.idx x = Lex.idx y) ↔ x = y := by
  casesm* O3C2 <;> simp [Lex.idx]

-- We want to unfold `idx` automatically in proofs, but only when we have a concrete element of
-- `O3C2` to work with; there's no obvious way to do this other than a `simp` lemma for each case.
@[simp] lemma idx_left : idx O3C2.left = 0 := rfl
@[simp] lemma idx_zero : idx O3C2.zero = 1 := rfl
@[simp] lemma idx_mid : idx O3C2.mid = 2 := rfl
@[simp] lemma idx_one : idx O3C2.one = 3 := rfl
@[simp] lemma idx_right : idx O3C2.right = 4 := rfl

-- Similarly, we want to recognize when a value of `O3C2` has been pinned down by its index, so
@[simp] lemma idx_eq_0_iff {x : O3C2} : idx x = 0 ↔ x = O3C2.left := by rw [← idx_left, idx_inj]
@[simp] lemma idx_eq_1_iff {x : O3C2} : idx x = 1 ↔ x = O3C2.zero := by rw [← idx_zero, idx_inj]
@[simp] lemma idx_eq_2_iff {x : O3C2} : idx x = 2 ↔ x = O3C2.mid := by rw [← idx_mid, idx_inj]
@[simp] lemma idx_eq_3_iff {x : O3C2} : idx x = 3 ↔ x = O3C2.one := by rw [← idx_one, idx_inj]
@[simp] lemma idx_eq_4_iff {x : O3C2} : idx x = 4 ↔ x = O3C2.right := by rw [← idx_right, idx_inj]

@[simp]
lemma idx_toLex {x} : idx (toLex x) = idx x := by rfl

/-- A second, linear order on `O3C2`. Mostly used to better exploit symmetries. -/
@[simps]
instance : LinearOrder (Lex O3C2) where
  le := (Lex.idx · ≤ Lex.idx ·)
  le_refl x := by rfl
  le_trans x y z hxy hyz := by grw [hxy, hyz]
  le_antisymm x y hxy hyx := by simpa using Nat.le_antisymm hxy hyx
  le_total x y := by casesm* Lex O3C2 <;> simp [Lex.idx]
  toDecidableLE := inferInstance

@[simp↓ high]
lemma toLex_le {x y : O3C2} : toLex x ≤ toLex y ↔ Lex.idx x ≤ Lex.idx y := by rfl

end Lex

[Aaron Liu]

you just want an arbitrary order?

[Aaron Liu]

does it have to be computable?

[Robert Maxton]

It needs to be explicit, in that I need to be able to say (ideally, quickly and easily) whether or not toLex left ≤ toLex right

[Aaron Liu]

Robert Maxton said:

It needs to be explicit, in that I need to be able to say (ideally, quickly and easily) whether or not toLex left ≤ toLex right

at compile time or at runtime

[Robert Maxton]

I'm basically only going to be using it in proofs, so compile time I think

[Aaron Liu]

you can try see if the O3C2.toCtorIdx exists

[Robert Maxton]

Like I said, it's so I can say "If I proof this for arrangement A, then I've also proved it for flipped A" in a convenient way, by saying "I shall only bother proving this for the arrangement where A happens to be monotone"

[Aaron Liu]

or you can write one yourself

[Robert Maxton]

well, I'm pretty sure I did in fact write it myself lel
the problem is mostly that using it conveniently requires a bunch of boilderplate lemmas >.>;

[Aaron Liu]

try putting @[simp] on idx?

[Aaron Liu]

not sure if that will do what I want it to do though

[Robert Maxton]

huh
O3C2.toCtorIdx and O3C2.enumList_getElem?_to_CtorIdx_eq both exist

[Robert Maxton]

let's see

[Robert Maxton]

.... lol, toCtorIdx is in fact just rec 0 ... n
amazing

[Robert Maxton]

well, at any rate, that certainly reduced the boilerplate

[Robert Maxton]

thanks!