Release

The file maude2lean can be run as an executable in Unix-like systems or with python maude2lean. Alternatively, the package maude2lean-1.2.2-py3-non-any.whl can be installed with pip install.

Release notes

Changes introduced in 1.2.0

• New option with-native-bool that replaces Maude's Bool type with Lean's bool (or Bool in Lean 4) in the translation. The basic operators are also replaced by the Lean ones, _and_ maps to &&, _or_ to ||, and not to ¬. The additional operators are declared as constants and their equations as axioms in the bool (or Bool) namespace. Standard equality is used for bool terms, so the Lean translation will be inconsistent if the original Maude definition is.
• Lean 4 is now supported. However, since Lean 4 is still ongoing work, some features of Lean 3 used in the translation are missing. For that reason, the generation of lemmas is not complete and they are not annotated with the attributes that used to integrate them into the simplifier in Lean 3. Moreover, Lean 4 may fail to prove the termination of some definitions introduced with the derived-as-defs variant.
• The syntax for declaring notation has changed in a non-backwards compatible way in Lean 3.50.3. When the declare-notation option of maude2lean is used, the resulting program will not work for Lean versions before 3.50.3.
• Support for some special polymorphic operators in Maude, if_then_else_fi, _==_, and _=/=_, for which equations are now generated.
• More flexible input for the translation options. Previously, the command expected either a single JSON, YAML, TOML or Python dictionary with all the options, or a single Maude file to be used with the default settings. The command now admits one or more Maude and configuration files. All Maude files will be loaded and the options in the multiple configuration files will be combined. Moreover, most of these options can also be passed via arguments in the command line, which are listed with --help. The command-line arguments take precedence over the configuration files. The JSON schema for the options is now included in the package and can be obtained with maude2lean --dump schema.
• New option with-original-stmt that tells the translator to insert the original statement as a comment along with its translation.
• Notation is also used in the inductive definition of the rules according to the use-notation option (previously, it was not used but in the lemmas). As a consequence, the types of the statement arguments are given explicitly, since Lean cannot longer infer them.
• The implementation now ensures that the sort-membership premises for the variables in the translation of a Maude statement appear in the order the variables appear in the left-hand side and condition, considering a depth-first traversal that visits children from left to right. The order of the arguments in the inductive cases also follow the same criterion (previously they appear in alphabetical order).
• New dictionary option kind-renaming to allow renaming kinds. The name of any sort in the kind can be used as key.
• New Boolean option with-axiom-simp to include structural axioms in the repertory of definitions for the simplifier.
• Information about the whole-kind sort optimization is now shown in verbose mode.

Changes introduced in 1.1.0

• The frozen annotation of operators (for disabling rewriting in some of their arguments) is now taken into account in the translation. More precisely, no rw_one.sub_<operator><index> axioms are generated for those indices listed in the operator's frozen attribute. This behavior can be disabled with the with-frozen flag.
• New option sort-renaming to rename Maude sorts when translated to Lean. Moreover, sorts that are not valid identifiers in Lean (for example, parameterized sorts) are escaped to avoid errors.
• New option metamodule to use a module defined at the metalevel as input module for the translation.
• Fixed a buggy generation of definitions when there are multiple strongly-connected components of kinds.
• Maude Python library version 1.2.2 is required.