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]

[Alex Brodbelt]

I was thinking about the same for MulEquiv and MonoidHom, since I am also working with chains of maps.
I found this open issue #6509 and I believe it is just a matter of adding Trans instances. For instance (pun not intended):

import Mathlib

variable (A B C : Type*) [MulOne A] [MulOne B] [MulOne C]

instance : Trans
  (@MonoidHom A B)
  (@MonoidHom B C)
  (@MonoidHom A C)
  where trans f g := g.comp f

instance : Trans
  (@MulEquiv A B)
  (@MulEquiv B C)
  (@MulEquiv A C)
  where trans f g := f.trans g

-- Having issues with this one
-- instance : Trans
--   (@MulEquiv A B)
--   (@MonoidHom B C)
--   (@MonoidHom A C)
--   where trans f g := g.comp f.toMonoidHom

--now works!
noncomputable example : ℤ →* ℝ :=
  calc
  ℤ →* ℚ := MonoidHom.smulOneHom
  ℚ →* ℝ := MonoidHom.smulOneHom
  ℝ →* ℝ := {
    toFun := fun x => abs x
    map_one' := by simp
    map_mul' := by simp
  }

--now works!
example : Multiplicative (ZMod 2) ≃* Multiplicative (ZMod 2) :=
  calc
  Multiplicative (ZMod 2) ≃* Multiplicative (ZMod 2) := sorry
  Multiplicative (ZMod 2) ≃* Multiplicative (ZMod 2) := sorry

[Alex Brodbelt]

I think I'll try open a PR for some of these if not all (I wonder if there is some further abstraction which can be done so this does not have to be done manually for each one) - I don't quite understand why you're not meant to provide the last two(?) implicit parameters, so maybe someone could enlighten me about this?

[Aaron Liu]

I feel like it's a bit hacky

[Aaron Liu]

calc is chaining the typeclasses instead of the types like it should be doing

[Alex Brodbelt]

whether it is hacky or not, I would find it useful :thinking: . I don't mind if it should be another tactic or not, though to me it would make sense to extend calc's capabilities