Calc mode

Stream: lean4

[Philip Wadler]

Theorem Proving in Lean (version for Lean 4) states: "The calc command can be configured for any relation that supports some form of transitivity. It can even combine different relations." However, it doesn't explain how to do the configuration!

In Lean 3, one prepends the @[trans] attribute to a suitable lemma. But when I attempt the same in Lean 4, I get the error message "unknown attribute trans". How should I proceed?

(Specifically, I want to define a one step reduction relation, M ~> N, and use calc with several steps
calc
M ~> N := ...
_ ~> P := ....
_ ~> Q := ...
to establish M ~>* Q, where ~>* is the transitive and reflexive closure of ~>.)

[Leonardo de Moura]

It now uses type classes. Here are some examples for Nat.
https://github.com/leanprover/lean4/blob/master/src/Init/Data/Nat/Basic.lean#L226-L236
I will update "Theorem Proving in Lean 4" with examples.

[François G. Dorais]

You just need appropriate instances of the Trans class. In your case, instances of Trans (.~>.) (.~>*.) (.~>*.) and Trans (.~>*.) (.~>.) (.~>*.) would do the trick.

[Philip Wadler]

Thank you for the help! I've gotten that to work for relations, defined as Prop.

However, the reduction relation I have in mind is not a Prop but a Type, because I want to compute with it. In particular, I can use a proof of the progress theorem to compute a sequence of reduction steps. That works only if progress is a Type not a Prop, since computation on Prop is disabled. Is calc and Trans restricted to work only with Prop? If so, is there an analogue of each that works with Type?

If you want to see the code I've produced so far, it is here:
https://github.com/plfa/plfl/blob/main/src/DeBruijn.lean
I define simply-typed lambda calculus, prove progress, and use it to compute the derivation reducing 2+2 to 4. It echoes a development in Agda found here
https://plfa.inf.ed.ac.uk/DeBruijn/
which is part of my textbook, so has considerably more text to explain it!

[Leonardo de Moura]

I pushed the following commit that removes this restriction from calc.
https://github.com/leanprover/lean4/commit/ee6e2036ddef27ddea87d0abb8a83b92bd7c8857
The modification should be in our next nightly build.

[Philip Wadler]

Wow, that's a blindingly fast response! I look forward to trying it out.