calc and grw with OrderIso

Stream: new members

[Eric Paul]

I often have some chain of docs#OrderIso that I want to construct and apply. It would be more readable if I could use grw and calc to construct these. In particular, is it possible to make something like either of these examples work?

import Mathlib

example [LinearOrder A] [LinearOrder B] [LinearOrder C]
    (h1 : A ≃o B) (h2 : B ≃o C) : A ≃o C :=
  calc A
    _ ≃o B := h1
    _ ≃o C := h2

import Mathlib

example [LinearOrder A] [LinearOrder B] [LinearOrder C]
    (h2 : B ≃o C) : A ⊕ₗ B ≃o A ⊕ₗ C := by
  grw [h2]

My understanding is that for calc to work, I need an instance of docs#Trans. However, it seems that requires a relation where I can't enforce that the two types being related have an instance of LE and so I can't create such an instance for OrderIso.
Separately, my attempts at tagging things with @[gcongr] in hopes that grw would work were also unsuccessful.
Has anyone tried something along these lines?

[Eric Paul]

Here's an approach for the rewriting that I think works well enough for me. I'm surprised the orderIso_of_iso is not already in mathlib.

import Mathlib

variable [LinearOrder A] [LinearOrder B] [LinearOrder C]

open CategoryTheory
open LinOrd

def orderIso_of_iso (iso : of A ≅ of B) : A ≃o B where
  toFun := iso.hom
  invFun := iso.inv
  left_inv := by simp [Function.LeftInverse]
  right_inv := by simp [Function.RightInverse, Function.LeftInverse]
  map_rel_iff' := by
    intro a b
    constructor
    · intro h
      by_contra!
      change iso.hom a ≤ iso.hom b at h
      have : iso.hom b ≤ iso.hom a := OrderHomClass.GCongr.mono iso.hom.hom' this.le
      have : iso.hom a = iso.hom b := by order
      apply_fun iso.inv at this
      simp only [Iso.hom_inv_id_apply] at this
      order
    · exact fun a_1 ↦ OrderHomClass.GCongr.mono iso.hom.hom' a_1

example [LinearOrder A] [LinearOrder B] [LinearOrder C]
    (h1 : A ≃o B) (h2 : B ≃o C) : A ≃o C := by
  apply orderIso_of_iso
  calc of A
    _ ≅ of B := Iso.mk h1
    _ ≅ of C := Iso.mk h2

[Eric Paul]

In order to try to use this approach with for grw, I needed to create this new notation otherwise @[gcongr] would complain that the conclusion was not in the right form. After making that notation, I can get gcongr working, but not grw yet.

import Mathlib

variable [LinearOrder A] [LinearOrder B] [LinearOrder C]

open CategoryTheory
open LinOrd

def orderIso_of_iso (iso : of A ≅ of B) : A ≃o B := sorry

def sumLex (a b : LinOrd) : LinOrd := of (a ⊕ₗ b)
infix:90 " +ₗ " => sumLex

@[gcongr]
def sumLexCongr (α₁ : LinOrd) {β₁ β₂ : LinOrd}
    (eb : β₁ ≅ β₂) : α₁ +ₗ β₁ ≅ α₁ +ₗ β₂ := by
  apply LinOrd.Iso.mk
  exact OrderIso.sumLexCongr (OrderIso.refl α₁) (orderIso_of_iso eb)

@[simp]
def sumLex_iso_sum : of (A ⊕ₗ B) = (of A) +ₗ (of B) := by rfl

example [LinearOrder A] [LinearOrder B] [LinearOrder C]
    (h2 : B ≃o C) : A ⊕ₗ B ≃o A ⊕ₗ C := by
  apply orderIso_of_iso
  simp
  gcongr
  · exact LinOrd.Iso.mk h2

When I use grw [(LinOrd.Iso.mk h2 : of B ≅ of C)], I get the error which I don't understand

tactic 'apply' failed, could not unify the conclusion of the term
  ?r ?b ?c → ?r ?a ?c
with the goal
  (of A +ₗ of C ≅ of A +ₗ of C) → (of A +ₗ of B ≅ of A +ₗ of C)

[Eric Paul]

I got the grw to work! I was just missing the following gcongr lemma

attribute [gcongr] Iso.trans

[Eric Paul]

As an update in case someone else in the future thinks about this, I tried switching over to this approach but all the little calls needed to make swapping over to LinOrd work cluttered things enough that I felt like it was not a gain in readability. So I went ahead and made some tactics instead so that I can now write the following and that works well for me.

def iso (A) (B) [LinearOrder A] [LinearOrder B] : A ≃o B := sorry
example [LinearOrder A] [LinearOrder B] [LinearOrder C] [LinearOrder D] [LinearOrder E]
    (h : C ≃o D) : (A ⊕ₗ B) ⊕ₗ C ≃o E ⊕ₗ B ⊕ₗ D := by
  orderCalc (A ⊕ₗ B) ⊕ₗ C
  _ ≃o A ⊕ₗ B ⊕ₗ C := by orderCongr
  _ ≃o E ⊕ₗ B ⊕ₗ D := by orderCongr [iso A E]