WFTactics

Stream: metaprogramming / tactics

[namibj]

I have a recursive definition that normalizes a Option (List α) where α is a tagged enum carrying a Nat.
I sort the list using a lexicographic order (with first by variant, then by value), then if the first variant-many contain the variants terminate out, otherwise prepend the first missing variant with a 0 value before recursing.
In all other cases (detecting a variant twice in a row while iteratively matching for the sequence is all variants; Option.none), I terminate with Option.none.
Clearly this can grow the list at most variant-count-many times before terminating the recursion.

I'd love a tactic (or an extension to WFTactics) that can deal with this "will grow only constant many times before terminating out".
I'll provide the github later (not cleaned up yet, need to check licensing before uploading); it happened during my AoC2023 Day01 Part1 solution.
A band-aid was to slap partial on it, but that's both ugly and will prevent me from using proof-based programming for Part2.

AoC 2023 Day02 solution

The shared problem instance/truth-valued function of part1 and part2 takes the second half of each input line (i.e., a String) plus a triple of Nat's.
For part1, the triple is fixed from the problem spec and you sum an extract (kinda turns out to be just a line number) from the first half of those lines where this function evaluates to true.
For part2, you have to find the smallest triple for which the function with that String input evaluates to true (if no such triple exists, the String is ill-formed/there's a syntax error in the input), multiply the 3 numbers that make up said triple, and sum those products over all input lines.
Topologically the triple behaves like a product order lattice's <= with a hidden derivate of the string on the left and the function argument triple on the right. (Is this discrete topology? Or is essentially nothing about that "topology"?)

I'd have liked to use the elegant way of branching on whether a triple exists for which the function on the current string evaluates to true (bailing out if not), and then just asking for the smallest such triple (lexicographic order should work and is a total order so "smallest" is obviously well-defined, due to the existance of a global minimum (natural numbers!)).

I know that's not really how Lean4 is supposed to be programmed with, but as I understand it, tactics are very much fair game for deriving a modified implementation that solves a related but different task, like automatic differentiation or here, using a region membership indicator function as input to derive a minimum/extremum search function.

In a way I think of this approach as a sort of "semantic macro" that relates the desired function's behavior to an input function's behavior. Critically, without necessarily providing an implementation of the desired function.

Should be very powerful when talking about abstract implementations, and attempting to reason about the correctness of any particular concrete implementation.

Like, for example here, the concrete implementation of doing exponential search on first all members of the triple together, then binary search on the members individually. I'd love having Lean4 tell me that this would indeed deliver the smallest such triple.

Oh, and yes, of course, I'm aware that AoC is just an exercise.
But last year it has shown itself to be a good exercise for me learning applied Futhark on AoC 2022. E.g., I managed to write an implementation for AoC 2022 Day5: crate stacker that processes the lines in parallel. Not because that's a good approach here, but because a language targeting GPUs and GPU-like processors is to be used for parallel implementations, so I ought to learn how to write parallel code even when it's not easy to.