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