Conv in a calc

Stream: new members

[Scott Viteri]

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]

If h'' is introduced by have then its definition is not "visible". Use let instead

[Scott Viteri]

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

[Scott Viteri]

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]

Oh yes, that's also no good!

[Reid Barton]

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

[Scott Viteri]

no problem, and thanks!

[Kevin Buzzard]

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]

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]

aah, even better than the sorry idea