List access error

Stream: new members

[Andy Jiang]

Hi I have a question about the error Lean is throwing in the following setup
I have some list prime_factors_sorted together with a proof that the length is at least 2. The following code throws an error

*some code here*
  have : prime_factors_sorted.length ≥ 2 := by simp; exact h₄
    let p := prime_factors_sorted[0]
    let q := prime_factors_sorted[1]

namely:
failed to prove index is valid, possible solutions:

- Use have-expressions to prove the index is valid
- Use a[i]! notation instead, runtime check is perfomed (sic), and 'Panic' error message is produced if index is not valid
- Use a[i]? notation instead, result is an Option type
- Use a[i]'h notation instead, where h is a proof that index is valid

but

 have : prime_factors_sorted.length ≥ 2 := by simp; exact h₄
    let p := prime_factors_sorted[(0 : Fin 2)]
    let q := prime_factors_sorted[1]

works
Is this expected behavior?

[Julian Berman]

Can you have a quick look at #backticks and change your question so it uses them to be a bit easier to read?

[Julian Berman]

I suspect the answer is yes though just looking at the error message -- I guess it's slightly surprising 0 : Fin 2 works -- are you more surprised at the working example or the nonworking one?

[Andy Jiang]

Well I guess I just want to understand what's going on so it's less of a trial-and-error process. At first I tried inserting (0: Fin prime_factors_sorted.length) and it rejected that as well. I assume (0 : Fin 2) is not the "correct" way to index this list? What is the correct way to do it? (Assuming that my code is only working accidentally)

[Andy Jiang]

Is the correct way to do it
let p := prime_factors_sorted.get ⟨0, by omega⟩
?

[Kevin Buzzard]

Not the answer to your question but by simpa using h_4 is more idiomatic than the non-terminal simp. You haven't posted a #mwe -- is the error you're reporting on p or q? I don't see anything wrong with the approach using omega but it might be slow -- you might be better off just supplying a proof directly (maybe find the term using exact??)

[Andy Jiang]

Thanks for the reply, the #mwe for my original question is

import Mathlib.Data.List.Basic

variable (l : List ℕ)
variable {h : l.length ≥ 2}

def a := l[0]
def b := l[1]
def c := l[(0 : Fin l.length)]
def d := l[(0 : Fin 2)]
def e := l.get ⟨0,by exact Nat.zero_lt_of_lt h⟩
def f := l.get ⟨0,by omega⟩

here a and c fail and the rest work.
By the way, I also am confused why omega works sometimes but not other times under seemingly the same hypotheses. For example

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Linarith

theorem easy (n m: ℕ): n < m-1 → m+1 > n := by
  intro h
  omega

theorem easy2 (m: ℕ) (n : Fin (m-1)): m+1 > n.val := by
  let h : (n.val < m-1) := n.isLt
  omega

theorem easy3 (m: ℕ) (n : Fin (m-1)): m+1 > n.val := by
  let h : (n.val < m-1) := n.isLt
  let p : ℕ := n.val
  have h2 : (p = n.val) := by
    tauto
  rw [← h2];rw [← h2] at h
  omega

The first one works but the second and third don't even though in the third example the tactic state is basically the same just with some extra assumptions.

[Eric Wieser]

Please take another look at #backticks and edit your message; you need three backticks not just one

[Kevin Buzzard]

c doesn't work because 0 : Fin n doesn't make sense in general (because n might be 0), and Lean is not going to magically spot that in this case it can't be 0 -- you have to tell it (Lean does not even "know" that x >= 2 implies x = t + 1 for some t, again this needs a proof; it's not hard but it must be present).

[Andy Jiang]

Thanks, mainly I'm trying to understand why b works but not a. Lean is doing some automatic inferences under the hood to get b to work right? Is it some search-boundary that's preventing it from doing a?

[Julian Berman]

I don't know the direct answer to your question, but from changing 2 to 3 I think we see that it has something to do with the last index, and that's all Lean is aware of -- as you say, yeah, however this feature works, Lean is trying to prove the index is valid, and that seems to be doing so correctly only for the last index. I think to understand why we have to find what tactic is being used to prove the length is longer and that'll answer the question, but I'm not sure yet how to do so, trying to figure that out myself

[Julian Berman]

(What I changed your code to is simply:

import Mathlib.Data.List.Basic

variable (l : List ℕ)
variable {h : 3 < l.length}

def a0 := l[0]
def a1 := l[1]
def a2 := l[2]
def a3 := l[3]
def c := l[(0 : Fin l.length)]
def d := l[(0 : Fin 2)]
def e := l.get ⟨0,by exact Nat.zero_lt_of_lt h⟩
def f := l.get ⟨0,by omega⟩

where you'll see that no matter what, if you play with the 2 numbers, only the last index is proven correctly
)

[Julian Berman]

OK simply grepping for the error message says the answer is get_elem_tactic, and that that basically tries either trivial or else simp (config := { arith := true })

[Julian Berman]

(I am brain dumping in case this is helpful to you for figuring out how to answer the question -- someone else I'm sure will straight up just know the answer)

[Julian Berman]

OK and it looks like get_elem_tactic is meant to be extensible -- which means there's a chance Mathlib extends it to use a more powerful tactic, but that you/we haven't imported enough to make that happen. Let's see... I guess by grepping through mathlib for that tactic.

[Julian Berman]

No that doesn't appear in Mathlib, so it looks like the answer is "no". omega discharged your goal there -- I know it's new -- not sure if it's a candidate for making these more automatic in all those cases, now I think I've exhausted what I'd be able to figure out quickly on my own

[Julian Berman]

Yeah, adding:

macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)

makes all those examples work automatically. I have no idea how bad of an idea that is, now someone who knows more will teach us both, or tell us to PR that.

[Andy Jiang]

ah ok so Lean tries some tactics automatically here and those tactics only can solve the less than one case. thanks for the help!

[Andy Jiang]

actually even more confusing to me is the failure of omega in the second example above. It seems like the tactic state is the same (with some extra junk) but omega fails when you add more hypotheses into the tactic state. This is really confusing to me

[Julian Berman]

Which second example? Here, all examples (other than the Fin l.length one) pass.

[Andy Jiang]

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Linarith

theorem easy (n m: ℕ): n < m-1 → m+1 > n := by
  intro h
  omega

theorem easy2 (m: ℕ) (n : Fin (m-1)): m+1 > n.val := by
  let h : (n.val < m-1) := n.isLt
  omega

theorem easy3 (m: ℕ) (n : Fin (m-1)): m+1 > n.val := by
  let h : (n.val < m-1) := n.isLt
  let p : ℕ := n.val
  have h2 : (p = n.val) := by
    tauto
  rw [← h2];rw [← h2] at h
  omega

This example I made up. Perhaps I should start a new thread about this. It's kind of confusing why omega fails sometimes but not other times to me

[Julian Berman]

I can't say I understand which kinds of goals omega is meant for either, but the last two statements are quite different from the first one -- you firstly have natural subtraction there which I know doesn't have a great reputation for behaving sanely.

[Mario Carneiro]

omega is supposed to be able to handle nat subtraction, although IIRC it has some iterative splitting thing to handle it and it's possible there are bugs in it

[Kevin Buzzard]

omega is new this week so if we can isolate some bugs that would be helpful