## Stream: general

### Topic: Recursive definitions against ℕ+ (pnat)

#### Eric Wieser (Jul 31 2020 at 09:10):

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 (Jul 31 2020 at 09:11):

(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 (Jul 31 2020 at 09:16):

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 (Jul 31 2020 at 09:20):

I'd go for

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


#### Eric Wieser (Jul 31 2020 at 09:20):

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

#### Eric Wieser (Jul 31 2020 at 09:21):

Because there is no add_comm_group unit

#### Gabriel Ebner (Jul 31 2020 at 09:23):

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

#### Gabriel Ebner (Jul 31 2020 at 09:23):

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

#### Eric Wieser (Jul 31 2020 at 09:24):

Am I missing an import to find those punit instances?

#### Eric Wieser (Jul 31 2020 at 09:25):

Yep! algebra.punit_instances

#### Eric Wieser (Jul 31 2020 at 09:25):

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

#### Kevin Buzzard (Jul 31 2020 at 10:00):

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

#### Eric Wieser (Jul 31 2020 at 10:10):

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 (Jul 31 2020 at 10:49):

@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

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 (Jul 31 2020 at 10:49):

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 (Jul 31 2020 at 10:51):

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

Last updated: May 14 2021 at 12:18 UTC