Zulip Chat Archive

Stream: general

Topic: simp vs rw


view this post on Zulip Yury G. Kudryashov (Jan 22 2020 at 23:07):

Hi, is there a command that can do rewrites inside forall / exists (like simp) but does them in a predictable order (like rw)?

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 23:08):

You mean without using conv?

view this post on Zulip Yury G. Kudryashov (Jan 22 2020 at 23:09):

Yes.

view this post on Zulip Yury G. Kudryashov (Jan 22 2020 at 23:10):

I just want to simplify f '' s ⊆ t to ∀ x ∈ s, f x ∈ t inside . rw can't do it, and simp only [image_subset_iff, subset_def] applies the latter lemma first.

view this post on Zulip Yury G. Kudryashov (Jan 22 2020 at 23:11):

Currently I write simp only [image_subset_iff], simp only [subset_def, mem_preimage]

view this post on Zulip Mario Carneiro (Jan 22 2020 at 23:11):

oof, kevin beat me with the conv

view this post on Zulip Mario Carneiro (Jan 22 2020 at 23:12):

use conv rw

view this post on Zulip Yury G. Kudryashov (Jan 22 2020 at 23:13):

Do you mean conv { (navigate), rw }?

view this post on Zulip Yury G. Kudryashov (Jan 22 2020 at 23:15):

I wanted to avoid explicit navigation.

view this post on Zulip Yury G. Kudryashov (Jan 22 2020 at 23:15):

It's inside 4 levels of forall, so I'll just stick to simp only [], simp only [].

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 23:17):

It's set.ball_image_iff if that helps...

view this post on Zulip Mario Carneiro (Jan 22 2020 at 23:17):

I guess it would not be hard to write a wrapper that looks like rw [a, b] and does simp only [a], simp only [b]

view this post on Zulip Anne Baanen (Jan 23 2020 at 09:35):

I've also been wanting a rewrite-under-binders tactic (I've been doing a lot of rewrites of the form finset.prod s (λi, ...)), so I'd be happy to program it :-)

view this post on Zulip Anne Baanen (Jan 23 2020 at 14:56):

Success:

example {α β : Type} {f : α  β} {t : set β} : ( s, f '' s  t) =  s : set α,  x  s, x  f ⁻¹' t :=
by simp_rw [set.image_subset_iff, set.subset_def]

view this post on Zulip Anne Baanen (Jan 23 2020 at 14:57):

At this point, the tactic is just:

/-- `simp_rw` is a version of `simp` where rules are applied in the given order like `rw` does .-/
meta def simp_rw (q : parse rw_rules) (l : parse location) : tactic unit :=
  q.rules.mmap' (λ (rule : rw_rule),
    if rule.symm
    then fail "simp_rw can only rewrite in forward direction"
    else simp none tt [simp_arg_type.expr rule.rule] [] l) -- equivalent to `simp only [rule] at l`

view this post on Zulip Anne Baanen (Jan 23 2020 at 15:47):

I discussed a bit with @Gabriel Ebner and we came to the conclusion that rewriting in the reverse direction is probably best done by extending the C++ code for simp.

view this post on Zulip Anne Baanen (Jan 23 2020 at 15:48):

So the first edition of simp_rw won't have support for simp_rw [←foo] unfortunately

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 15:59):

There's always foo.symm

view this post on Zulip Anne Baanen (Jan 23 2020 at 16:01):

Indeed! But foo.symm doesn't help if foo : ∀x, bar x = baz x :(

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 16:02):

then it's (foo _).symm :-/

view this post on Zulip Anne Baanen (Jan 23 2020 at 16:03):

The hope was that the tactic could just add these underscores and then apply the appropriate symm, but the types don't get inferred nicely when you do that

view this post on Zulip Anne Baanen (Jan 23 2020 at 17:09):

Here's the pull request: https://github.com/leanprover-community/mathlib/pull/1900

view this post on Zulip Mario Carneiro (Jan 23 2020 at 19:29):

You can build the symmetry transform manually (using app and lambda)


Last updated: May 13 2021 at 22:15 UTC