chaining together heterogeneous equalities

Stream: new members

[Patrick Nicodemus]

How do you chain together heterogeneous equalities?

example het_eq (A B C D  :Type u) (a : A) (b : B) (c :C) (d :D)
  (p : a ≍ b)(q : b ≍ c) (r : c ≍ d) : a ≍ d := by
  calc
  a ≍ b := p
  _ ≍ c := q -- invalid 'calc' step, left-hand side is C : Type u but previous right-hand side is  b : B
  _ ≍ d := r

[Aaron Liu]

oh heq doesn't work with calc because of how the arguments are ordered

[Aaron Liu]

probably best to use docs#HEq.trans manually or automation would take care of this too

[Eric Wieser]

Should the argument order be changed so that this works?

[Aaron Liu]

it looks like it would give you one parameter and three indices instead of what we have now which is two parameters and two indices

[Patrick Nicodemus]

Okay. I used HEqtrans manually and that was fine.

[Kenny Lau]

@Patrick Nicodemus you can also use the trans tactic:

import Batteries.Tactic.Trans

universe u

example (A B C D : Type u) (a : A) (b : B) (c : C) (d : D)
    (p : a ≍ b) (q : b ≍ c) (r : c ≍ d) : a ≍ d := by
  trans b
  · exact p
  trans c
  · exact q
  · exact r