Zulip Chat Archive
Stream: general
Topic: rewriting class operations
Reid Barton (Jun 05 2018 at 14:18):
I have this instance:
instance Xplus.setoid : setoid Xplus := ⟨Xplus_rel, Xplus_rel.refl, Xplus_rel.symm, Xplus_rel.trans⟩
How can I use a tactic to rewrite a ≈ b somewhere in the goal to Xplus_rel a b?
Reid Barton (Jun 05 2018 at 14:21):
Is there some name I can pass to rw or simp?
Kenny Lau (Jun 05 2018 at 14:21):
set_option pp.notations false
Simon Hudon (Jun 05 2018 at 14:22):
Does change Xplus_rel a b do it for you?
Sebastian Ullrich (Jun 05 2018 at 14:23):
simp [(≈)] should do it
Reid Barton (Jun 05 2018 at 14:23):
change works if I write out the whole new goal (which isn't bad at all using copious _s)
Reid Barton (Jun 05 2018 at 14:24):
simp [(≈)] turned it into setoid.r, not Xplus_rel
Reid Barton (Jun 05 2018 at 14:24):
Oh, but [(≈), setoid.r] worked
Kenny Lau (Jun 05 2018 at 14:24):
≈ is literally setoid.r
Reid Barton (Jun 05 2018 at 14:25):
No, it's literally has_equiv.equiv
Kenny Lau (Jun 05 2018 at 14:25):
oh
Reid Barton (Jun 05 2018 at 14:26):
Great, this is better than what I had before. I feel like I run into this a lot
Chris Hughes (Jun 05 2018 at 14:54):
I often use show Xplus_rel a b in these situtations.
Simon Hudon (Jun 05 2018 at 15:01):
That's similar to change but @Reid Barton pointed out that that only works if there's nothing else in your goal.
Chris Hughes (Jun 05 2018 at 15:20):
show Xplus_rel _ _
Simon Hudon (Jun 05 2018 at 15:23):
That doesn't work if the goal is p ∧ Xplus_rel a b
Kenny Lau (Jun 05 2018 at 15:23):
split
Simon Hudon (Jun 05 2018 at 15:26):
This is an ad hoc response to it. @Reid Barton Is looking for one solution that will work for a variety of goals
Reid Barton (Jun 05 2018 at 15:27):
And won't get longer the longer my goal is
Last updated: Dec 20 2023 at 11:08 UTC