Recursive definitions against ℕ+ (pnat)

Stream: general

[Eric Wieser]

I'm trying to write an recursive definition against a ℕ+, but am having a really hard time. Ideally I'd match against 1 and n + 1, but that doesn't seem to work. My follow up attempt is as follows, but this fails at proof of well-founded-ness

def Kₙ (α : Type) : ℕ+ → Type
| ⟨0, _⟩ := by linarith
| ⟨1, _⟩ := α
| ⟨n + 2, _⟩ := α × Kₙ ⟨n + 1, by linarith⟩

Am I missing an obvious trick here?

[Eric Wieser]

(again, I realize this definition is contrived, but matching against pnat and fin n is something I'd like to know how best to do)

[Eric Wieser]

This works, but feels clumsy:

def Kₙ_aux : Π (n: ℕ), n > 0 → Type
| 0 _ := by linarith
| 1 _ := α
| (n + 2) _ := α × Kₙ_aux (n+1) (by linarith)
def Kₙ (n : ℕ+) := Kₙ_aux α n.val n.property

[Gabriel Ebner]

I'd go for

def Kₙ : ℕ → Type
| 0 := unit
| 1 := α
| (n+1) := α × Kₙ n

[Eric Wieser]

Ah, but then I can't use the builtin add_comm_group (prod x y) instance

[Eric Wieser]

Because there is no add_comm_group unit

[Gabriel Ebner]

We have punit instances. The trivial group should definitely be punit.

[Gabriel Ebner]

Even if it didn't work, you could define a add_comm_group (Kₙ (n+1)) instance.

[Eric Wieser]

Am I missing an import to find those punit instances?

[Eric Wieser]

Yep! algebra.punit_instances

[Eric Wieser]

It would be great if lean had a mechanism to suggest imports

[Kevin Buzzard]

Instead of using the equation compiler you can just write your own recursor as a function and then apply that.

[Eric Wieser]

My goal here is to produce something as readable as possible for someone who doesn't really know lean, and the pattern matcher seems clearer to me than writing my own recursor

[Utensil Song]

@Eric Wieser 's #mwe

import algebra.field
import algebra.module.prod
import algebra.punit_instances
import data.vector
import tactic

variables (α : Type) [field α]

-- vectors
def Kₙ : ℕ → Type
| 0 := unit
| (n + 1) := α × Kₙ n

-- addition and scalar multiplication
instance : Π (n : ℕ), add_comm_group (Kₙ α n)
| 0 := by {dunfold Kₙ, apply_instance}
| (n + 1) := by {dunfold Kₙ, haveI := Kₙ.add_comm_group n, apply_instance}

instance : Π n, module α (Kₙ α n)
| 0 := by {dunfold Kₙ, apply_instance}
| (n + 1) := by {dunfold Kₙ, haveI := Kₙ.module n, apply_instance}

[Utensil Song]

Should the following work? But it doesn't yet.

@[derive [add_comm_group, module α]]
def Kₙ : ℕ → Type
| 0 := unit
| (n + 1) := α × Kₙ n

[Utensil Song]

Feels like a pattern, could be a new derive_handler PR?