help dealing with cast on fin

Stream: general

[Frederick Pu]

Does anyone have any tips on how to prove a goal liek this?

vars : VarMap
name : Name
he✝ : (inferType vars (var name)).isSome = true
ctx : DVector (Array.map (fun x => x.snd.type) vars).toList
x : Fin (Array.size vars)
h : Array.findLastFinIdx? (fun x => x.fst == name) vars = some x
he : (Array.findLast? (fun x => decide (x.fst = name)) vars).isSome = true
this : x = (some x).get ⋯
⊢ ↑(cast ?m.88
      (⟨Array.size vars - 1, ⋯⟩ - (cast ⋯ (Array.findFinIdx? (fun x => x.fst == name) (Array.reverse vars))).get ⋯)) =
  Array.size vars - 1 - ↑((Array.findFinIdx? (fun x => decide (x.fst = name)) (Array.reverse vars)).get ⋯)

like i feel like we should be able to just strip away the cast and push the .val inside of the cast

[Ruben Van de Velde]

Not really, no. You might have more luck with a #mwe, but even then, maybe not much more. It looks suspicious that you have a metavariable ?m.88 in your cast, though

[Aaron Liu]

It should be possible to strip away the cast if it isn't an "evil" cast

[Aaron Liu]

how did you even end up with these casts in your goal?

[Edward van de Meent]

if instead of docs#cast you use docs#Fin.cast, i imagine that things will go a lot smoother...

[Edward van de Meent]

also, can i interest you in docs#Fin.last ?

[Aaron Liu]

can we have Fin.last take a [NeZero n] instead of returning a Fin (n + 1)

[Violeta Hernández]

Edward van de Meent said:

if instead of docs#cast you use docs#Fin.cast, i imagine that things will go a lot smoother...

I wonder if docs#Fin.cast_eq_cast should be reversed and made simp?

[Edward van de Meent]

I feel like that wouldn't trigger? I'm not sure though. Also, there is the usability issue of it being unable to simp when the rewrite already is with something like congr(Fin $h) : Fin n = Fin m. Strictly speaking that's not a reason against the simp lemma, but it does seem to me like it would make bad (beginner) UX?

[Aaron Liu]

well the special case of Fin is nice because it's injective

[Frederick Pu]

I switched to using Fin.cast and now the metavariable is gone:

vars : VarMap
name : Name
he✝ : (inferType vars (var name)).isSome = true
ctx : DVector (Array.map (fun x => x.snd.type) vars).toList
x : Fin (Array.size vars)
h : Array.findLastFinIdx? (fun x => x.fst == name) vars = some x
he : (Array.findLast? (fun x => decide (x.fst = name)) vars).isSome = true
this : x = (some x).get ⋯
⊢ ↑(⟨Array.size vars - 1, ⋯⟩ - Fin.cast ⋯ ((Array.findFinIdx? (fun x => x.fst == name) (Array.reverse vars)).get ⋯)) =
  Array.size vars - 1 - ↑((Array.findFinIdx? (fun x => decide (x.fst = name)) (Array.reverse vars)).get ⋯)

[Aaron Liu]

maybe it's just hidden

[Frederick Pu]

it's weird that it's hidden for Fin.cast and not cast

[Frederick Pu]

is there a sense in which cast is less proof irrelevant?

[Aaron Liu]

I mean the pretty printer may have hidden it behind the ⋯

[Frederick Pu]

yeah i just dont understand why the pretty printer doesnt do that for cast also?

[Frederick Pu]

also i think this might be a bug with grind

[Frederick Pu]

def Array.findLastFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) := Option.map (fun res => ⟨as.size - 1, by {
    have := res.isLt
    grind
}⟩ - Fin.cast (size_reverse) res) (as.reverse.findFinIdx? p)

[Frederick Pu]

but when i do

def Array.findLastFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) := Option.map (fun res => ⟨as.size - 1, by {
    grind [res.isLt]
}⟩ - Fin.cast (size_reverse) res) (as.reverse.findFinIdx? p)

i get:

redundant parameter `res.isLt`, `grind` uses local hypotheses automaticallyLean 4

[Frederick Pu]

but then this:

def Array.findLastFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) := Option.map (fun res => ⟨as.size - 1, by {
    grind
}⟩ - Fin.cast (size_reverse) res) (as.reverse.findFinIdx? p)

gives:

`grind` failed
case grind.2
α : Type u
p : α → Bool
as : Array α
res : Fin as.reverse.size
h : as.size ≤ as.size - 1
h_1 : ¬-1 * ↑as.size + 1 ≤ 0
⊢ False
(trace)Lean 4

[Frederick Pu]

also here's a version of Fin.last that uses NeZero instead:

def Fin.last' {n : Nat} [NeZero n] : Fin n :=
    match h :  n with
    | (k + 1) => Fin.last k
    | 0 => by {
        apply False.elim
        expose_names
        rw [h] at inst
        simp at inst
    }

def Fin.val_last'_eq {n : Nat} [NeZero n] : (Fin.last' (n := n)).val = n - 1 := sorry

def Fin.le_last' {n : Nat} [NeZero n] : ∀ i : Fin n, i ≤ (Fin.last' (n := n)) := sorry

def Array.findLast? {α : Type u} (p : α → Bool) (as : Array α) : Option α := as.reverse.find? p

[Frederick Pu]

btw I was able to close the sorry thanks everyone for your help