Zulip Chat Archive
Stream: mathlib4
Topic: simpNF definition of "simplified"?
Arien Malec (Jan 13 2023 at 20:04):
I'm getting the message for mathlib4#1517
Encodable.encode_true /- Left-hand side simplifies from
Encodable.encode true
to
Encodable.encode (↑Equiv.boolEquivPUnitSumPUnit true)
using
simp only [@Encodable.encode_ofEquiv]
Try to change the left-hand side to the simplified term!
I assume I want to nolint this one (and the equivalent for false)
Johan Commelin (Jan 13 2023 at 20:13):
No, because the linter has a valid complaint.
Johan Commelin (Jan 13 2023 at 20:13):
In this case, please copy the lemma, and call it encode_true'. Mark that copy as @[simp] and remove @[simp] from the original.
In the copy, turn the LHS into what the linter suggests.
Johan Commelin (Jan 13 2023 at 20:14):
Ooh, wait. These are rfl-lemmas. So the dsimp test applies.
Johan Commelin (Jan 13 2023 at 20:16):
Johan Commelin (Jan 13 2023 at 20:17):
Huh? The docs seem broken.
Johan Commelin (Jan 13 2023 at 20:17):
Anyway, it looks like maybe that equiv should have simp lemmas.
Arien Malec (Jan 13 2023 at 20:19):
I guess my issue here is thinking that ↑Equiv.boolEquivPUnitSumPUnit true is simpler than true
Johan Commelin (Jan 13 2023 at 20:20):
Well, it can become simpler.
Johan Commelin (Jan 13 2023 at 20:20):
There should be a simp-lemma for that expression.
Johan Commelin (Jan 13 2023 at 20:21):
Where is that equiv defined?
Johan Commelin (Jan 13 2023 at 20:21):
mathlib or core?
Arien Malec (Jan 13 2023 at 20:24):
Mathlib.Logic.Equiv.Basic
But then again, if I try what simpNF suggests, I get:
invalid coercion notation, expected type is not known
Johan Commelin (Jan 13 2023 at 20:28):
Can you write attribute [simps] Equiv.boolEquivPUnitSumPUnit just above that encode_true lemma?
Arien Malec (Jan 13 2023 at 20:29):
Nope -- declaration is in an imported module.
Johan Commelin (Jan 13 2023 at 21:27):
Ooof, Lean4 is so strict about these things :grinning:
Eric Wieser (Jan 13 2023 at 22:09):
(mathlib4#1517 since the link above is broken)
Eric Wieser (Jan 13 2023 at 22:10):
Encodable.encode_ofEquiv (docs#encodable.encode_of_equiv) feels like a bad simp lemma to me
Eric Wieser (Jan 13 2023 at 22:11):
Unfolding instances is a pretty weird things to do
Arien Malec (Jan 13 2023 at 22:55):
Eric Wieser said:
(mathlib4#1517 since the link above is broken)
Oops, fixed.
Arien Malec (Jan 14 2023 at 00:20):
Removed, should put PR back to green.
Arien Malec (Jan 14 2023 at 00:22):
Sadly we won't spell true as inr (or the reverse?).
Eric Wieser (Jan 14 2023 at 09:10):
Eric Wieser said:
Unfolding instances is a pretty weird things to do
Thinking again, can this be resolved by putting a docs4#noindex around the instance argument after the @? Would that prevent unification and force syntactic matching?
Mario Carneiro (Jan 14 2023 at 09:31):
Eric Wieser said:
Eric Wieser said:
Unfolding instances is a pretty weird things to do
Thinking again, can this be resolved by putting a docs4#noindex around the instance argument after the @? Would that prevent unification and force syntactic matching?
It's the opposite - noindex will make it ignore the syntactic matching by replacing it with a metavariable, and then use unification to ensure that the instance applies. (That is, you can use noindex to make instances that match up to semireducible defeq, rather than simply reducible/instance defeq.)
Eric Wieser (Jan 14 2023 at 10:37):
Is there any way to make this lemma only match syntactically and not via unification? I realize this is sort of a special case and that unification is the right thing to do for typeclass arguments most of the time
Last updated: Dec 20 2023 at 11:08 UTC