Support field projectors for recursive structs in Lean backend

[R1kM]

Lean structures cannot be recursive. For this reason, recursive Rust structs are extracted to inductives with one constructor.

Similarly to what is already done for Coq, this PR generates projectors which allows to retrieve the expected behavior of structs once extracted to Lean. The translation function is similar to the one for Coq, however, there are some minor differences throughout the function, which is why I duplicated the code instead of making extract_type_decl_lean_record_field_projectors backend-generic.

This PR also removes the rewriting of Lean field projectors for recursive structs into let-bindings, to instead use the newly generated projectors.

I tested this feature with the following Rust code, which should be added to the testsuite once the refactoring of Aeneas tests (#182) is complete.

struct AVLNode<T> {
    value: T,
    left: AVLTree<T>,
    right: AVLTree<T>,
}

type AVLTree<T> = Option<Box<AVLNode<T>>>;


fn get_val<T>(x: AVLNode<T>) -> T  { x.value }

fn get_left<T>(x: AVLNode<T>) -> AVLTree<T> { x.left }

Fixes #185

[sonmarcho]

The output looks good. I just want to investigate the problem of generating simplification lemmas (see #185) before merging this.

[R1kM]

It seems that for structures, Lean 4 automatically adds the attribute reducible to projectors, which allows to retrieve the behavior you wanted (i.e., simplify even with simp only []).
Maybe we could just add this attribute to generated projectors?

[sonmarcho]

Following some experimentations, it seems we need to add @[reducible] and we also need to register explicitly register the projection functions for simp to reduce them. The function which does so is Lean.addProjectionFnInfo. We can write a custom command for this for the time being.

[sonmarcho]

There is an interesting discussion here as to why recursive structures are not supported:
leanprover/lean4#4182

[sonmarcho]

After some discussions: we will mark the projectors as reducible and simp for the time being.

[R1kM]

After some discussions: we will mark the projectors as reducible and simp for the time being.

This is done in e76ef95