Defining an inductive type using Vector

Stream: lean4

[Geoffrey Irving]

I'd like to define the second one of these inductive types, but I'm blocked by the listed error. Is there an easy way to work around the error?

import Mathlib

-- This one works, but the function it takes doesn't know the lists have the same size
inductive GoodTower : Type where
  /-- Run a subcomputation, then sample an answer based on the results -/
  | sub : List GoodTower → (List Bool → Bool) → GoodTower

-- This one doesn't work, because
--   (kernel) invalid nested inductive datatype 'Vector', nested inductive datatypes
--   parameters cannot contain local variables.
inductive BadTower : Type where
  /-- Run a subcomputation, then sample an answer based on the results -/
  | sub : {n : ℕ} → Vector BadTower n → (Vector Bool n → Bool) → BadTower

[Geoffrey Irving]

Aha, this works and is cleaner anyways:

/-- Recursive computations that can run subcomputations -/
inductive Tower : Type where
  /-- Run some subcomputations, then produce an answer based on the results -/
  | subs : {n : ℕ} → (Fin n → Tower) → ((Fin n → Bool) → Bool) → Tower

[Notification Bot]

Geoffrey Irving has marked this topic as resolved.

[Kim Morrison]

One could also redesign Mathlib's List.Vector so that it isn't just a wrapper around List, but itself an inductive type. List.Vector is rarely used in Mathlib, so it would feasible, but possibly un-rewarding, to do this.

[Kyle Miller]

I was wondering if the problem had anything to do with the argument order to Eq, and it seems like I just ran into a bug:

inductive BadTower : Type where
  | sub {n : ℕ} (v : List BadTower) (h : n = v.length) : BadTower
/-
application type mismatch
  List.length v
argument has type
  _nested.List_1
but function has type
  List BadTower → ℕ
-/

[Kyle Miller]

(The other argument order gives "invalid nested inductive datatype 'Eq', nested inductive datatypes parameters cannot contain local variables.")

[Kyle Miller]

Hate to suggest touching the kernel, but I wonder if there's some property of Eq that could be taken advantage of when eliminating nested inductives? Could the original BadTower Just Work?

[Notification Bot]

Geoffrey Irving has marked this topic as unresolved.

[Arthur Adjedj]

Kyle Miller said:

Hate to suggest touching the kernel, but I wonder if there's some property of Eq that could be taken advantage of when eliminating nested inductives? Could the original BadTower Just Work?

The issue doesn't have to do with equality, but instead with the fact that you're trying to rely on a function over Lists that uses the nested appearance. Since the kernel does not also translate the function List.length into a new/temporary _nested.List_1.length, it instead produces a type error. The following code triggers the same error without the use of equality:

inductive Foo (A : Type)

def Foo.bar : Foo A → Type := fun _ => Nat

inductive BadTower : Type where
  | sub {n : ℕ} (v : Foo BadTower) : Foo.bar v →  BadTower

[Arthur Adjedj]

As for the original error presented by @Geoffrey Irving , it is twofolds:

• First, the kernel currently does not currently manage nested indexed inductives types, and nested inductives types for which nested appearances may contain variables that are not parameters. I should get around to polishing a RFC for this at some point...
• Even if the kernel did manage such types, it would still encounter the issue of functions relying on nested appearances being present in some constructor (as pointed out by Kyle). Indeed, the translation of nested appearances into auxiliary inductive types would lead to the appearance of List.length in a field of the translation of Vector.

[Eric Wieser]

Kim Morrison said:

One could also redesign Mathlib's List.Vector so that it isn't just a wrapper around List, but itself an inductive type. List.Vector is rarely used in Mathlib, so it would feasible, but possibly un-rewarding, to do this.

Does docs#Vector3 work?

[Eric Wieser]

Only for rather unusual interpretations of "works":

-- use `#guard_msgs` to silence an internal error we don't care about
/--
error: application type mismatch
  BadTower.rec fun {n} a a_1 a_ih => ((a_2 : Fin2 n) → motive (a a_2)) ×' ((a : Fin2 n) → a_ih a)
argument has type
  {n : ℕ} → Vector3 BadTower n → (Vector3 Bool n → Bool) → (Fin2 n → Sort (max 1 u)) → Sort (max (max 1 (imax 1 u)) 1 u)
but function has type
  ({n : ℕ} →
      (a : Vector3 BadTower n) →
        (a_1 : Vector3 Bool n → Bool) →
          ((a_2 : Fin2 n) → (fun t => Sort (max 1 u)) (a a_2)) → (fun t => Sort (max 1 u)) (BadTower.sub a a_1)) →
    (t : BadTower) → (fun t => Sort (max 1 u)) t
-/
#guard_msgs in
inductive BadTower : Type where
  /-- Run a subcomputation, then sample an answer based on the results -/
  | sub : {n : ℕ} → Vector3 BadTower n → (Vector3 Bool n → Bool) → BadTower

[Arthur Adjedj]

The good news is, this is not a kernel error, and the inductive type, as well as its recursor/constructors are available in the environment after the error. At first glance, it looks like Lean fails to generate the auxiliary definition BadTower.below, used to do course-by-value recursion. This is worth reporting in an issue.

[Arthur Adjedj]

MWE:

def Foo (α : Type) := Unit → α

inductive Bar : Type where
  | sub : Foo Bar → Bar

[Arthur Adjedj]

In the MWE, the problem seems to be that Lean cannot unify (max (max 1 (imax 1 u)) 1 u) and max 1 u. The core problem here is that Lean does not know that imax 1 u can reduce to u. The normalisation procedure for universes already normalises imax 0 u to u, perhaps adding another special-case for imax 1 u could be worth it ?

[Eric Wieser]

Since you've made the MWE, mind filing the issue?

[Arthur Adjedj]

lean4#7096