No more (kernel) support for reducing inductive result types

[dselsam]

The following is not currently supported in Lean4:

inductive finite_inter_closure : set (set α)
| basic {s} : s ∈ S → finite_inter_closure s
| univ : finite_inter_closure set.univ
| inter {s t} : finite_inter_closure s → finite_inter_closure t → finite_inter_closure (s ∩ t)

The outer set in the result type needs to be unfolded to expose an additional parameter. The change necessary to run mathport is implemented in this commit on my mathport branch: https://github.com/dselsam/lean4/commit/1bef1cb3498cf81f93095bda16ed8bc65af42535. This patch is sufficient for mathport but not for using this feature directly in Lean4, since many other places in the elaboration pipeline also do not whnf, e.g. constructions such as mk_no_confusion.

[leodemoura]

The plan is to unfold inductive declarations in the elaborator before we send them to the kernel. I think it is cleaner.
Moreover, the patch is too hackish to merge. For example, we have nested inductive types in the Lean 4 kernel, and it doesn't handle them.

I think it is easier to refactor and write finite_inter_closure as

inductive finite_inter_closure : set α -> Prop
| basic {s} : s ∈ S → finite_inter_closure s
| univ : finite_inter_closure set.univ
| inter {s t} : finite_inter_closure s → finite_inter_closure t → finite_inter_closure (s ∩ t)

[leodemoura]

Here is an example where the patch fails:

def PList (α : Type u) := List (α × α)

inductive Foo1 (α : Type u) where
  | mk (x : PList (Foo1 α))

I don't want to keep patching the kernel to support these variants. I think it is much cleaner to handle these different cases in the elaborator.