## Stream: general

### Topic: simp vs rw

#### 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)?

#### Kevin Buzzard (Jan 22 2020 at 23:08):

You mean without using conv?

Yes.

#### 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.

#### Yury G. Kudryashov (Jan 22 2020 at 23:11):

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

#### Mario Carneiro (Jan 22 2020 at 23:11):

oof, kevin beat me with the conv

#### Mario Carneiro (Jan 22 2020 at 23:12):

use conv rw

#### Yury G. Kudryashov (Jan 22 2020 at 23:13):

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

#### Yury G. Kudryashov (Jan 22 2020 at 23:15):

I wanted to avoid explicit navigation.

#### 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 [].

#### Kevin Buzzard (Jan 22 2020 at 23:17):

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

#### 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]

#### 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 :-)

#### 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]


#### 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


#### 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.

#### Anne Baanen (Jan 23 2020 at 15:48):

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

#### Kevin Buzzard (Jan 23 2020 at 15:59):

There's always foo.symm

#### Anne Baanen (Jan 23 2020 at 16:01):

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

#### Kevin Buzzard (Jan 23 2020 at 16:02):

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

#### 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

#### Anne Baanen (Jan 23 2020 at 17:09):

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

#### 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