# Zulip Chat Archive

## 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,
by rwa ←add_right_eq_self
```

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