Substitute local let binding

Stream: general

[Nikolai Morin]

In implementing a 2D Array indexing operation, I'm stuck at how to substitute a let binding like this:

def get
  (mat : Mat m n α)
  (i_m : Fin m)
  (i_n : Fin n)
: α :=
  let idx : Nat := i_m.val * n + i_n.val
  let isLt : idx < mat.arr.size :=
       [...]
        have : i_m.val * n + i_n.val ≤ pred_m * n + pred_n := n_succ_pred_n ▸ this
        have : idx ≤ pred_m * n + pred_n := this -- here
        sorry
  mat.arr.get ⟨idx, isLt⟩

It's not an equality, so I can't use Eq.subst or the rw tactic.

[Yaël Dillies]

rfl should work

[Nikolai Morin]

If I write

have aux : idx = i_m.val * n + i_n.val := by simp; rfl

then rfl complains

type mismatch
  HEq.rfl
has type
  HEq ?m.3990 ?m.3990 : Prop
but is expected to have type
  ↑i_m✝ * n + ↑i_n✝ = ↑i_m * n + ↑i_n : Prop

I guess the cross means it's a shadowed variable? I didn't redefine i_m or i_n though. Here's the full function in case that's relevant:

full function

structure Mat (m : Nat) (n : Nat) (α : Type) where
arr : Array α
size_ok : arr.size = m * n
deriving Repr

def get
(mat : Mat m n α)
(i_m : Fin m)
(i_n : Fin n)
: α :=
let idx : Nat := i_m.val * n + i_n.val
let isLt : idx < mat.arr.size :=
match m with
| .zero => absurd i_m.isLt (Nat.not_lt_zero i_m.val)
| .succ pred_m =>
have hm₁ : i_m.val ≤ pred_m := Nat.le_of_lt_succ i_m.isLt
have hm₂ : i_m.val * n ≤ pred_m * n := Nat.mul_le_mul_right n hm₁
match n_succ_pred_n : n with
| .zero => absurd i_n.isLt (Nat.not_lt_zero i_n.val)
| .succ pred_n =>
have : i_n.val ≤ pred_n := Nat.le_of_lt_succ i_n.isLt
have : i_m.val * Nat.succ pred_n + i_n.val ≤ pred_m * Nat.succ pred_n + pred_n :=
Nat.add_le_add hm₂ this
have : i_m.val * n + i_n.val ≤ pred_m * n + pred_n := n_succ_pred_n ▸ this
have aux : idx = i_m.val * n + i_n.val := by simp; rfl
-- have : idx ≤ pred_m * n + pred_n := rfl
sorry
mat.arr.get ⟨idx, isLt⟩

[Yaël Dillies]

You should learn how to write functioning that someone can just paste to see what the problem is. Please see #mwe

[Nikolai Morin]

@Yaël Dillies Sorry, I've now added the missing Mat definition to my previous post and verified that it's self-contained.

[Yaël Dillies]

Oh I see, the problem is that the subsequent match creates new variables i_m and i_n instead of changing the type of the old ones but it doesn't create a new let binding for idx either. That's a bit dumb.

[Yaël Dillies]

This works, however,

structure Mat (m : Nat) (n : Nat) (α : Type) where
arr : Array α
size_ok : arr.size = m * n
deriving Repr

def get
(mat : Mat m n α)
(i_m : Fin m)
(i_n : Fin n)
: α :=
let idx : Nat := i_m.val * n + i_n.val
have aux : idx = i_m.val * n + i_n.val := rfl
let isLt : idx < mat.arr.size :=
match m with
| .zero => absurd i_m.isLt (Nat.not_lt_zero i_m.val)
| .succ pred_m =>
have hm₁ : i_m.val ≤ pred_m := Nat.le_of_lt_succ i_m.isLt
have hm₂ : i_m.val * n ≤ pred_m * n := Nat.mul_le_mul_right n hm₁
match n_succ_pred_n : n with
| .zero => absurd i_n.isLt (Nat.not_lt_zero i_n.val)
| .succ pred_n =>
have : i_n.val ≤ pred_n := Nat.le_of_lt_succ i_n.isLt
have : i_m.val * Nat.succ pred_n + i_n.val ≤ pred_m * Nat.succ pred_n + pred_n :=
Nat.add_le_add hm₂ this
have : i_m.val * n + i_n.val ≤ pred_m * n + pred_n := n_succ_pred_n ▸ this
-- have : idx ≤ pred_m * n + pred_n := rfl
sorry
mat.arr.get ⟨idx, isLt⟩

[Nikolai Morin]

Thanks. Is there a way to preserve the old variables (like n) when matching?