rw inside of List.get

Stream: new members

[Alex Meiburg]

I have two lists that are equal and I want to simplify a List.get expression using this. My understanding is that rw can't do this, because of the dependent typing of the i argument to get? So, I understand the problem, but not how to resolve it. :) Any help?

mwe of the problem I'm facing (obviously a very silly looking example, but mwe's usually are):

theorem foobar {l₁ l₂ : List ℝ} (h : l₁ = l₂) : l₁ = l₂ := by
  apply List.ext_get
  case hl => rw [h]
  intro n hn₁ hn₂
  -- rw [h]
  -- nope, "tactic 'rewrite' failed, motive is not type correct"

  -- simp [h]
  -- nope, "simp made no progress"

  -- conv =>
  --   lhs
  --   arg 1
  -- nope, "cannot select argument"
  sorry

[Yongyi Chen]

subst h followed by rfl worked for me. Wonder what subst h; rfl would expand to (rather, what its tactic equivalent would be) without using the subst tactic though.

[Alex Meiburg]

ah, that's what I needed! I guess when I use rw I'm really usually just using it for subst. I wasn't aware that subst could "go in" where rw can't. Thanks!

[Notification Bot]

Alex Meiburg has marked this topic as resolved.

[Kyle Miller]

If subst h doesn't work (because it's an equality between list expressions that aren't variables) you could try congr!, which works here

[Alex Meiburg]

It seems like every day I learn a few new tactics that I wish I had known about for a while now :')

[Notification Bot]

Alex Meiburg has marked this topic as unresolved.

[Kyle Miller]

congr! can "select" arguments that are hard to select. It closes the goal because it uses assumption to try to clean things up.

[Alex Meiburg]

oops, yes, this actually isn't what I need. I forgot that subst only works on equalities of variables. Really, I want to rewrite that l1 = a::ls, and then do quite a bit further manipulation... so my mwe doesn't capture either of those issues. I'll try to make a better mwe I guess?

[Kyle Miller]

When you have functions that don't work right with simp, you can write @[congr] lemmas to help it rewrite at each argument. Here's a possible one for List.get, but a downside with this particular one is that it inserts Fin.cast expressions, which isn't great.

import Mathlib.Tactic

@[congr]
theorem List.congr_get {α : Type*} {l₁ l₂ : List α} (h : l₁ = l₂)
    {i₁ i₂ : Fin l₁.length} (hi : i₁ = i₂) :
    l₁.get i₁ = l₂.get (i₂.cast congr(length $h)) := by
  subst_vars
  rfl

theorem foobar {l₁ l₂ : List ℝ} (h : l₁ = l₂) : l₁ = l₂ := by
  apply List.ext_get
  case hl => rw [h]
  intro n hn₁ hn₂
  simp_rw [h]
  /-
  ⊢ List.get l₂ (Fin.cast _ { val := n, isLt := hn₁ }) = List.get l₂ { val := n, isLt := hn₂ }
  -/

[Kyle Miller]

I guess you could also use this congr lemma, which could be better, since it ought to at least let simp eliminate the Fin.cast a bit earlier (though it won't in your example).

@[congr]
theorem List.congr_get {α : Type*} {l₁ l₂ : List α} (h : l₁ = l₂)
    {i₁ : Fin l₁.length} {i₂ : Fin l₂.length} (hi : i₁.cast congr(length $h) = i₂) :
    l₁.get i₁ = l₂.get i₂ := by
  subst_vars
  rfl

(I didn't know this was a legal congr lemma until now!)

[Alex Meiburg]

Well, I can't say I totally understand why that lets congr solve things it otherwise couldn't, but cool thanks! :) It seems like it does resolve my issue, I think...

[Notification Bot]

Alex Meiburg has marked this topic as resolved.

[Kyle Miller]

@Alex Meiburg It's not for congr, but for simp (and simp_rw). Here's a model for you for how simp does its rewriting. Say you want to run simp on a goal e. What simp's job is is to come up with an equality e = e' with e' the result of simplification, and then it rewrites e using this equality.

So, it sets up the goal e = ?e' with the RHS a metavariable, and then it does the following recursive procedure. It finds an appropriate "congruence lemma" given specific features of e (it is able to generate its own, but you can give it custom congruence lemmas like I did for List.get when it needs help). Then it essentially uses apply with this congruence lemma. This results in some number of hypotheses (two in the case of List.congr_get) of the same x = ?x' form, corresponding to sub-parts of e, and then it recurses.

[Kyle Miller]

Somewhere in here it uses @[simp] lemmas to actually come up with simplifications to particular subexpressions, rather than just using the congruence lemmas to navigate into the subexpressions.

[Notification Bot]

Alex Meiburg has marked this topic as unresolved.

[Alex Meiburg]

I see, okay. I'm still struggling with anything involving List.get, I think the dependent types or something are just making my life miserable. My state looks like this (modulo some irrelevant hypotheses):

α: Type u_2
inst: Semiring α
P: α[X]
n: ℕ
hn: n < natDegree P + 1
this: natDegree P ≥ 1
hn₂: ¬n = 0
⊢ coeff P
    (List.get (List.reverse (List.range (natDegree P + 1)))
      { val := n, isLt := (_ : n < List.length (List.reverse (List.range (natDegree P + 1)))) }) =
  List.get (leadingCoeff P :: List.replicate (natDegree P) 0)
    { val := n, isLt := (_ : n < Nat.succ (List.length (List.replicate (natDegree P) 0))) }

There's all these nice lemmas about List.get, like List.get_reverse, but I can't seem to apply any of them. Or like, if I have that n=0, then I would like to use List.get_cons_zero since I have List.get (... :: ...) { val := 0, ... }, but I can't seem to apply it. The congr lemma you shared fixed some issues but it's still saying no every step of the way...

I think maybe I'm just fundamentally ignorant about how to handle things when the Fin argument to get are dependent on the list, and then the Fin.isLt is dependent on the Fin.val... ugh

[Alex Meiburg]

I see, okay. I'm still struggling with anything involving List.get, I think the dependent types or something are just making my life miserable. My state looks like this (modulo some irrelevant hypotheses):

α: Type u_2
inst: Semiring α
P: α[X]
n: ℕ
hn: n < natDegree P + 1
this: natDegree P ≥ 1
hn₂: ¬n = 0
⊢ coeff P
    (List.get (List.reverse (List.range (natDegree P + 1)))
      { val := n, isLt := (_ : n < List.length (List.reverse (List.range (natDegree P + 1)))) }) =
  List.get (leadingCoeff P :: List.replicate (natDegree P) 0)
    { val := n, isLt := (_ : n < Nat.succ (List.length (List.replicate (natDegree P) 0))) }

There's all these nice lemmas about List.get, like List.get_reverse, but I can't seem to apply any of them. Or like, if I have that n=0, then I would like to use List.get_cons_zero since I have List.get (... :: ...) { val := 0, ... }, but I can't seem to apply it. The congr lemma you shared fixed some issues but it's still saying no every step of the way...

I think maybe I'm just fundamentally ignorant about how to handle things when the Fin argument to get are dependent on the list, and then the Fin.isLt is dependent on the Fin.val... ugh

[Alex Meiburg]

At this point I don't even know how to make a good mwe. I can't even use the proof state as an example because of the underscores in the goal... and I don't know how to handle those :(

[Kyle Miller]

Could you use docs#List.get! instead of List.get so that you could avoid dependent types?

[Alex Meiburg]

Maybe. I really want to use List.ext_get, and there doesn't seem to be a List.ext_get! -- yet. (Say that three times quickly...) Maybe I'll just prove a List.ext_get! and then use that. Doesn't seem like it should be too bad! And then I can avoid this madness haha

[Yongyi Chen]

By the way, here's another way I found that's really tricky (path induction):

induction h with
| refl => rfl

[Yongyi Chen]

I think this is similar to subst h under the hood, but they're different in one way: induction uses Eq.rec while subst uses Eq.ndrec (at least in this case).

[Notification Bot]

Yongyi Chen has marked this topic as unresolved.

[Kyle Miller]

@Yongyi Chen Is that different from doing cases h? That's a common trick for handling the case when h is an equality involving constructors

[Yongyi Chen]

Using by? I see that the expansion of cases h also uses Eq.ndrec but also wraps the expression in an Eq.casesOn.

[Kyle Miller]

(I think the big difference between subst and cases is that the latter does "dependent elimination", meaning it can handle more equalities than just those with a free variable on one side. induction is very similar to cases, maybe even the same in what it can do)

[Yongyi Chen]

Makes sense, subst h and rcases h with rfl expand to the same thing. So rcases (or cases) is more general.

[Kyle Miller]

Is there some inference about subst vs induction that you're drawing regarding Eq.rec vs Eq.ndrec? Or is that a difference you noticed between them?

[Yongyi Chen]

I noticed the difference using by?. I don't claim to understand too much.

[Yongyi Chen]

Induction doesn't seem to be too happy in this example:

example {a b : ℕ} (ha : a < 10) (hb : b < 10) (h : Fin.mk a ha = Fin.mk b hb) : a = b := by
  induction h with
  /-
  index in target's type is not a variable (consider using the `cases` tactic instead)
    { val := b, isLt := hb }
  -/
  | refl => sorry

[Kyle Miller]

Ah, ok, induction has a subst-like restriction. (The "indices" for the Eq type are the x and y in x = y). It's cases that knows how to carry out dependent elimination, where it sees that h is the same as a = b and ha = hb (though ha and hb are propositions, so it might just ignore them)

[Kyle Miller]

(I don't really know what dependent elimination is beyond having experience with Lean's error messages that complain when cases can't do it.)

[Alex Meiburg]

The first step to sanity

/-- If two lists are the same length and get! is the same on all indices, the lists are equal. -/
theorem List.ext_get! [Inhabited α] (hl : length l₁ = length l₂)
    (h : ∀ n, get! l₁ n = get! l₂ n) : l₁ = l₂ :=
  ext fun n => by
      cases h₃ : get? l₁ n <;> cases h₄ : get? l₂ n
      case none.none => rfl
      case none.some => exfalso; linarith [get?_eq_none.mp h₃, (get?_eq_some.mp h₄).1]
      case some.none => exfalso; linarith [get?_eq_none.mp h₄, (get?_eq_some.mp h₃).1]
      case some.some => congr; exact (get!_of_get? h₃) ▸ (get!_of_get? h₄) ▸ h n