GaloisConnection pred succ

Stream: mathlib4

[Kevin Buzzard]

A TODO in Order/SuccPred.Basic.lean here asks if pred and succ form a Galois connection. I saw this and got nerdsniped but I really need to get back to other things now so I thought I'd post my thoughts (which can I'm sure be golfed):

import Mathlib.Order.SuccPred.Basic
import Mathlib.Order.GaloisConnection

open Order

variable (α : Type) [Preorder α] [SuccOrder α] [PredOrder α]

lemma le_succ_pred (a : α) : a ≤ succ (pred a) := by
  by_cases h : IsMin a
  · exact le_trans (le_pred_iff_isMin.mpr h) (le_succ (pred a))
  · have := pred_covBy_of_not_isMin h
    by_cases h2 : pred a < succ (pred a)
    · apply this.2 at h2
      rw [lt_iff_le_not_le] at h2
      push_neg at h2
      apply h2
      apply succ_le_of_lt
      exact this.1
    · rw [lt_iff_le_not_le] at h2
      push_neg at h2
      rcases this with ⟨h3, h4⟩
      specialize h2 (le_succ _)
      rw [succ_le_iff_isMax] at h2
      exfalso
      rw [lt_iff_le_not_le] at h3
      apply h3.2
      apply h2
      exact h3.1

lemma pred_mono (a b : α) (h : a ≤ b) : pred a ≤ pred b := by
  exact pred_le_pred h

By symmetry I'm assuming that one can prove pred (succ a) <= a and succ_mono, and then use docs#GaloisConnection.monotone_intro to finish, if anyone would like to take this on. In particular I think it's true. Note that it's not symmetric: it's not true that succ (pred a) <= a because if the base type is Fin 37 then succ (pred 0) = 1 > 0.

[Kevin Buzzard]

@Yaël Dillies this is all your doing

[Yaël Dillies]

Wait what! I didn't think anyone (or you out of all of them) would figure this one out.

[Johan Commelin]

For the symmetry-claim, can't you use OrderDual?

[Yaël Dillies]

I think you can use yael-golf :grinning:

[Johan Commelin]

That tactic is very expensive. It comes with a 2~3 week delay because of some exams or such....

[Kevin Buzzard]

Well it's been a TODO since something like 2021 so I'm not sure there's a hurry :-)

[Ruben Van de Velde]

I think this morally obligates @Yaël Dillies to prove some FLT sorries :innocent:

[Yaël Dillies]

I mean, given that I might be in Imperial for several months next year, hmm, maybe?

[Yaël Dillies]

The tactic is bored of revision:

lemma le_succ_pred (a : α) : a ≤ succ (pred a) := by
  by_cases h : IsMin a
  · exact h.le_pred.trans (le_succ _)
  · exact (pred_covBy_of_not_isMin h).wcovBy.le_succ

[Yaël Dillies]

#13505

[Yaël Dillies]

Actually,

lemma le_succ_pred (a : α) : a ≤ succ (pred a) := (pred_wcovBy _).le_succ

[Floris van Doorn]

exact? could have almost figured out a conjecture in the doc.

[Yaël Dillies]

... yep

[Kevin Buzzard]

It's interesting! Yael wrote in 2021 that they weren't sure if it was true or not, and in fact I probably spent over an hour in total on the proof above because I also didn't know if it was true or not. The stuff I deleted before I posted here was two potential counterexamples to the Galois connection claim built as inductive types, the first one of which failed to work, and then I started working on the hypothesis that corollaries of the Galois connection claim might be easier to disprove, and came up with the second counterexample to a ≤ succ (pred a) which also failed to work out etc. This has been my "tube problem" for the last two days. I even tried to create some kind of structure theorem for PredSuccOrders and ended up with some kind of understanding of what they might look like, which ultimately led me to the proof. But once you know what you're actually trying to do (because the process converged on the journey in this morning), things get much easier. Once I had the proof I figured I'd broken the back of it and I'd let someone else analyse my work. It doesn't surprise me that there's a much shorter proof but I wasn't expecting a one-liner :-)

[Yaël Dillies]

Actually, you are missing a key step. When Violeta Hernández was working on polytopes, they needed the covering relation. We wrote !3#10676 together and I immediately got the hunch that covby.succ_eq (now docs#CovBy.succ_eq) was going to be key to proving the Galois connection. But I couldn't figure it out, so I wrote a mysterious "covers should help here." in the module doc instead.

[Kevin Buzzard]

That lemma only works for partial orders and I decided that I definitely wanted to stay in preorderland, but the preorder version is easy to guess

[Yaël Dillies]

As it turns out, my hunch was exactly right, as all we needed was CovBy.succ_eq, Order.covBy_succ and a few corollaries added over the years (Floris' WCovBy turns out to be really useful, but all it does here is saving us the case split. Without it, you get my second-to-last code snippet).

[Yaël Dillies]

I guess exact? could have helped had you stated your lemma for PartialOrder? docs#WCovBy.le_succ requires PartialOrder on master (I'm weakening it to Preorder in #13505).