How do I unwrap array access in a proof?

Stream: general

[Shelvacu]

This is the simplest possible example for what I'm trying to do:

theorem aaaa {α : Type} (x : α) : x = #[x][0] := by sorry

α : Type
x : α
⊢ x = #[x][0]

if I try to simp [Array.instGetElemNatLtSize] it goes into a stackoverflow

And perhaps more importantly, is there a better way I could've figured this out without asking here? Lean state search wasnt helpful and neither was leansearch. I feel like this is a really simple/basic proof, is there some list somewhere of "when your proof looks like this, you probably want this tactic"?

[Kyle Miller]

Here you might guess that indexing an array ought to be equal by definition, and it turns out to work:

theorem aaaa {α : Type} (x : α) : x = #[x][0] := by rfl

[Shelvacu]

wait what? Why does simp not work when rfl does?

[Kyle Miller]

Or you might guess that there's a simp lemma out there that would work, and indeed there is:

theorem aaaa {α : Type} (x : α) : x = #[x][0] := by
  -- simp? produces
  simp only [List.getElem_toArray, List.getElem_cons_zero]

[Kyle Miller]

(simp on its own works with just Lean imported, and I used simp? to see what it did)

[Kyle Miller]

How did you come across using Array.instGetElemNatLtSize as something to unfold?

[Shelvacu]

okay something weird is going on here, when I recreate the exact proof state using a theorem it works just fine, but doesn't work in the actual proof

[Kyle Miller]

You could try setting pp.explicit (or pp.all) to true to see if there are some small differences.

Or you could try by congr! from within your actual proof to see what the differences are, if they're not otherwise resolvable.

[Shelvacu]

Okay I was able to fix it, and from that extract what I think is an actual reproduction of the issue:

def theSize : Nat := 1

def make (x : UInt8) : Vector UInt8 theSize := Vector.singleton x

def access (data : Vector UInt8 theSize) : UInt8 := data[0]

theorem cccc (x : UInt8) : x = access (make x) := by
  simp [access, make]
  -- look at this proof state
  simp [theSize]

x : UInt8
⊢ x = { toArray := #[x], size_toArray := ⋯ }[0]

there's no mention of theSize, but it's secretly still there wreaking havok. pp.explicit was able to show it, thank you.

[Shelvacu]

Kyle Miller said:

How did you come across using Array.instGetElemNatLtSize as something to unfold?

roughly: I know the var[idx] desugars to a function call, and I probably want to unfold that function call (because nothing else was working), and then from there I was able to dig through the docs and find the right instance

[Shelvacu]

At a more general level, I come from a programming background, not a math background, and I've definitely been kinda throwing stuff at the wall and seeing what sticks when it comes to proofs.

[Shelvacu]

congr also works, though I don't understand why

[Kyle Miller]

Fun fact: rfl still works there.

theorem cccc (x : UInt8) : x = access (make x) := by rfl

[Kyle Miller]

Shelvacu said:

and then from there I was able to dig through the docs and find the right instance

Ok, I was curious if some AI system was leading you astray.

In the future, unfolding instances alone is usually not helpful. Mathlib has unfold_projs that sometimes illuminates some things. It unfolds projections of instances, which can bring you towards understanding definitions.

[Kyle Miller]

Did you do congr and not congr!? These are different tactics. (One day I hope congr! will be upstreamed into congr.)

I think it works here because rfl works, so it's not doing anything special.

[Shelvacu]

I tried both, they both solve it.

[Kyle Miller]

There's a debugging flag here, and "no passes succeeded" followed by "Dispatched goal by post-processing step." pretty much means we can assume that congr! succeeds because it tries rfl.

set_option trace.congr! true
theorem cccc (x : UInt8) : x = access (make x) := by
  congr!
/-
[congr!] Default smartHCongr? failed, trying LHS/RHS method
[congr!] trying to apply congr lemma ∀ (data data' : Vector UInt8 theSize), data = data' → HEq (access data) (access data')
[congr!] failed to apply congr lemma ▶
[congr!] no passes succeeded
[congr!] Dispatched goal by post-processing step.
-/

[Kyle Miller]

(My suggestion of congr! makes more sense when there are things that look like they should be equal but aren't for some hidden reason. It's not useful here.)