Combining have and `calc`

Stream: general

[Eric Wieser]

I thought I'd try writing up the example sheets I'm supervising in (nonidiomatic) lean:

import data.real.basic
import data.set.lattice
import order.boolean_algebra

namespace cued

-- yes, constants / axioms are bad but I want to reduce boilerplate for pedagogy
constant Ω : Type*
constant ℙ : set Ω → ℝ
axiom pos : ∀ s : set Ω, 0 ≤ ℙ s
axiom certain : ℙ (set.univ) = 1
axiom disj {A B} : disjoint A B → ℙ (A ∪ B) = ℙ A + ℙ B

lemma impossible : ℙ ∅ = 0 :=
suffices ℙ set.univ + ℙ ∅ = ℙ set.univ, by rwa ←add_right_eq_self,
calc ℙ set.univ + ℙ ∅ = ℙ (set.univ ∪ ∅) : by rw disj (set.disjoint_empty _)
                  ... = ℙ set.univ        : by rw set.union_empty

The proofI have on paper does this in the other order, by first doing the calc and then applying add_right_eq_self. I can get this order with have _, from, but that feels a bit ugly:

lemma impossible : ℙ ∅ = 0 :=
have _, from  -- this is just noise!
calc ℙ set.univ + ℙ ∅ = ℙ (set.univ ∪ ∅) : by rw disj (set.disjoint_empty _)
                  ... = ℙ set.univ        : by rw set.union_empty,
by rwa ←add_right_eq_self

Is there another nice way to spell this?

[Eric Wieser]

Perhaps have calc?

[Johan Commelin]

I've wished for a slightly less noisy version of that as well. Ideally have foo, calc .... would work.

[Johan Commelin]

Ooh, I like have calc, if it can be made to work

[Mario Carneiro]

have := calc is pretty close to that already

[Mario Carneiro]

there is no need to give the type ascription in a calc block since it comes with its own type ascription

[Eric Wieser]

have := calc doesn't seem legal in term mode

[Ruben Van de Velde]

Or have, calc

[Eric Wieser]

have, calc is also a syntax error

[Mario Carneiro]

@Eric Wieser It's not, but I'm not sure how worthwhile it is to extend lean 3 term syntax at this point

[Mario Carneiro]

you should just stay in tactic mode

[Mario Carneiro]

you can do so even while sticking to a very restricted tactic grammar if you are worried about overwhelming readers

[Mario Carneiro]

have _, by calc is probably the tersest equivalent in term mode

[Mario Carneiro]

or let this := calc

[Eric Rodriguez]

Can't you do add_right_eq_self.mpr $ calc... ?

[Eric Rodriguez]

Oh I see you explicitly don't want said order