simp vs rw

Stream: general

[Yury G. Kudryashov]

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]

You mean without using conv?

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

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]

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

[Mario Carneiro]

oof, kevin beat me with the conv

[Mario Carneiro]

use conv rw

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

I wanted to avoid explicit navigation.

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

There's always foo.symm

[Anne Baanen]

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

[Kevin Buzzard]

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

[Anne Baanen]

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]

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

[Mario Carneiro]

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