Lean backend

[anjapetkovic]

This PR creates a backend for Lean theorem prover, similar to the Rocq backend.
It uses the same structure of the backend as Rocq.hs, but adapted to Lean syntax in Lean.hs

The summary of the main changes:

• new file src/Act/Lean.hs that generates the state transition system in Lean
• new file lib/Actlib.lean that generates the act library for Lean, and it's accompanying lakefile.toml
• slightly changed test cases in tests/lean: the spec had to be changed from Rocq test case, because to is a reserved word in Lean
• A documentation of the Lean backend (similar to Rocq) in doc/src/lean.md
• Adapted documentation for Rocq backend, to account for the new way we report preconditions
• Nits to integrate the new backend into the pipeline.

[zoep]

Indentation seems weird here (also in the Rocq case, but it wont let me do a suggestion)

Suggested change

	| Lean { file :: w ::: Maybe String <?> "Path to file"
	| Lean { file :: w ::: Maybe String <?> "Path to file"

[zoep]

As a general remark for future work: we can consider factoring out commonalities in the interface for Rocq and Lean (e.g., have the specific prover be an option to a more general command).

[zoep]

Perhaps we could use a symbolic link to the AMM so that it automatically stays up-to-date when we change it?

[zoep]

Very nice work! Just some minor remarks.

[lefterislazar]

Looks good. There were some hypothesis that were left-over from before the factorization that was merged for Rocq, and their removal did not carry over. I also added some basic functionality to test the generated Lean files for compilation using make test-lean. After the checks we can merge.

[lefterislazar]

Everything looks good

[anjapetkovic]

Thanks for cleaning up the code Lefteris!