# Zulip Chat Archive

## Stream: new members

### Topic: Conv in a calc

#### Scott Viteri (Oct 18 2019 at 00:18):

The last line in the following fails -- even though it is the same operation that is proved to create h''.

Is there an issue with using conv in calc, or am I misunderstanding how calc works?

theorem le_trans {x y z : α} (h : x ≤ y) (h' : y ≤ z) : x ≤ z := begin replace h : x = x ⊓ y, from (eq.subst (le_def x y) h), replace h' : y = y ⊓ z, from (eq.subst (le_def y z) h'), refine (eq.subst (le_def x z).symm _), have h'' : x ⊓ y = x ⊓ (y ⊓ y), from by conv { to_lhs, congr, skip, rw ←(inf_idem y) } calc x = x ⊓ y : by exact h, ... = x ⊓ (y ⊓ y) : by conv { to_lhs, congr, skip, rw ←(inf_idem y) }

#### Reid Barton (Oct 18 2019 at 00:34):

If `h''`

is introduced by `have`

then its definition is not "visible". Use `let`

instead

#### Scott Viteri (Oct 18 2019 at 00:37):

The issue was the comma at the end of the first calc line

#### Scott Viteri (Oct 18 2019 at 00:38):

h'' seems still too be visible -- lean doesn't complain at the following:

theorem le_trans {x y z : α} (h : x ≤ y) (h' : y ≤ z) : x ≤ z := begin replace h : x = x ⊓ y, from (eq.subst (le_def x y) h), replace h' : y = y ⊓ z, from (eq.subst (le_def y z) h'), refine (eq.subst (le_def x z).symm _), have h'' : x ⊓ y = x ⊓ (y ⊓ y), from by conv { to_lhs, congr, skip, rw ←(inf_idem y) }, calc x = x ⊓ y : by exact h ... = x ⊓ (y ⊓ y) : by exact h''

#### Reid Barton (Oct 18 2019 at 00:38):

Oh yes, that's also no good!

#### Reid Barton (Oct 18 2019 at 00:38):

Ah, I didn't read closely enough about `h''`

.

#### Scott Viteri (Oct 18 2019 at 00:39):

no problem, and thanks!

#### Kevin Buzzard (Oct 18 2019 at 07:51):

I remember really struggling with calc syntax as a beginner, and the error messages are unforgiving -- you just get a red line under the ... and something you don't understand in the error messages. The way I do it now is to lay everything out with `sorry`

proofs and to make sure I've got the syntax of the calc block exactly right before I start filling in the theorems.

#### Floris van Doorn (Oct 18 2019 at 15:04):

When writing `calc`

proofs, I strongly suggest first writing

calc foo = x : _ ... = y : _ ... = z : _

and only after that type-checks, filling in the underscores.

#### Kevin Buzzard (Oct 18 2019 at 17:45):

aah, even better than the sorry idea

Last updated: Dec 20 2023 at 11:08 UTC