Zulip Chat Archive

Stream: new members

Topic: What's the lean4 equivalent of 'cc'?

jim (Dec 03 2022 at 17:32):

Hi all! I'm learning Lean this evening, by working through the Natural Numbers Game. However, I'm using Lean 4, and the game just seems to be for Lean 3. So I'm converting each challenge to Lean 4 as I go. I've hit my first stumbling block: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=6&level=9 This chapter recommends solving with the tactic cc, but I can't see this tactic in Lean 4, or any equivalent of it. Could someone suggest how I would concisely solve this one in Lean 4?

jim (Dec 03 2022 at 17:46):

I found https://leanprover.github.io/lean4/doc/lean3changes.html - which looks useful, but it only seems to cover "language-level" breaking changes, rather than breaking changes in libraries, tactics, macros etc

jim (Dec 03 2022 at 17:57):

I also found congr, but it seems to be something different, and only usable within a conv mode (not really sure what I'm talking about here)

Reid Barton (Dec 03 2022 at 18:04):

I think the Lean 4 equivalent of cc is called cc--it just hasn't been written yet.

Reid Barton (Dec 03 2022 at 18:04):

I also didn't realize that this "maze" was within the scope of cc.

jim (Dec 03 2022 at 18:10):

A very logician-style answer :)

jim (Dec 03 2022 at 18:10):

Thanks, no worries - I don't think I need it

Kyle Miller (Dec 03 2022 at 18:17):

solve_by_elim might work for the maze (docs4#Mathlib.Tactic.SolveByElim.solveByElim)

jim (Dec 03 2022 at 18:28):

Thanks @Kyle Miller - I'm just using prelude etc at the moment and haven't figured out how to install packages like mathlib - I'll give it a go

Patrick Massot (Dec 04 2022 at 08:26):

@jim have you seen https://lovettsoftware.com/NaturalNumbers/TutorialWorld.lean.html?

Last updated: Dec 20 2023 at 11:08 UTC