## 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