calc mode for types

Stream: mathlib4

[loooong]

We know calc mode is applicable for relations. Is it still applicable for other types (functions, equivalence, etc.)? For example, if I want to define a function: from A to D, I have three function A to B, B to C and C to D, I want to write as following

example (A B C D : Type )(f : A → B)(g : B → C)(h : C → D) : A → D := by
  calc
    A → B := f
    _ → C := g
    _ → D := h

i.e., I want to use calc mode for compositions. For another example, I want to use calc mode for trans of equivalence. Is there any way I can do that?

[Eric Wieser]

This works:

-- hack: Lean doesn't allow `→` in calc
abbrev imp (A B : Type _) := A → B
infix:50 "→'" => imp

instance : Trans imp imp imp where trans f g := Function.comp g f

example (A B C D : Type _) (f : A → B) (g : B → C) (h : C → D) : A → D := by
  calc
    A →' B := f
    _ →' C := g
    _ →' D := h

[Eric Wieser]

For equivalence it works out of the box:

import Mathlib.Logic.Equiv.Basic

example (A B C D : Type _) (f : A ≃ B) (g : B ≃ C) (h : C ≃ D) : A ≃ D := by
  calc
    A ≃ B := f
    _ ≃ C := g
    _ ≃ D := h

[loooong]

Thank you! I will try it!

[Jireh Loreaux]

@Eric Wieser why isn't → allowed in calc? Is there a specific reason (e.g., because it's foundational notation), or is it just "we didn't bother to support this character"?

[Eric Wieser]

Calc looks for expressions of the form some_rel _ _ _ A B, which A → B isn't without an auxiliary function.

[Eric Wieser]

In Lean 3 there was special hard-coded support for →, I guess Lean 4 didn't bother to add that (or decided deliberately not to)

[Matthew Ballard]

Can I suggest a change?

import Mathlib.Logic.Equiv.Basic

example (A B C D : Type*) (f : A ≃ B) (g : B ≃ C) (h : C ≃ D) : A ≃ D := by
  calc
    A ≃ B := f
    _ ≃ C := g
    _ ≃ D := h

[Eric Wieser]

Annoyingly adding _s doesn't work for MulEquiv:

import Mathlib.Algebra.Hom.Equiv.Basic

-- TODO: PR this!
instance : Trans (@MulEquiv A B) (@MulEquiv B C) (@MulEquiv A C) where trans := MulEquiv.trans

example (A B C D : Type*) [Monoid A] [Monoid B] [Monoid C] [Monoid D] (f : A ≃* B) (g : B ≃* C) (h : C ≃* D) : A ≃* D := by
  -- fails if you put `_`s at the start of each line
  calc
    A ≃* B := f
    B ≃* C := g
    C ≃* D := h

[loooong]

I want to use calc mode for LinearEquiv, but it seems to that I cannot use it directly. There are so many implicit variables for LinearEquiv.trans. Can someone give me some advice.

[Eric Wieser]

import Mathlib.Algebra.Module.Equiv

variables (R A B C D : Type _) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
   [Module R A] [Module R B] [Module R C] [Module R D]

-- TODO: PR a more general version of this!
instance : Trans
  (@LinearEquiv R R _ _ (RingHom.id _) (RingHom.id _) _ _ A B _ _)
  (@LinearEquiv R R _ _ (RingHom.id _) (RingHom.id _) _ _ B C _ _)
  (@LinearEquiv R R _ _ (RingHom.id _) (RingHom.id _) _ _ A C _ _) where trans := LinearEquiv.trans

example (R A B C D : Type _) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
   [Module R A] [Module R B] [Module R C] [Module R D] (f : A ≃ₗ[R] B) (g : B ≃ₗ[R] C) (h : C ≃ₗ[R] D) : A ≃ₗ[R] D := by
  calc
    A ≃ₗ[R] B := f
    B ≃ₗ[R] C := g
    C ≃ₗ[R] D := h

[loooong]

Thank you! this version is suitable for me!

[Eric Wieser]

I opened #6509 to track the TODO