interactive transitivty proof

Stream: new members

[Callan McGill]

Is there a nice way to prove an inequality by transitivity in stages? I know you can do something like exact trans h1 h2 but I want to be able to do that interactively by generating goals or something like that?

[Adam Topaz]

Calc mode could work. You could also use refine in a tactic block, e.g refine trans h1 _, or in term mode put a hole as in trans h1 _ to see what the expected type of _ is, and fill it in progressively. It would be easier to help if you have an example in mind, and post a #mwe

[Reid Barton]

You can also use tactic#transitivity -- if your goal is A <= C and you use transitivity B then you will have new goals A <= B and B <= C

[Reid Barton]

Usually calc is nice for readability.

[Callan McGill]

cool thanks, I only just started lean so I didn't know about calc. My example was trying to prove the sum rule for sequences and having various points where I want to prove an inequality transitively

[Callan McGill]

If I am in a tactic environment how do I switch to calc, do I need to use have or something else?

[Reid Barton]

One potential issue with using transitivity B is that it might be tricky/annoying to write down B in the exact form you want, especially if there are coercions involved. If you already have a proof of one of the new goals then Adam's suggestion of using refine trans is convenient because then Lean will work out what B is for you.

[Reid Barton]

In tactic mode, calc BLAH is the same as exact calc BLAH.

[Callan McGill]

very helpful, thank you both!

[Anne Baanen]

Reid Barton said:

In tactic mode, calc BLAH is the same as exact calc BLAH.

Slight correction: a while ago (in commit lean#203) we made it expand to refine calc instead, so you can insert holes to be proved later on in the tactic script. Just wanted to make sure you knew of this bonus feature :)

[Kyle Miller]

Is this mentioned in any documentation? (The calc page makes it seem like you need to put exact before calc to use it in tactic mode.)

[Anne Baanen]

Doesn't look like there was any documentation, so I made some