induction on fin n

Stream: maths

[Jeffrey Li]

Hi, I'm wondering how to perform induction on fin n? I want to rewrite the following code:

open nat

variables {A : Type*} {ops : ℕ  → A → A}
def chain : ℕ → Op A
| zero := ops 0
| (x+1) := ops (x+1) ∘ chain x

to be able to work with fin n as follows:

variables {B : Type*} {opsFin : (fin n)  → B → B}
def chainFin(finZero : has_zero (fin n)): (fin n) → Op B
| finZero := opsFin finZero
| (x+1) := opsFin (x+1) ∘ chainFin x

However currently I am getting the error cannot synthesize placeholder (x).

[Yaël Dillies]

That's because fin n is not an inductive type, but a subtype. What are you trying to do eventually?

[Jeffrey Li]

I'm just trying to define the inductive chain function that takes fin n as an argument

[Yaël Dillies]

Also you're feeding in the statement that fin n has a zero, rather than the zero itself.

[Yaël Dillies]

What's the inductive chain function? I can think of many chain concepts.

[Jeffrey Li]

So i have a series of n differential operators on A, so for example D_1, D_2, ..., and the ith chain should be D_1 D_2 ... D_i

[Yaël Dillies]

Have you considered the option of defining them as junk value when greater than n? This might make your life easier.

[Jeffrey Li]

Haha yeah, but I also need to do alot of induction with n in my project later anyways so I thought I might as well figure out how to do it at the start

[Yaël Dillies]

Even more so then!

[Jeffrey Li]

Is there no good way to do induction on fin n?

[Yaël Dillies]

Not really, fin n is an annoying little guy

[Yaël Dillies]

By that I mean that instead of having D : fin n → B → B, you have D : ℕ → B → B and you just don't care about what D k is for n ≤ k.

[Jeffrey Li]

Oh I see, thanks for your help then, I'll just do my best to work around it

[Yaël Dillies]

If ever you need some extensionality property, like "My sequences of differential operators D and E agree if D 0 = E 0, ..., D n = E n, then you might want to force the junk value to be id or something. If you do not constrain it, you can have two sequences that are the same everywhere you care about, but don't have the same junk values. I have no idea whether it's a problem in your case.

[Yakov Pechersky]

I think Anne made the equation compiler work on fin n but I can't find the commit.

[Eric Wieser]

You have to match on ⟨0, _⟩ and ⟨n+1, h⟩ I think

[Kyle Miller]

@Jeffrey Li Is this roughly what you're looking for?

import data.fin.tuple.basic
import tactic

open nat

variables {A : Type*} {ops : ℕ → (A → A)}

def chainFin : Π {n : ℕ} (ops : fin n → (A → A)), (A → A)
| 0 ops := id
| (n+1) ops := chainFin (fin.init ops) ∘ ops ⟨n, lt_add_one n⟩

[Kyle Miller]

I wasn't sure what Op was so I had (A → A) stand in for it.

[Kyle Miller]

Just to show its properties:

lemma chainFin_one (ops : fin 1 → (A → A)) :
  chainFin ops = ops 0 := rfl

lemma chainFin_two (ops : fin 2 → (A → A)) :
  chainFin ops = ops 0 ∘ ops 1 := rfl

lemma chainFin_three (ops : fin 3 → (A → A)) :
  chainFin ops = ops 0 ∘ ops 1 ∘ ops 2 := rfl