reducing inductive result types

Stream: lean4

[Daniel Selsam]

Leo and I recently revisited some of the forwardport/backport decisions that we had postponed when first working on binport. We decided that we will not support https://github.com/dselsam/binport/issues/3 in Lean4. Could somebody please backport this change? (Not removing the feature from the kernel, just changing the very small number of inductive types that currently use the feature)

[Mario Carneiro]

We could also support this in the porting tool

[Daniel Selsam]

It is barely used. It seems much easier to backport.

[Scott Morrison]

Is there an easy way to produce a list of the places in mathlib this currently occurs?

[Mario Carneiro]

import all

meta def bad : expr → bool
| (expr.sort _) := ff
| (expr.pi _ _ _ ty) := bad ty
| _ := tt
open tactic
#eval do
  env ← get_env,
  trace $ list.map declaration.to_name $
    env.filter $ λ d, env.is_inductive d.to_name && bad d.type

-- [category_theory.presieve.singleton,
--  category_theory.presieve.pullback_arrows,
--  has_finite_inter.finite_inter_closure,
--  zorn.chain_closure,
--  ε_NFA.ε_closure,
--  category_theory.presieve.of_arrows,
--  generate_pi_system]

[Daniel Selsam]

There are some others where the issue is in constructor arguments, e.g. the thunk lazy_list in

inductive lazy_list (α : Type u) : Type u
| nil : lazy_list
| cons (hd : α) (tl : thunk lazy_list) : lazy_list

[Mario Carneiro]

Oh that one's actually a problem, we can't change that without breaking lazy_list because thunk is magic

[Mario Carneiro]

but surely lean should be able to handle this, it's a nested inductive

[Daniel Selsam]

thunk is just a def in lean3, but a structure in lean4 -- for this example, it would be sufficient for binport if we just make thunk a structure in lean3 instead of changing this type (so we can auto-align thunk -> Thunk)

[Mario Carneiro]

Well, I want to press more on the issue with defs in constructors, because that seems like it might be a problem in lean 4. It seems weird to me that this would work:

def X (A : Type) := Nat -> A
def Y (A : Type) := Sum A Unit

inductive Foo
| a : X Foo -> Foo
| b : Y Foo -> Foo

But this would not:

def X (A : Type) := Nat -> A
def Y (A : Type) := Sum A Unit

inductive Foo
| a : X Foo -> Foo

[Mario Carneiro]

Ah, no after some testing the line is a bit different; defs like X just can't be used at all in nested inductives

[Daniel Selsam]

Currently, (most of) the type traversals inside the inductive-type module (and all built-in constructions) do not whnf before descending into the body. So, many of the checks (e.g. ok-nesting/positivity) are effectively syntactic.