fixing `subst` in core

Stream: maths

[Scott Morrison]

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]

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

[Chris Hughes]

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]

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

[Reid Barton]

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]

By definitional proof irrelevance, not by construction

[Chris Hughes]

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.

[Chris Hughes]

I'm on my phone

[Kevin Buzzard]

and you're checking things reduce??

[Mario Carneiro]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Andrew Ashworth]

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

[Mario Carneiro]

I think that they have different use cases and different behavior

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

You also don't always want to rewrite repeatedly

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

Probably none unless I misunderstood the purpose of simp_rw

[Kevin Buzzard]

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]

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]

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

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Okay, perhaps I can avoid subst here after all.

[Gabriel Ebner]

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]

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]

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]

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]

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]

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