dependent rewriting

Stream: general

[Simon Hudon]

I just wrote a tactic for dependent rewriting. Is there any interest in having it in mathlib?

Here is what it does:

def foo' (i j : ℕ) (v : vector ℤ j) (h : i ≤ j) : Prop := i ≤ j

example (i : ℕ) (j : ℕ) (v : vector ℤ (j - i)) (h : i ≤ j - i) (h' : ∀ i, j - i = i) :
  foo' i (j - i) v h :=
begin
  dep_rw h',
--   i j : ℕ,
-- v : vector ℤ (j - i),
-- h : i ≤ j - i,
-- h' : ∀ (i : ℕ), j - i = i
-- ⊢ foo' i i (cast _ v) (cast _ h)
end

f has a dependent type and rewriting j requires to add a cast to v and h at the same time which is pretty tricky to do. That's why dependent rewriting can be handy in those situations. The norm in mathlib is to try to avoid this kind dependent function type. When you have to use them though, it's good to have a tactic that accommodates them.

[Reid Barton]

Yes, this would be extremely useful.

[Reid Barton]

Would it be practical to make rw itself do this?

[Simon Hudon]

I don't believe so. I think rw does its job by finding occurrences of the lhs and abstracting them so you don't need a complex tree rewriting. In order to make it dependent, I need to use the congruence lemmas that congr generates

[Simon Hudon]

Unless you use dependent rewriting as a sort of plan B if the motive is not type correct

[Reid Barton]

If it's not practical to make rw do this automatically then perhaps we can at least change the "motive is not type correct" error to mention dep_rw.

[Simon Hudon]

That makes sense. We should probably get it into core in that case

[Bhavik Mehta]

When I get the motive error, I sometimes think about using simp_rw instead. How does this differ from that?

[Simon Hudon]

Actually, I'm not familiar with simp_rw. Does it insert cast for you?

[Bhavik Mehta]

I don't think it does - taking a closer look I think your tactic is just cleverer than simp_rw in terms of working with dependent functions

[Yury G. Kudryashov]

simp_rw is a sequence of simp only

[Yury G. Kudryashov]

Someone's it's useful to avoid loops

[Kevin Buzzard]

Oh that's the point of it!

[Bhavik Mehta]

I sometimes use it when my goal state has a term which contains a proof (eg f x h, where x is data and h is a proof involving x), and I want to rewrite something like x = y - rw gives everyone's favourite motive error but simp_rw sometimes works

[Yakov Pechersky]

Would this rw tactic help here? Neither rw not simp_rw work:

import data.vector2

variables {α β : Type}
variable {n : ℕ}

def vector.last (v : vector α (n + 1)) : α := v.nth (fin.last n)

lemma vector.last_def (v : vector α (n + 1)) : v.last = v.nth (fin.last n) := rfl

lemma vector.to_list_reverse (v : vector α n) : v.reverse.to_list = v.to_list.reverse := rfl

lemma vector.reverse_nth_zero (v : vector α (n + 1)) : v.reverse.head = v.last :=
begin
  rw ←vector.nth_zero,
  rw vector.last_def,
  rw vector.nth_eq_nth_le,
  rw vector.nth_eq_nth_le,
  simp_rw vector.to_list_reverse,
  simp_rw [fin.val_eq_coe, fin.coe_last, fin.coe_zero],
  have : n = v.to_list.length - 1,
    { simp only [nat.add_succ_sub_one, add_zero, vector.to_list_length] },
  simp_rw [this], --breaks here
  sorry,
end

[Simon Hudon]

Can you show what the goal is at the point where it breaks?

[Yakov Pechersky]

lemma vector.reverse_nth_zero (v : vector α (n + 1)) : v.reverse.head = v.last :=
begin
  rw ←vector.nth_zero,
  rw vector.last_def,
  rw vector.nth_eq_nth_le,
  rw vector.nth_eq_nth_le,
  simp_rw vector.to_list_reverse,
  simp_rw [fin.val_eq_coe, fin.coe_last, fin.coe_zero],
  have : n = v.to_list.length - 1,
    { simp only [nat.add_succ_sub_one, add_zero, vector.to_list_length] },
    /-
invalid simplification lemma 'this' (use command 'set_option trace.simp_lemmas true' for more details)
state:
α : Type,
n : ℕ,
v : vector α (n + 1),
this : n = v.to_list.length - 1
⊢ v.to_list.reverse.nth_le 0 _ = v.to_list.nth_le n _
-/

  simp_rw [this], --breaks here
  sorry,
end

[Yakov Pechersky]

I do have a proof for the lemma though, avoiding the issue:

lemma vector.reverse_nth_zero (v : vector α (n + 1)) : v.reverse.head = v.last :=
begin
  have : 0 = v.to_list.length - 1 - n,
    { simp only [nat.add_succ_sub_one, add_zero, vector.to_list_length, nat.sub_self,
                 list.length_reverse] },
  rw [←vector.nth_zero, vector.last_def, vector.nth_eq_nth_le, vector.nth_eq_nth_le],
  simp_rw [vector.to_list_reverse, fin.val_eq_coe, fin.coe_last, fin.coe_zero, this],
  rw list.nth_le_reverse,
end

[Reid Barton]

Yes, this is exactly the sort of situation in question--you can't simply rewrite n because the type of the following proof depends on it

[Yakov Pechersky]

But rewriting 0 does work, even though the nth_le 0 _ proof relies on it too.

[Simon Hudon]

Do you rewrite it to something definitionally equal?

[Yakov Pechersky]

I don't think 0 = v.to_list.length - 1 - n are defeq, since I require that 5 lemma simp only to prove that.

[Reid Barton]

I think there are weird conditions where rewriting can work even in the presence of proofs because the way rw works means that it also rewrites the proof

[Yakov Pechersky]

Totally. The other steps in simp_rw are able to do that rewrite too. Interestingly, the last rw list.nth_le_reverse in my functional proof will not work if I use simp_rw instead.

[Eric Wieser]

Would dep_rw help with my goal in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Difficulty.20with.20dependent.20rewrites/near/214686669?

[Simon Hudon]

I think it might

[Yakov Pechersky]

Another vector use case. Often, rw <- vector.cons_head_tail v fails since v is in proofs. But simp_rw <- vector.cons_head_tail v results in deep recursion.

[Mario Carneiro]

use the single_pass option perhaps?

[Mario Carneiro]

actually it might be easier to do rcases on \exists h t, v = h :: t if you are trying to eliminate it

[Yakov Pechersky]

Great advice, thanks!