Zulip Chat Archive
Stream: general
Topic: Rewriting with variables
Bernd Losert (Dec 24 2021 at 14:51):
Say I have a goal like p.fst * p.snd = 10 and I have variables x := p.fst and y := p.snd. How do I rewrite the goal so that it reads x * y = 10.
Eric Rodriguez (Dec 24 2021 at 14:55):
are those created from let? You can just use change x * y = 10 if so, but if you want to rewrite (which I'd recommend) then the set tactic may be better.
Eric Wieser (Dec 24 2021 at 14:56):
dsimp only [x, y] might work
Bernd Losert (Dec 24 2021 at 14:56):
Yes, they are let variables.
Bernd Losert (Dec 24 2021 at 14:57):
dsimp didn't work.
Bernd Losert (Dec 24 2021 at 14:58):
change works. Great.
Eric Rodriguez (Dec 24 2021 at 14:58):
they want to go the other way, Eric :)
Bernd Losert (Dec 24 2021 at 15:02):
Hmm... can't I do a let ⟨x, y⟩ := p instead of doing two lets?
Eric Rodriguez (Dec 24 2021 at 15:03):
try obtain \<x, y> := p; but i'd not recommend this unless you never want to see p again
Bernd Losert (Dec 24 2021 at 15:03):
Using normal parenthesis doesn't work either.
Bernd Losert (Dec 24 2021 at 15:04):
obtain works. Is that a tactic?
Eric Rodriguez (Dec 24 2021 at 15:04):
yeah, it's a different syntax for rcases
Bernd Losert (Dec 24 2021 at 15:05):
Haha. It shows (x, y).fst and (x, y).snd
Eric Rodriguez (Dec 24 2021 at 15:06):
welcome to lean :p dsimp will then clear that (or maybe simp only) but that's type theory for you
Bernd Losert (Dec 24 2021 at 15:08):
Ah, nice. Thanks a lot.
Bernd Losert (Dec 24 2021 at 15:08):
Working with relations on products is going to get annoying.
Bernd Losert (Dec 24 2021 at 15:09):
Is there a version of assume that can destruct using ⟨x, y⟩?
Anne Baanen (Dec 24 2021 at 15:10):
Yakov Pechersky (Dec 24 2021 at 15:16):
Bernd, when you are in tactic mode, on every new step (that is, what comes right after a comma, for example), the first word you write always refers to a tactic. Like exact, refine, intro, cases, change, convert, congr, induction, norm_num... Some of those tactics take identifiers, some take expressions, some have a very precise syntax that take locations (at h, at *, at |-). Hopefully that helps your differentiate tactic tokens from term tokens
Bernd Losert (Dec 24 2021 at 15:17):
Anne Baanen said:
Fantastic.
Bernd Losert (Dec 24 2021 at 15:18):
Yakov Pechersky said:
Bernd, when you are in tactic mode, on every new step (that is, what comes right after a comma, for example), the first word you write always refers to a tactic. Like exact, refine, intro, cases, change, convert, congr, induction, norm_num... Some of those tactics take identifiers, some take expressions, some have a very precise syntax that take locations (at h, at *, at |-). Hopefully that helps your differentiate tactic tokens from term tokens
So let is also a tactic? Interesting.
Eric Rodriguez (Dec 24 2021 at 15:20):
The thing that may be confusing you is that let is also a thing in term mode:
example : 1 = 1 :=
let a := rfl in a
but it's just a coincidence. assume is also synonymous with \lam, and there was one more that just flew out of my head, but other than that there is no real overlap (afair)
Bernd Losert (Dec 24 2021 at 15:23):
Yes, that does confuse me. I also have a hard time making sense of tactic definitions.
Yakov Pechersky (Dec 24 2021 at 16:24):
dec_trivial is another token that is the same in both term mode and tactic mode
Mario Carneiro (Dec 24 2021 at 22:08):
Some tokens that act approximately the same in term and tactic mode: assume, have, let, suffices, show, calc, by, from
Last updated: Dec 20 2023 at 11:08 UTC