Using List.get in Vector.Basic

Stream: mathlib4

[Arien Malec]

I'm porting Data.Vector.Basic and the mapping from Vector.nth to List.get is foundational, but this was previously spelled List.nthLe

I'd like to get the following working:

import Mathlib.Data.Vector

namespace Vector

theorem length_coe (v : Vector α n) :
    ((coe : { l : List α // l.length = n } → List α) v).length = n :=
  v.2

-- deprecate
theorem nth_eq_nth_le :
    ∀ (v : Vector α n) (i), nth v i = v.toList.nthLe i.1 (by rw [toList_length] ; exact i.2)
  | ⟨_, _⟩, _ => rfl

-- replace
theorem nth_eq_get :
    ∀ (v : Vector α n) (i), nth v i = v.toList.get i (by rw [toList_length] ; exact i.2)
  | ⟨_, _⟩, _ => rfl

end Vector

I'm getting errors on the first theorem:

type mismatch
  v.property
has type
  List.length v.val = n : Prop
but is expected to have type
  List.length (coe v) = n : Prop

and I don't understand Lean 3 to Lean 4 coercion handling well enough to understand the fix.

With that in hand, I want to use it to tell the second theorem that I have i: Fin (length (toList v))

[Yury G. Kudryashov]

There is no coe function in Lean 4.

[Yury G. Kudryashov]

Lean 4 unfolds coercions, so you can use Subtype.val directly.

[Yury G. Kudryashov]

For other theorems, you need something like docs#fin.cast

[Yury G. Kudryashov]

Do we have it in Lean 4?

[Arien Malec]

docs4#Fin.cast ?

[Arien Malec]

or docs4#Fin.coe_cast

[Yury G. Kudryashov]

Fin.cast

[Arien Malec]

It turns out that lemma is seemingly useless. I need a proof that the round trip preserves the length. Hmm.

[Yury G. Kudryashov]

What exactly do you need? I mean, can you post a lemma statement without a proof?

[Arien Malec]

I believe with:

@[simp]
theorem length_toList (v: Vector α n): Fin n = Fin ((v.toList).length) := by sorry

gets me there?

[Arien Malec]

wait...

[Arien Malec]

that gets me a type; can I use it in the declaration?

[Arien Malec]

Where I'm trying to get is:

theorem nth_eq_get :
    ∀ (v : Vector α n) (i), nth v i = v.toList.get i := sorry

So I need to recast i, which is Fin n to Fin (v.toList.length), so I think I need to prove the above...

[Arien Malec]

If I follow your hints on Fin.cast, I need an Equiv to do that instead...

[Arien Malec]

Which brings me full circle back to length_coe

@[simp]
theorem length_coe (v : Vector α n) :
    ((coe : { l : List α // l.length = n } → List α) v).length = n :=
  v.2
#align vector.length_coe Vector.length_coe

@[simp]
theorem length_toList (v: Vector α n) : n = v.toList.length := by
  simp only [length_coe]

[Yury G. Kudryashov]

You can use (not tested)

@[simp] theorem length_val (v : Vector α n) : v.val.length = n := v.2

@[simp] theorem length_toList (v : Vector α n) : v.toList.length = n := v.2

@[simp] theorem nth_eq_get (v : Vector α n) (i : Fin n) :
    v.nth i = v.toList.get (Fin.cast v.length_toList.symm i) :=
  rfl

[Yury G. Kudryashov]

BTW, I think that RHS should be the definition of Vector.nth (and it should be called Vector.get).

[Arien Malec]

Yury G. Kudryashov said:

BTW, I think that RHS should be the definition of Vector.nth (and it should be called Vector.get).

I agree -- was defined upstream of this file, but will do a PR to deprecate nth and #align to get

[Yury G. Kudryashov]

You can just replace the definition, no need to deprecate.

[Yury G. Kudryashov]

Just use get instead of nth everywhere and #align vector.nth Vector.get

[Yury G. Kudryashov]

Note that Fin.cast preserves val: (Fin.cast h i).val = i.val is a rfl. Can't say the same about Eq.cast.

[Yury G. Kudryashov]

(at least, I'm not sure).

[Yury G. Kudryashov]

Also, I know that definitions that use pattern matching break rfl equalities in Lean 3. If this is the case in Lean 4, then we should avoid them.

[Yury G. Kudryashov]

It's not the case in Lean 4:

def test : ℕ × ℕ → ℕ × ℕ
  | (a, b) => (a + 1, b + 1)

lemma test_fst (x : ℕ × ℕ) : (test x).1 = x.1 + 1 := rfl -- works

[Yury G. Kudryashov]

So, no need to worry about this.

[Reid Barton]

I believe this is a side effect of eta for structures (here x).