Zulip Chat Archive

Stream: general

Topic: congr' vs congr


view this post on Zulip Eric Wieser (Jan 08 2021 at 15:14):

I have a goal state where congr' 3 closes the goal, but congr gives me an awful a == b goal where a and b are smul_comm_class objects. Does this mean that there's more to congr' than just " stop after n steps"?

view this post on Zulip Eric Wieser (Jan 08 2021 at 15:15):

The line in question is https://github.com/leanprover-community/mathlib/pull/5269/files#diff-48c4d86a6f8902ed17b9728588594da05839379ca05b4dcabc31a3999850cf65R749

view this post on Zulip Anne Baanen (Jan 08 2021 at 15:38):

congr doesn't always check at each subexpression if the sides of the equality are already defeq:

def const :      := λ x _, x
example {m n : } : const 0 m = const 0 n :=
by congr -- Unsolved goals: ⊢ m = n
example {m n : } : id (const 0 m) = id (const 0 n) :=
by congr -- Succeeds

view this post on Zulip Anne Baanen (Jan 08 2021 at 15:39):

Not sure that that is the same thing as your issue, just something interesting I found when investigating it.

view this post on Zulip Eric Wieser (Jan 08 2021 at 15:45):

I don't understand what's going on in your example at all, but it's quite likely the same as my problem


Last updated: May 10 2021 at 18:22 UTC