Rewriting equalities in term mode

Stream: new members

[Philippe Duchon]

I am (not for the first time) going through MIL, and trying to write some of the proofs both in tactic mode and in term mode. Mostly, I'm writing a tactic mode proof first, and then converting it into term mode.

One point that I am having difficulty with is when my tactic mode proof uses calc (but here I more or less see why; calc uses a lot of transitivity and selective rewriting under the hood, and is much better at picking the right lemmas than I am), or does a little rewriting.

What is the "term mode equivalent" of rewriting?

[Kevin Buzzard]

\t

[Robin Arnez]

Yes, h \t x where h : a = b and x : .... a ... has type x : ... b ... and it also works the other way round (turning .... b ... into ... a ...). Regarding calc: calc also works in term mode and you can translate a calc proof basically entirely into a proof using trans (i.e. trans h (trans h' ...)).

[Philippe Duchon]

OK thanks (I admit that I thought Kevin's answer was the result of a premature "send")

I suppose trans is a somewhat high-level transitivity construct that knows how to deal with a variety of situations - something I tend to associate with tactic proofs, but I may have the wrong mental image here.

[Kevin Buzzard]

Oh I'm sorry! I was on mobile. The answer is ▸ which is typed with \t