Recent Releases of maude2lean
maude2lean - 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](https://github.com/leanprover-community/lean/commit/31f3a46d7c18d6b2255a72df4f9d62644145d83b). 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_
- Lean
Published by ningit about 4 years ago
