## Stream: general

### Topic: Combining have and calc

#### Eric Wieser (Feb 07 2022 at 08:27):

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,


Is there another nice way to spell this?

#### Eric Wieser (Feb 07 2022 at 08:30):

Perhaps have calc?

#### Johan Commelin (Feb 07 2022 at 08:31):

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

#### Johan Commelin (Feb 07 2022 at 08:31):

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

#### Mario Carneiro (Feb 07 2022 at 08:31):

have := calc is pretty close to that already

#### Mario Carneiro (Feb 07 2022 at 08:32):

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

#### Eric Wieser (Feb 07 2022 at 08:36):

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

#### Ruben Van de Velde (Feb 07 2022 at 08:36):

Or have, calc

#### Eric Wieser (Feb 07 2022 at 08:36):

have, calc is also a syntax error

#### Mario Carneiro (Feb 07 2022 at 08:36):

@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 (Feb 07 2022 at 08:37):

you should just stay in tactic mode

#### Mario Carneiro (Feb 07 2022 at 08:38):

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

#### Mario Carneiro (Feb 07 2022 at 08:39):

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

#### Mario Carneiro (Feb 07 2022 at 08:40):

or let this := calc

#### Eric Rodriguez (Feb 07 2022 at 08:50):

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

#### Eric Rodriguez (Feb 07 2022 at 08:57):

Oh I see you explicitly don't want said order

Last updated: Dec 20 2023 at 11:08 UTC