Inductive definition on (Fin n)?

Stream: new members

[Ching-Tsun Chou]

Is it possible to make an inductive definition on Fin n (more precisely, Fin (n + 1) where n : ℕ) in a manner similar to an inductive definition on ℕ? I tried something like the following:

def MakeFinRun (M : DetAutomata A) (n : ℕ) (as : Fin n → A) : Fin (n + 1) → M.State
  | 0 => M.get_init
  | k + 1 => M.get_next (MakeinRun M n as k) (as k)

and got the following error message on the k + 1 case which I don't understand:

invalid patterns, k is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
⟨.(match ↑k + 1 % (n + 1), n + 1 with
| 0, x => 0
| n@h:n_1.succ, m => if m ≤ n then n.modCore m else n),
⋯⟩

Is there a way to make the above work?

[Matt Diamond]

if structural recursion doesn't work, maybe docs#Fin.induction will?

[Ching-Tsun Chou]

How do I use an induction theorem to make an inductive definition? Is there an example I can look at?

[Ching-Tsun Chou]

Fortunately, well-founded recursion works here:

def MakeFinRun (M : DetAutomata A) (n : ℕ) (as : Fin n → A) (k : Fin (n + 1)) : M.State :=
  if h : k > 0 then
    have h1 : k - 1 < k := by exact Fin.sub_one_lt_iff.mpr h
    have h2 : k - 1 ≠ Fin.last n := by exact Fin.ne_last_of_lt h1
    M.get_next (MakeFinRun M n as (k - 1)) (as (Fin.castPred (k - 1) h2))
  else M.get_init

[Edward van de Meent]

you can also do this:

def MakeFinRun (M : DetAutomata A) (n : ℕ) (as : Fin n → A) : Fin (n + 1) → M.State
  | 0 => M.get_init
  | ⟨k + 1,_⟩ => M.get_next (MakeFinRun M n as ⟨k,by omega⟩) (as ⟨k,by omega⟩)

[Edward van de Meent]

the thing is: Fin is an inductive type, just maybe not in the way you might have expected

[Edward van de Meent]

so you just need to know how to properly match on it

[Ching-Tsun Chou]

@Edward van de Meent Thanks a lot! Do you know where I can look up such information? Or you just have to know it?

[Edward van de Meent]

If you look at the definition of Fin, you'll see it's a subtype, which always can be destructed in this way

[Ching-Tsun Chou]

I see. Thanks! In a proof, how do I unfold such a definition? For an recursive definition on ℕ, simp usually works. But simp seems unable to reduce the implicit match in the MakeFinRun. Are there additional theorems I need to give to simp, or I need to use some special tactics?

[Ching-Tsun Chou]

For example, how do I prove the following?

def foo (n : ℕ) : Fin (n + 1) → ℕ
  | 0 => 13
  | ⟨k + 1, _⟩ => 42 + k

example (n : ℕ) : foo 0 = 13 := by sorry

example (n : ℕ) : foo 7 = 48 := by sorry

[Robin Arnez]

This example doesn't work? foo takes 2 parameters and you only provided one?
If you do specify both parameters though, rfl will do it:

notation "ℕ" => Nat

def foo (n : ℕ) : Fin (n + 1) → ℕ
  | 0 => 13
  | ⟨k + 1, _⟩ => 42 + k

example (_ : ℕ) : foo 10 0 = 13 := by rfl
example (_ : ℕ) : foo 10 7 = 48 := by rfl

[Robin Arnez]

As an alternative, simp [foo] also works

[Ching-Tsun Chou]

Sorry, my mistake. The type of goals I want to prove are:

example (n : ℕ) : foo n 0 = 13 := by rfl

example (n : ℕ) (h : n > 7) : foo n 7 = 48 := by sorry

I found that simp does not work in the first example. In the second example, the assumption h has to play a role somehow.

[Robin Arnez]

If you make your definition a bit simpler then this works:

import Mathlib.Data.Fin.Basic

def foo (n : ℕ) (x : Fin (n + 1)) : ℕ :=
  match x.val with
  | 0 => 13
  | k + 1 => 42 + k

example (_ : ℕ) : foo 10 0 = 13 := by simp [foo]

example (_ : ℕ) : foo 10 7 = 48 := by simp [foo]

example (n : ℕ) : foo n 0 = 13 := by simp [foo]

example (n : ℕ) (h : 7 ≤ n) : foo n 7 = 48 := by
  simp [foo, Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt (Nat.lt_add_one_of_le h)]

[Ching-Tsun Chou]

That's a neat idea. But, unfortunately, my real use case involves a recursive definition (see the earlier part of this thread). So I would need to produce something of type Fin (n + 1) to feed into the recursive call.

[Aaron Liu]

You can use something like docs#Fin.succRec

[Aaron Liu]

or docs#Fin.induction

[Aaron Liu]

You can also make an auxiliary definition that takes the proof of x < n + 1 unbundled

[Ching-Tsun Chou]

is there an example of how to use such induction principles to make recursive definitions?

[Ching-Tsun Chou]

I just realized that instead of struggling with a recursive definition on Fin (n+1) and the associated proofs, I can just recurse on ℕ and then chop off the tail that I don't need. Perhaps the following definitions will be easier to work with. Time will tell.

def MakeInfRun (M : DetAutomata A) (as : ℕ → A) : ℕ → M.State
  | 0 => M.get_init
  | k + 1 => M.get_next (MakeInfRun M as k) (as k)

def MakeFinRun (M : DetAutomata A) (n : ℕ) (as : Fin n → A) : Fin (n + 1) → M.State :=
  match n with
  | 0 => fun _ ↦ M.get_init
  | _ + 1 =>
    let as' := fun k : ℕ ↦ if k < n + 1 then as k else as 0
    fun k ↦ MakeInfRun M as' k.toNat

[Ching-Tsun Chou]

After more trials and errors, I found that the definition using well-founded recursion given below is the easier to work with.

def MakeFinRun (M : DetAutomata A) (n : ℕ) (as : Fin n → A) (k : Fin (n + 1)) : M.State :=
  if h : k > 0 then
    have h1 : k - 1 < k := by exact Fin.sub_one_lt_iff.mpr h
    have h2 : k - 1 ≠ Fin.last n := by exact Fin.ne_last_of_lt h1
    M.get_next (MakeFinRun M n as (k - 1)) (as (Fin.castPred (k - 1) h2))
  else M.get_init

[Shreyas Srinivas]

docs#Fin2 is already inductive

[Ching-Tsun Chou]

Thanks for pointing this out. I did not know Fin2. Unfortunately, I already have a lot of definitions and proofs that use Fin. It is a bit too late to switch to Fin2 at this point.

[Aaron Liu]

Use docs#Fin.cases

[Aaron Liu]

I don't know if this works because you don't have a #mwe but

def MakeFinRun (M : DetAutomata A) (n : ℕ) (as : Fin n → A) (k : Fin (n + 1)) : M.State :=
  k.cases M.get_init fun k =>
    M.get_next (MakeFinRun M n as k.castSucc) (as k)

[Matt Diamond]

if termination-checking fails, there's docs#Fin.induction (as I suggested earlier... sorry that I didn't have the time to provide an example then):

def MakeFinRun (M : DetAutomata A) (n : ℕ) (as : Fin n → A) (k : Fin (n + 1)) : M.State :=
  k.induction M.get_init fun j IH => M.get_next IH (as j)