## Stream: maths

### Topic: fixing subst in core

#### Scott Morrison (Apr 04 2020 at 05:12):

I've sorted out a source of inconvenient eq.recs that I've been suffering from, and it's very simple, and probably easily fixable in core. (Thanks @Reid Barton for the reminders to track problems to their origin instead of patching things afterwards...)

In

def f (a b : ℕ) (h : a = b) : ℕ :=
by { subst h, exact 0}

#print f


we see

def f : Π (a b : ℕ), a = b → ℕ :=
λ (a b : ℕ) (h : a = b), eq.rec 0 h


which is perhaps unsurprising given we used subst. With pp.all, we see

def f : Π (a b : nat), @eq.{1} nat a b → nat :=
λ (a b : nat) (h : @eq.{1} nat a b), @eq.rec.{1 1} nat a (λ (b : nat), nat) (@has_zero.zero.{0} nat nat.has_zero) b h


and observe that we're doing eq.rec transport through the family (λ (b : nat), nat), which in particular is a constant family (the fibre doesn't depend on the base), and so the whole eq.rec term is equal (but not definitionally) to just 0. (See eq_rec_constant.)

Now, it's possible to clean up after the fact, but painful (and you have to know it's happening).

Could we just change the behaviour of subst, to detect when the target doesn't even depend on the substitution we're doing (i.e. the eq.rec it wants to generate is through a constant family), and avoiding producing the eq.rec?

#### Reid Barton (Apr 04 2020 at 13:23):

Why invoke subst in the first place though? Some automation thing?

#### Chris Hughes (Apr 04 2020 at 15:41):

I'm not sure, but I think one way around it might be to only ever use eq.mp for data, and use eq.rec to prove the proof obligation that the two goals are equal after substituting a = b. Then I think you're guaranteed the right definitional equality whenever the two types before and after applying eq.mp are definitionally equal.

#### Mario Carneiro (Apr 04 2020 at 15:51):

the definitional behavior of eq.rec and eq.mp are basically the same

#### Reid Barton (Apr 04 2020 at 15:57):

I think Chris's point is that if you go through eq.mp, its argument is a proof of (in this case) nat = nat and so it's definitionally equal to rfl however you constructed it.

#### Reid Barton (Apr 04 2020 at 15:57):

By definitional proof irrelevance, not by construction

#### Chris Hughes (Apr 04 2020 at 15:58):

Say I used funext to prove h : f = g, where f g : nat - > nat. Then eq.rec_on h (fin (g 2)) does not reduce, but eq.mp (eq.rec_on h rfl) (fin (g 2)) does.

I'm on my phone

#### Kevin Buzzard (Apr 04 2020 at 15:59):

and you're checking things reduce??

#### Mario Carneiro (Apr 04 2020 at 16:01):

Oh I see. Yes that should work. But lean doesn't have to guess here, it knows when the sides are defeq and just skip emitting the term

#### Chris Hughes (Apr 04 2020 at 16:05):

I assumed this is why rw always uses eq.mpr. If indeed it does, I can't check right now.

#### Patrick Massot (Apr 04 2020 at 16:11):

Speaking of fixing core, is there any reason why simp_rw does not become the official rw?

#### Mario Carneiro (Apr 04 2020 at 16:58):

I haven't used it. What's the difference?

#### Patrick Massot (Apr 04 2020 at 17:17):

https://leanprover-community.github.io/mathlib_docs/tactics.html#simp_rw

#### Andrew Ashworth (Apr 04 2020 at 17:23):

is this going to make my rw much slower in big proofs?

#### Mario Carneiro (Apr 04 2020 at 17:23):

I think that they have different use cases and different behavior

#### Mario Carneiro (Apr 04 2020 at 17:24):

In DTT it's not clear whether one mechanism (congr lemmas vs eq.rec) dominates the other

#### Kevin Buzzard (Apr 04 2020 at 17:24):

It might even break your big proofs! It might simplify too much I guess?

#### Patrick Massot (Apr 04 2020 at 17:24):

I'm only using simp_rw as "rw that works under binders".

#### Kevin Buzzard (Apr 04 2020 at 17:25):

right but in theory it might rewrite under a binder which it didn't do before, if something occurs both inside and outside

#### Reid Barton (Apr 04 2020 at 17:27):

You also don't always want to rewrite repeatedly

#### Mario Carneiro (Apr 04 2020 at 17:32):

Here is an example where the simp strategy fails and rw works

example : ∀ (p : 1 + 1 = 3 → Prop) h, p h :=
begin
have : (1 + 1 = 3) = false := sorry,
simp only [this], -- fails
rw [this], -- works
end


#### Gabriel Ebner (Apr 04 2020 at 17:33):

Empirically speaking, I would find it interesting to know how many rw invocations in mathlib could be replaced by simp_rw.

#### Kevin Buzzard (Apr 04 2020 at 17:52):

I would be interested to know how many erwinvocations in the perfectoid project could be replaced with simp_rw

#### Reid Barton (Apr 04 2020 at 17:54):

Probably none unless I misunderstood the purpose of simp_rw

#### Kevin Buzzard (Apr 04 2020 at 17:56):

My algorithm for rewriting under binders used to be: (1) try rw and then remember it doesn't work (2) try erw (3) try simp only (4) whine to co-authors

#### Reid Barton (Apr 04 2020 at 17:56):

erw doesn't rewrite under binders, it rewrites up to definitional equality. I guess if you're lucky enough that might look like rewriting under binders?

#### Scott Morrison (Apr 05 2020 at 01:11):

@Reid Barton, the subst in question that I'm concerned about is in equiv_rw. I agree it may be viable to decide whether or not to actually use subst here, but my point is just that the only eq.recs this subst is generating that cause problems are unnecessary ones!

#### Reid Barton (Apr 05 2020 at 01:13):

I mean, "don't use subst to construct data" seems like a sound general principle, whether or not there are some edge cases where it happens not to do any harm (but doesn't seem to do any good either?)

#### Scott Morrison (Apr 05 2020 at 01:14):

Hmmm.... I'm not sure what to replace it with in equiv_rw.

#### Scott Morrison (Apr 05 2020 at 01:15):

Leaving that line out (or replacing it with clear) certainly breaks some of things things I want equiv_rw to do.

#### Scott Morrison (Apr 05 2020 at 01:15):

But maybe you're saying those things I want it to do, I shouldn't want.

#### Scott Morrison (Apr 05 2020 at 02:07):

Okay, perhaps I can avoid subst here after all.

#### Gabriel Ebner (Apr 05 2020 at 08:16):

For posterity, here is a stable link that will not change when new commits are pushed to master: https://github.com/leanprover-community/mathlib/blob/23681c3db3dc30695a97a769641a99511297f784/src/tactic/equiv_rw.lean#L207 (You can press y on the github page to get this link.)

#### Gabriel Ebner (Apr 05 2020 at 08:53):

More productively, I think it is useful to distinguish three cases here:

1. e : α ≃ β, a : α ⊢ ℕ (a does not occur as a dependency)
2. e : α ≃ β, a : α, h : 0 < a ⊢ ℕ (a only occurs as a dependency in hypotheses)
3. e : α ≃ β, a : α ⊢ 0 < a (a occurs in the target)

For 1, you don't need any eq.rec at all, probably the easiest way to handle it is assert+clear.
Case 2 should only require eq.rec on the hypotheses, which is probably fine since they're often propositions. But I don't see any easy way to implement this without introducing a β-redex in the produced term.
For 3, I don't think there's any way around subst (or another way to produce eq.rec).

#### Mario Carneiro (Apr 05 2020 at 09:24):

I'm not sure that you can do case 2 with eq.rec in the hypotheses only, or at least not easily, because there could be dependencies in the hypotheses as well, for example e : α ≃ β, a : α, v : T a, h : v = 0 ⊢ ℕ. For this you would have to tuple the hypotheses up or something, and I'm not convinced the result is better than just revert and eq.rec the goal

#### Mario Carneiro (Apr 05 2020 at 09:26):

Plus, this has the potential to compromise one of the things I like most about subst, which is that it works in any situation, cleaning up all sorts of DTT hell

#### Mario Carneiro (Apr 05 2020 at 09:27):

I think it is reasonable to detect when subst would have an equivalent effect to clear and do that instead, but otherwise I think having a reliable term being produced is useful

#### Gabriel Ebner (Apr 05 2020 at 09:27):

Oh, these changes are not meant for subst. The subst tactic should really stay as it is.

Last updated: May 14 2021 at 18:28 UTC