Zulip Chat Archive

Stream: general

Topic: Recursive definitions against ℕ+ (pnat)


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jul 31 2020 at 09:20):

I'd go for

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

view this post on Zulip Eric Wieser (Jul 31 2020 at 09:20):

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

view this post on Zulip Eric Wieser (Jul 31 2020 at 09:21):

Because there is no add_comm_group unit

view this post on Zulip Gabriel Ebner (Jul 31 2020 at 09:23):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jul 31 2020 at 09:24):

Am I missing an import to find those punit instances?

view this post on Zulip Eric Wieser (Jul 31 2020 at 09:25):

Yep! algebra.punit_instances

view this post on Zulip Eric Wieser (Jul 31 2020 at 09:25):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

-- 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}

view this post on Zulip 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

view this post on Zulip 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