You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have been tossing ideas around on how to work towards nested structural recursion, and this idea may reach the bar for worth-noting-as-an-RFC.
Summary
The kernel’s approach to compiling nested inductive (e.g. Tree nested under List) is
Create a non-nested mutual inductive, by copying the structure of the inductive that we nest under (List), creating an auxillary inductive (ListTree).
In the types and reduction rules of the generated recursors, replace the type former and constructors of the auxillary inductive with the ones expected by the user.
This way they get their Tree type with the expected types in the constructor and recursors, but they do get an extra recursor Tree.rec_1 (stemming from ListTree.rec), and it’s all disconnected from List.rec.
So I wonder: Can’t we also rewrite ListTree.rec with (a suitable instantiation of) List.rec in the rules for Tree.rec, and hopefully gain extra definitional equalities?
To rewrite the auxillary recursor, define a helper definition with the same type as the auxillary recursor, but implemented using the recursor of the nested-under inductive:
pass the motives corresponding to the desired type through to its recursor
pass through the F-args, but for x_ih parameter that isn't provided by the desired recursor, instantiated that with the that type’s .rec and full set of motives/F-args.
(This paragraph isn’t really helpful, I know, the example below is maybe better, and at some point this needs to be specified precisely).
Example with some code
import Lean.Elab.Command
inductiveTreewhere | node : List Tree → Tree
open Lean Meta
set_option pp.explicit true
set_option pp.funBinderTypes true
-- This the generated rule's RHS.-- The type and constructors of the auxillary `ListTree` have been replaced-- by their `List Tree` counterpats, but we still see `Tree.rec_1`.-- Can we replace that with `List.rec`?/--info: fun (motive_1 : Tree → Sort u) (motive_2 : List Tree → Sort u) (node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a)) (nil : motive_2 (@List.nil Tree)) (cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail)) (a : List Tree) => node a (@Tree.rec_1 motive_1 motive_2 node nil cons a)-/
#guard_msgs(whitespace:=lax) in
run_meta dolet recVal ← getConstInfoRec ``Tree.rec
logInfo recVal.rules[0]!.rhs
-- Here is a definition with the same type as `Tree.rec_1`, but referring to `List.rec` instead.noncomputabledefTree.rec_1_impl
{motive_1 : Tree → Sort u}
{motive_2 : List Tree → Sort u}
(node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a))
(nil : motive_2 (@List.nil Tree))
(cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
(ts : List Tree) :=
@List.rec Tree motive_2 nil (fun (head : Tree) (tail : List Tree) ih_tail => cons head tail (@Tree.rec motive_1 motive_2 node nil cons head) ih_tail) ts
-- With this, I could imagine the following rule RHS'noncomputabledefproposedRuleRHS
(motive_1 : Tree → Sort u)
(motive_2 : List Tree → Sort u)
(node : (a : List Tree) → motive_2 a → motive_1 (Tree.node a))
(nil : motive_2 (@List.nil Tree))
(cons : (head : Tree) → (tail : List Tree) → motive_1 head → motive_2 tail → motive_2 (@List.cons Tree head tail))
(a : List Tree) :=
node a (@Tree.rec_1_impl motive_1 motive_2 node nil cons a)
Is this sound?
Most crucial is of course the question of whether this is sound, a question which I cannot answer easily. (Intuitively it ought to be.)
In the example above the replacement recursor is at least provabily equal:
theoremTree.rec_1_eq_rec1_impl : @Tree.rec_1 = @Tree.rec_1_impl := by
funext motive_1 motive_2 node nil cons ts
induction ts
next => rfl
next t ts ih => simp [ih, Tree.rec_1_impl]
so that is reason for optimism that this will hold for more complicated types.
(Actually, it seems that any parametric definition with the same type as @Tree.rec_1 is going to be equal to it, for a suitable definition of parametric.)
But that theorem like isn’t sufficient, as there are metatheoretic properties to worry about.
Happy to hear expert advise here, either about how to argue that it is, or show why it isn’t.
Ha, with addDeclWithoutChecking I can easily experiment with this, very nice.
At least if the functions are defined via .rec we get the desired definitional equality`
-- Let’s replace `Tree.rec_1` with a term defined via `List.rec`:
run_meta dolet decl ← getConstInfoDefn ``Tree.rec_1_impl
let decl := { decl with name := ``Tree.rec_1}
let env ← getEnv
let .ok env' := env.addDeclWithoutChecking (.defnDecl decl) | throwError "addDeclWithoutChecking failed"
modifyEnv (fun _ => env')
-- A variant of List.map defined directly with the recursornoncomputabledefList.map' (f : α → β) : List α → List β :=
List.rec [] (fun x xs xs_ih => (f x) :: xs_ih)
noncomputabledefTree.id : Tree → Tree :=
Tree.rec (fun ts ts_ih => .node ts_ih) [] (fun _x _xs x_ih xs_ih => x_ih :: xs_ih)
theoremTree.id_eq_1 :
Tree.id (.node ts) = .node (List.map' Tree.id ts) := rfl
With the existing .below/.brecOn construction, this does not work right away:
-- Now using brecOnmutualdefTree.id2 : Tree → Tree
| .node ts => .node (Tree.id2_aux ts)
defTree.id2_aux : List Tree → List Tree
| [] => []
| x::xs => Tree.id2 x :: Tree.id2_aux xs
endtheoremTree.id2_aux_eq : Tree.id2_aux = List.map Tree.id2 := by
funext ts
induction ts
next => rfl
next t ts ts_ih => rw [id2_aux, List.map, ts_ih]
/--error: type mismatch rflhas type id2_aux = id2_aux : Propbut is expected to have type id2_aux = List.map id2 : Prop-/
#guard_msgs intheoremTree.id2_aux_deq : Tree.id2_aux = List.map Tree.id2 := rfl
And it seems to me that while I can express Tree.rec_1 in terms of List.rec, I don't yet see how to similarly express Tree.below_1 in terms of List.below. So maybe we only get nested primitive recusion this way? Or maybe there is a generalization of the course-of-value construction that admits such nested recursion?
I have been tossing ideas around on how to work towards nested structural recursion, and this idea may reach the bar for worth-noting-as-an-RFC.
Summary
The kernel’s approach to compiling nested inductive (e.g.
Tree
nested underList
) isList
), creating an auxillary inductive (ListTree
).This way they get their
Tree
type with the expected types in the constructor and recursors, but they do get an extra recursorTree.rec_1
(stemming fromListTree.rec
), and it’s all disconnected fromList.rec
.So I wonder: Can’t we also rewrite
ListTree.rec
with (a suitable instantiation of)List.rec
in the rules forTree.rec
, and hopefully gain extra definitional equalities?To rewrite the auxillary recursor, define a helper definition with the same type as the auxillary recursor, but implemented using the recursor of the nested-under inductive:
x_ih
parameter that isn't provided by the desired recursor, instantiated that with the that type’s .rec and full set of motives/F-args.(This paragraph isn’t really helpful, I know, the example below is maybe better, and at some point this needs to be specified precisely).
Example with some code
Is this sound?
Most crucial is of course the question of whether this is sound, a question which I cannot answer easily. (Intuitively it ought to be.)
In the example above the replacement recursor is at least provabily equal:
so that is reason for optimism that this will hold for more complicated types.
(Actually, it seems that any parametric definition with the same type as
@Tree.rec_1
is going to be equal to it, for a suitable definition of parametric.)But that theorem like isn’t sufficient, as there are metatheoretic properties to worry about.
Happy to hear expert advise here, either about how to argue that it is, or show why it isn’t.
Does this help?
The hope is that with this we can construct
in a way that this this equation holds definitionally.
I did not work it through yet if that’s actually true, given our course-of-value recursion strategy.
Also the interaction with smart unfolding is unclear. Can there be useful a smart unfolding for a function like this?
The text was updated successfully, but these errors were encountered: