# Zulip Chat Archive

## Stream: general

### Topic: Autogenerating recursive calls

#### Wojciech Nawrocki (Jan 10 2020 at 01:24):

Hello! Something I would really like for working with types that have many constructors is some kind of code generator for structural recursion in which I only want to touch some subsets of the constructors. For example, consider a simple type of formulas:

inductive formula | var: string → formula | plus: formula → formula → formula | mult: formula → formula → formula

for which I need to write a rename-variables function that changes all 'x's to 'y's:

def rename (x: string) (y: string): formula → formula | (var nm) := if nm = x then (var y) else (var nm) | (plus f₁ f₂) := plus (rename f₁) (rename f₂) | (mult f₁ f₂) := mult (rename f₁) (rename f₂)

Most of this function is trivial and simply calls itself recursively on occurrences of the same type within constructors. Writing such functions is boring and most of the code is boilerplate. Instead, I would like a way to simply say:

@[recurse] def rename (x: string) (y: string): formula → formula | (var nm) := if nm = x then (var y) else (var x)

or something similarly short and have Lean autogenerate the rest. Does anyone know if something like or close to it is possible? Has it been done in another language?

(This seems like the kind of thing some variation on lenses could work for but I'm not quite sure.)

#### Simon Hudon (Jan 10 2020 at 01:34):

I think I would break down the problem into generating a `replace`

function which looks like:

def replace (f: formula → option formula): formula → formula | x := match f x with | some y := y | none := match x with | var v := var v | plus x y := plus (replace x) (replace y) | mult x y := mult (replace x) (replace y) end end

(not sure if that compiles) and then define your recursive function (by hand or automatically) as:

def rename (x: string) (y: string) : formula → option formula | (var nm) := some $ if nm = x then (var y) else (var x) | _ := none def rename' (x: string) (y: string) : formula → formula := replace (rename x y)

#### Simon Hudon (Jan 10 2020 at 01:35):

The code for `replace`

can be generated using the `induction`

tactic.

#### Tim Daly (Jan 10 2020 at 04:50):

Actually, no. All the hash function is doing is checking that the proof object is unchanged. Lean could concatenate a version number to the proof it gives to Axiom (for the GCD, for example). When Axiom returns the GCD computation, Lean has to decide to trust the result. So Axiom provides the proof that Lean initially provided for GCD (which Axiom stored a long time ago) and the hash code. Lean can then concatenate the version number of the proof checker to the proof source code, compute the hash and compare it to the prior hash. If either the version number is wrong or the proof text has changed then the hash won't match.

A hash mismatch due to a version number change on Lean's proof checker means that Lean needs to fully check the provided proof. If the version number hasn't changed then the proof text must have changed and Lean needs to fully check the provided proof. But if the hash matches then nothing has changed and there is evidence that the GCD proof previously passed Lean's proof checker so it doesn't need to be re-checked, saving a lot of work.

The hash has nothing to do with the actual method of proof.

The problem to solve is to scale proof checking and trusted computation to larger computations. A Groebner basis can have many steps using other algorithms and each proof of each sub-algorithm needs to be provided to Lean to be checked. A hash checker would make this a very low cost but very trustable operation.

#### Tim Daly (Jan 10 2020 at 05:00):

The cryptographic idea that directly applies is called HMAC.key-hashed message authentication codes.

#### Wojciech Nawrocki (Jan 10 2020 at 11:30):

Thanks Simon! `replace`

doesn't compile but a version where the structural recursion is top-level does:

def replace₂ (f: formula → option formula): formula → formula | z@(var v) := match f z with | some y := y | none := z end | z@(plus x y) := match f z with | some y := y | none := plus (replace₂ x) (replace₂ y) end | z@(mult x y) := match f z with | some y := y | none := mult (replace₂ x) (replace₂ y) end

It works for the simple case, however I should have been more specific in that I also want to consider functions which may include arbitrary processing of recursive results, e.g.

@[recurse] def rename (x: string) (y: string): formula → formula | (var nm) := if nm = x then (var y) else (var nm) | (plus f₁ f₂) := mult (rename f₁) (rename f₂)

which I'm not sure generalize into a single higher-order function since then one cannot call `replace`

from `rename`

. This is the reason why I asked about code generation. I guess that's what tactics do and `induction`

is a good shout for going some way towards shorter definitions.

#### Simon Hudon (Jan 10 2020 at 12:55):

Let's try this again, then.

def rewrite (f: formula → formula): formula → formula | e@(var _) := f e | (plus e e') := f (plus (rewrite e) (rewrite e')) | (mult e e') := f (mult (rewrite e) (rewrite e'))

Then you should be able to write `rename`

so that, together with `rewrite`

it will form `rename_all`

. What do you think?

#### Chris B (Jan 10 2020 at 13:01):

I think this is also one of the big selling points of recursion schemes (ala Haskell) if you're interested, but I haven't actually studied them enough to know if you could implement them in Lean. @Simon Hudon Do you know if anything like Haskell's `Fix`

can be done with Lean?

#### Simon Hudon (Jan 10 2020 at 13:14):

I also love recursion schemes. `Fix`

is hard to encode directly but there are ways to get close. The simplest approach would be to define it as:

inductive fix (F : Type -> Type) : Type 1 | intro (a : Type) : F a -> (a -> fix) -> fix

It's not quite perfect though. For one thing, `fix`

lies in a different universe than `F`

so `F fix`

is not type correct. More type trickery can still help here.

In another direction, @Mario Carneiro, @Jeremy Avigad and I wrote a paper last year defining quotients of polynomial functors and using them to construct broader classes of inductive and coinductive data types in Lean. `Fix`

is a direct result of that theory QPF.

#### Wojciech Nawrocki (Jan 10 2020 at 13:33):

Then you should be able to write

`rename`

so that, together with`rewrite`

it will form`rename_all`

. What do you think?

Indeed that should work, but it will not if I modify the function a bit:

def weird_rename (x: string) (y: string): formula → formula | (var nm) := if nm = x then (var y) else (var nm) | (plus f₁ f₂) := mult f₁ (weird_rename f₂)

To express this, `rewrite`

would have to pass both rewritten and not-rewritten results, which can be done but I think it would have to make the resulting `rewrite'`

very specific. On first glance recursion schemes do seem to be solving a similar problem, thanks for the link!

#### Simon Hudon (Jan 10 2020 at 14:19):

No worries

#### Simon Hudon (Jan 10 2020 at 14:19):

Consider the following, I think it helps with your weird case:

open formula inductive formula_struct : formula → formula → Prop | plus₁ (f₁ f₂) : formula_struct f₁ (plus f₁ f₂) | plus₂ (f₁ f₂) : formula_struct f₂ (plus f₁ f₂) | mult₁ (f₁ f₂) : formula_struct f₁ (mult f₁ f₂) | mult₂ (f₁ f₂) : formula_struct f₂ (mult f₁ f₂) def weird_rename (x: string) (y: string): Π f : formula, (Π f', formula_struct f' f → formula) → option formula | (var nm) rec := some $ if nm = x then (var y) else (var nm) | (plus f₁ f₂) rec := some $ mult f₁ (rec f₂ $ by constructor) | (mult _ _) _ := none lemma well_founded_struct : well_founded formula_struct := sorry variable step : Π f : formula, (Π f', formula_struct f' f → formula) → option formula notation `♯` := by constructor def rewrite : formula → formula := well_founded.fix well_founded_struct $ λ x, match x with | e@(var v) := λ rec, match step e rec with | some e' := e' | none := e end | e@(plus x y) := λ rec, match step e rec with | some e' := e' | none := plus (rec x ♯) (rec y ♯) end | e@(mult x y) := λ rec, match step e rec with | some e' := e' | none := mult (rec x ♯) (rec y ♯) end end def weird_rename_all (x: string) (y: string): formula → formula := rewrite (weird_rename x y)

#### Simon Hudon (Jan 10 2020 at 14:19):

(it compiles)

#### Simon Hudon (Jan 10 2020 at 14:20):

But the proof of well-foundedness of the structural ordering is left as an exercise

#### Simon Hudon (Jan 10 2020 at 14:20):

You can also opt for a different well-founded relation

#### Wojciech Nawrocki (Jan 10 2020 at 15:05):

Thanks Simon, this is quite an interesting solution! By the way, is the generation of a `formula_struct`

roughly similar to what the equation compiler does?

#### Simon Hudon (Jan 10 2020 at 19:06):

By the way, is the generation of a formula_struct roughly similar to what the equation compiler does?

No. When declaring `formula`

, an axiom is added to the system:

#check @formula.rec -- formula.rec : -- Π {C : formula → Sort u_1}, -- (Π (a : string), C (formula.var a)) → -- (Π (a a_1 : formula), C a → C a_1 → C (formula.plus a a_1)) → -- (Π (a a_1 : formula), C a → C a_1 → C (formula.mult a a_1)) → -- Π (n : formula), C n

This is called a recursor. It is expressive enough to encode structural recursion and induction.

#### Wojciech Nawrocki (Jan 10 2020 at 23:43):

Right, `weird_rename`

is indeed expressible via `formula.rec`

. I was wondering more whether the equation compiler is capable of generating well-foundedness relations similar to `formula_struct`

in the `wf_rec`

module when structural recursion fails, as is the case for `rewrite`

but to think of it now that seems to be asking for way too much.

#### Simon Hudon (Jan 10 2020 at 23:49):

We could get `formula_struct`

generated ourselves

Last updated: May 10 2021 at 00:31 UTC