Is there a tactic for case analysis on Fin?

Stream: new members

[Mark Fischer]

I have a proof where I repeat this 9 times, once for each possible value of Fin 9 in place of ***_***.

have h₂ : List.all (box_idxs ***_***) (· < 81) := by decide
have h₃ := List.all_eq_true.mp h₂ e h
simp only [decide_eq_true_eq] at h₃
exact h₃

Here it is:

import Mathlib

def size : (x : ℕ) × { y : ℕ // x = y ^ 2 } := ⟨9, 3, by decide⟩

def box_idxs (n : ℕ) : List ℕ :=
  let root := size.snd.val
  let range := List.range root
  let offset := n / root * root * size.fst + (n % root) * root
  let index (r : ℕ) (c : ℕ) := offset + size.fst * r + c
  index <$> range <*> range

example: box_idxs 0 = [0,1,2,9,10,11,18,19,20] := by decide
example: box_idxs 8 = [60,61,62,69,70,71,78,79,80] := by decide

-- I should probably prove that this works for:
-- `n < m → e < (m * m)`
-- but I'm not that far along yet.
theorem capped_box_idxs (n : Fin 9) (e : ℕ): e ∈ box_idxs n → e < 81 :=
  λ h ↦ match h₁ : n with
  | ⟨0, _⟩ => by
    have h₂ : List.all (box_idxs 0) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨1, _⟩ => by
    have h₂ : List.all (box_idxs 1) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨2, _⟩ => by
    have h₂ : List.all (box_idxs 2) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨3, _⟩ => by
    have h₂ : List.all (box_idxs 3) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨4, _⟩ => by
    have h₂ : List.all (box_idxs 4) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨5, _⟩ => by
    have h₂ : List.all (box_idxs 5) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨6, _⟩ => by
    have h₂ : List.all (box_idxs 6) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨7, _⟩ => by
    have h₂ : List.all (box_idxs 7) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  | ⟨8, _⟩ => by
    have h₂ : List.all (box_idxs 8) (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃

def castℕFin (l : List ℕ) (n : ℕ) (h: ∀e ∈ l, e < n) : List (Fin n) :=
  match l with
  | [] => []
  | a :: as => by
    simp only [List.mem_cons, forall_eq_or_imp] at h
    obtain ⟨h₁, h₂⟩ := h
    exact ⟨a, h₁⟩ :: castℕFin as n h₂

I have two questions:

1. I can see that this isn't the best way to prove this. I really should be unfolding box_idxs and proving it that way, that is on my todo list, but does Mathlib support a better way to brute force this?
2. Does Lean "see" that castℕFin has no computational content? Is there a better way to perform this cast?

[Kyle Miller]

Mathlib has the fin_cases tactic

[Kyle Miller]

By the way, the decide tactic is usually not doing anything special when you're proving an equality.

These work:

def size : (x : ℕ) × { y : ℕ // x = y ^ 2 } := ⟨9, 3, rfl⟩
example: box_idxs 0 = [0,1,2,9,10,11,18,19,20] := rfl

[Kyle Miller]

Here's a brute force proof:

theorem capped_box_idxs (n : Fin 9) (e : ℕ) (h : e ∈ box_idxs n) : e < 81 := by
  fin_cases n <;> fin_cases h <;> decide

The fin_cases h is using the fact that e is an element of a List and that it can compute that list using reduction.

[Mark Fischer]

Awesome. Thanks for the help!
Here's the more concise version, I get a surprising linting error on n' for an unused variable.

theorem capped_box_idxs (n : Fin 9) (e : ℕ): e ∈ box_idxs n → e < 81 := by
  intro h
  let n' := n
  fin_cases n <;> {
    have h₂ : List.all (box_idxs n') (· < 81) := by decide
    have h₃ := List.all_eq_true.mp h₂ e h
    simp only [decide_eq_true_eq] at h₃
    exact h₃
  }

[Mark Fischer]

ah, wow. I'll need to study that for a moment

[Mark Fischer]

Oh, that's a very pretty proof and makes sense to me. Cool