Using `calc` to construct isomorphisms

Stream: general

[Yuma Mizuno]

calc is useful to construct isomorphisms like

variable (C : Type) [Category C] (a b c d : C)

example : a ≅ d :=
  calc
    a ≅ b := _
    _ ≅ c := _
    _ ≅ d := _

I wrote the following slightly different code by chance

example : a ≅ d :=
  calc
    a
    _ ≅ b := _
    _ ≅ c := _
    _ ≅ d := _

since a was a long expression. Actually, this is the third style in the language reference. However, I noticed that the produced expression is slightly different than the previous one, inserting auxiliary Trans.trans rfl _ in the expression.

In such a case, should we avoid the latter style?

[Yuma Mizuno]

One problem of this slight difference is that Trans.trans rfl _ is not simplified by simp. This may be solved by adding the following simp lemmas:

@[simp]
theorem trans_left_rfl (α β : Type*) (r : α → β → Sort*) (a : α) (b : β) (f : r a b) :
  Trans.trans rfl f = f := rfl

@[simp]
theorem trans_right_rfl (α β : Type*) (r : α → β → Sort*) (a : α) (b : β) (f : r a b) :
  Trans.trans f rfl = f := rfl

[Aaron Liu]

The way calc implements being able to have an optional first line like this is kind of weird. It also causes parsing errors when you have single line calc blocks, and it also allows you to write zero-line calc blocks.

[Yuma Mizuno]

I like this style (only a in the first line) when both a and b are around 80 characters long.

[Aaron Liu]

There are better ways to implement it

[Yuma Mizuno]

I wasn't really concerned with the implementation.

@Aaron Liu Would better ways you have in mind result in more restricted syntax? Or would the syntax stay the same but the generated expressions change?

[Aaron Liu]

The syntax would stay mostly the same, but the parsing would be modified a bit and the generated expressions would omit the Trans.trans rfl part

[Aaron Liu]

I haven't actually tried it yet though, so I don't know if it would work

[Aaron Liu]

the parser is so complicated

[Aaron Liu]

I finally figured out how to get this to parse

[Robin Carlier]

Note something else that I noticed when constructing isomorphisms with calc: #lean4 > Reassocating a calc proof : the terms constructed is left-associated when the one we’d write by hand is right-associated. This makes no difference as soon as you put a @[simps] but I feel it’s a bit of a bummer if you intend to stay at the "higher order" level and want to avoid over-reliance on ext for isos/nat isos..