Generalize proof of equality over given FinVec

Stream: new members

[Bernardo Borges]

Hello everyone,
I'm trying to create a proof that all elements of my FinVec of tuples are zeros:

import Mathlib.Data.Fin.Tuple.Reflection

open FinVec

example : ∀ (i : Fin 2), ![(0, 0), (0, 0)] i = (0, 0) := by
  intro i
  -- Maybe something like
  -- cases' i <;> rfl
  match i with
  | 0 => rfl
  | 1 => rfl

As you can see, I just went through every value of this Fin 2 types to finish the proof. As you can see, this wouldn't scale for a Fin 100 vector and so on, and also won't allow me to create a general proof. Any suggestions on how to finish this one? Thanks

[Bjørn Kjos-Hanssen]

You can use fin_cases:

import Mathlib

example : ∀ (i : Fin 2), ![(0, 0), (0, 0)] i = (0, 0) := by
  intro i
  fin_cases i <;> rfl

[Bernardo Borges]

Yes this works, Thanks! I'm just wondering, is this "performance heavy"? As in, it'll take a long time to unify for larger Fin type?

[Bernardo Borges]

# The `fin_cases` tactic.

Given a hypothesis of the form `h : x ∈ (A : List α)`, `x ∈ (A : Finset α)`,
or `x ∈ (A : Multiset α)`,
or a hypothesis of the form `h : A`, where `[Fintype A]` is available,
`fin_cases h` will repeatedly call `cases` to split the goal into
separate cases for each possible value.

Idk, this looked heavy to me

[Bjørn Kjos-Hanssen]

But do you really want to write ![(0, 0), (0, 0),(0, 0), (0, 0),(0, 0), (0, 0),(0, 0), (0, 0), (...a hundred entries...) ]? :smile:

[Edward van de Meent]

Bernardo Borges said:

and also won't allow me to create a general proof

indeed, but for that you first need a function to create these vectors for any given size. as soon as you do that, proving it becomes a lot simpler suddenly, as you get access to induction.

[Bernardo Borges]

What I really mean is that this doesnt work:

import Mathlib.Data.Fin.Tuple.Reflection
import Mathlib.Tactic.FinCases

open FinVec

example : ∀ (i : Fin 2), ![(0, 0), (0, 0)] i = (0, 0) := by
  intro i
  fin_cases i <;> rfl

def zerosVec : (n : ℕ) → Fin n → (ℕ × ℕ)
| 0 => ![]
| (n+1) => Matrix.vecCons (0,0) (zerosVec n)

-- Works fine on constant n
#eval zerosVec 7
example : ∀ (i : Fin 7), (zerosVec 7) i = (0, 0) := by
  intro i
  fin_cases i <;> rfl

-- Doesn't generalize really
example (n : Nat) : ∀ (i : Fin n), (zerosVec n) i = (0, 0) := by
  intro i
  -- fin_cases i <;> rfl
-- tactic 'cases' failed, nested error:
-- dependent elimination failed, failed to solve equation
--   List.pmap Fin.mk (List.range n) ⋯ = i :: as✝
-- at case List.Mem.head
  sorry

[Edward van de Meent]

indeed. however, since you define it inductively, using induction actually becomes a better proof strategy.

[Bernardo Borges]

How can I apply induction on the zerosVec function?

[Eric Wieser]

This works:

import Mathlib.Data.Fin.Tuple.Reflection

open FinVec

def FinVec.const {α} (x : α) : (n : ℕ) → Fin n → α
  | 0 => ![]
  | (n + 1) => Matrix.vecCons x (FinVec.const x n)


def FinVec.const_eq {α} (x : α) : (n : ℕ) → FinVec.const x n = fun i => x
  | 0 => funext fun x => x.elim0
  | (n + 1) => funext <| by
    rw [Fin.forall_fin_succ]
    refine ⟨rfl, fun i => ?_⟩
    rw [const, FinVec.const_eq x n]
    rfl

example : ∀ (i : Fin 2), ![(0, 0), (0, 0)] i = (0, 0) := by
  intro i
  refine congr_fun (FinVec.const_eq _ 2) i

[Edward van de Meent]

you start with induction on n. then use Fin.induction on i.

[Eric Wieser]

(this is the general pattern used in Mathlib.Data.Fin.Tuple.Reflection)

[Edward van de Meent]

my solution:

Code

example (n : Nat) : ∀ (i : Fin n), (zerosVec n) i = (0, 0) := by
  induction n using zerosVec.induct with
  | case1 => simp only [Prod.mk_zero_zero, IsEmpty.forall_iff]
  | case2 n h =>
    intro i
    rw [zerosVec]
    induction i using Fin.induction with
    | zero => simp only [Prod.mk_zero_zero, Matrix.cons_val_zero]
    | succ i =>
      simp only [Prod.mk_zero_zero, Matrix.cons_val_succ]
      exact h i

[Eric Wieser]

Even shorter:

example : ∀ (i : Fin 2), ![(0, 0), (0, 0)] i = (0, 0) := by
  exact congr_fun (FinVec.etaExpand_eq fun i => (0, 0))

[Bernardo Borges]

Very interesting. By using congr_fun did you prove that fun i => (0,0) is equal to the finvec above?

[Eric Wieser]

Well, rather I proved that using FinVec.etaExpand_eq fun i => (0, 0))

[Eric Wieser]

congr_fun just says "since the functions equal, their applications are equal"

[Bernardo Borges]

I've never seen this way to define the FinVec, it will surely be useful as well. i.e.

#eval @FinVec.etaExpand (Nat×Nat) 3 (λ _i => (0,0))

[Bernardo Borges]

The whole point of the proof, to get the forall expression
∀ (i : Fin 2), ![(0, 0), (0, 0)] i = (0, 0) boils down if I just had defined the vector this way

[Eric Wieser]

You should not actually use etaExpand for defining anything

[Eric Wieser]

It exists strictly for assembling proof tricks like the one I give above

[Eric Wieser]

Note that #eval (fun _i : Fin 3 => (0,0)) gives exactly the same output as what you wrote

[Bernardo Borges]

Understood!

Eric Wieser said:

You should not actually use etaExpand for defining anything