Maude2Lean — Reference of constructor names and lemmas
For every kind k in the Maude specification, an inductive type ks is defined where s is the first of the most general sorts in the kind. Moreover, some other inductive types and definitions are generated
- the inductive type
MSort enumerating the sorts of the module,
- the function
kind : MSort → Type mapping each sort to its kind,
- the relation
subsort : MSort → MSort → Prop specifying the generator of the subsort relation given by the subsort statements in Maude,
- the predicates k
.ctor_only : k → Prop that holds on terms all whose symbols are constructor terms as indicated by the Maude attribute ctor,
- and the functions k
.repr : k → string that gives a string representation of a term.
The last two definitions are families of functions, one for each kind, and their generation is disabled by default (see the translation options).
Relation constructors
The following binary relations are inductively defined for each kind k with the constructors enumerated in the tables below:
- k
.eqa for equality modulo structural axioms (associativity, commutativity, etc),
- k
.has_sort for the membership of a term in a sort,
- k
.eqe for equality modulo equations and structural axioms,
- k
.rw_one for the one-step sequential rule-rewrite relation,
- and k
.rw_star for the reflexive and transitive closure of the previous.
The constructor c of the relation k.r can be accessed with k.r.c. Moreover, aliases can be declared for some constructors at the kind namespace by enabling the with-aliases option in the configuration. Infix notation can also be defined for the relation with the use-notation option.
Some constructors are the translation of statements (membership axioms, equations, and rules) in the Maude module. Their names in the tables below include a fragment label that will be filled with the label attribute of the statement. In the absence of that attribute, the constructor is labeled with the name of the top symbol of its left-hand side. Names clashes are disambiguated by appending a number to the labels in the order they appear in the Maude source.
Equality modulo structural axioms (eqa)
| Name |
Meaning |
Alias |
refl |
Reflexivity |
✗ |
symm |
Symmetry |
✗ |
trans |
Transitivity |
✗ |
eqa_f |
Congruence axiom for f |
✓ |
f_comm |
Commutativity for f |
✓ |
f_assoc |
Associativity for f |
✓ |
f_left_id |
Left identity for f |
✓ |
f_right_id |
Right identity for f |
✓ |
f_idem |
Idempotency for f |
✓ |
Sort membership (has_sort)
| Name |
Meaning |
Alias |
subsort |
Subsort membership implies sort membership (depends on subsort) |
See lemmas |
f_decl |
Implicit membership axiom in the operator declaration of f |
✓ |
mb_label |
Explicit membership axiom |
✓ |
Equality modulo equations (eqe)
| Name |
Meaning |
Alias |
from_eqa |
Extension of =A |
✗ |
symm |
Symmetry |
✗ |
trans |
Transitivity |
✗ |
eqe_f |
Congruence axiom for f |
✓ |
eq_label |
Explicit equation in Maude |
✓ |
One-step sequential rule rewrite (rw_one)
| Name |
Meaning |
Alias |
eqe_left |
Rewriting modulo =E (left-hand side) |
✗ |
eqe_right |
Rewriting modulo =E (right-hand side) |
✗ |
symm |
Symmetry |
✗ |
trans |
Transitivity |
✗ |
sub_fi |
Rewrite inside the ith argument of f |
✓ |
rl_label |
Explicit rewrite rule in Maude |
✓ |
Rewrite in any number of steps (rw_star)
| Name |
Meaning |
Alias |
step |
Extension of →R |
✗ |
symm |
Symmetry |
✗ |
trans |
Transitivity |
✗ |
Lemmas
| Name |
Meaning |
subsort_s_r |
Terms in a subsort s are in the supersort r (for every pair in the subsort relation generator) |
eqe_refl |
Equality modulo equations is reflective |
eqa_congr |
=A is a congruence for itself |
eqe_congr |
=E is a congruence for itself |
eqa_eqe_congr |
=A is a congruence for =E |
eqa_rw_one_congr |
=A is a congruence for →R |
eqe_rw_one_congr |
=E is a congruence for →R |
eqa_rw_star_congr |
=A is a congruence for →R* |
eqe_rw_star_congr |
=E is a congruence for →R* |
rw_star_sub_fi |
Sequence of rewrites inside the ith argument of f |