\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

User-defined rewrite rules

Warning

Rewrite rules are highly experimental.

In particular, ill-typed rewrite rules will lead to mistyped expressions, and manipulating these will most often result in inconsistencies and anomalies.

This section describes the extension of Rocq's reduction mechanisms with user-defined rewrite rules, as a means to extend definitional equality. It should not be confused with the rewrite tactic or setoid rewriting which operate on propositional equality and other relations which are defined in Rocq.

Rewrite rules need to be enabled by passing the option -allow-rewrite-rules to the Rocq program.

Error Rewrite rule declaration requires passing the flag "-allow-rewrite-rules".

Symbols

Rewrite rules operate on symbols, which are their own kind of constants. They stand in-between defined constants and axioms, in that they don't always reduce as defined constants do, but they may still reduce using the provided rules, unlike axioms.

Command Symbol​Symbols assumpt​( assumpt )+

Binds an ident to a type as a symbol.

Symbol pplus : nat -> nat -> nat.
pplus is declared
Notation "a ++ b" := (pplus a b).

Rewrite rules

Command Rewrite Rule​Rules ident := |? rewrite_rule+|
rewrite_rule::=univ_decl |-? rw_pattern => term

Declares a named block of rewrite rules. The name is declared in the same namespace as constants and inductives.

Rewrite rules have two parts named pattern (left-hand side) and replacement (right-hand side). Patterns are a subclass of terms described below, while replacements are regular terms, which can also refer to the pattern variables matched by the pattern with the ?name syntax. When a rule is applied, the term is matched against the pattern, subterms aligned with pattern variables are collected and then substituted into the replacement, which is returned.

Rewrite Rule pplus_rewrite := | ?n ++ 0 => ?n | ?n ++ S ?m => S (?n ++ ?m) | 0 ++ ?n => ?n | S ?n ++ ?m => S (?n ++ ?m).

Pattern syntax

Patterns are a subclass of terms which are rigid enough to be matched against. Informally, they are terms with pattern variables (?name), where those may not appear on the left of applications or as the discriminee of a match or a primitive projection; furthermore a pattern may not have let-bindings, (co-)fixpoints or non-symbol constants.

As a formal grammar, it is easier to understand them with the separation between head-pattern (rw_head_pattern) and eliminations (non-base-case constructions for rw_pattern):

where qualid univ_annot? (in the second line for rw_head_pattern) can refer to symbols, sorts, inductives and constructors, but not arbitrary constants. The projections must be primitive to be allowed.

Finally, a valid pattern needs its head head-pattern to be a symbol.

Higher-order pattern holes

Patterns with lambdas (fun), products (forall) and matches introduce new variables in the context which need to be substituted in the replacement. To this end, the user can add what to substitute each new variable with, using the syntax ?name@{name := term+;}. Note that if in the replacement, the context was extended with a variable bearing the same name, this explicit substitution is inferred automatically (like for existential variable instantiations).

Symbol raise : forall (A : Type), A.
raise is declared
Rewrite Rule raise_nat :=   match raise nat as n return ?P   with 0 => _ | S _ => _ end   => raise ?P@{n := raise nat}.
Toplevel input, characters 93-118: > Rewrite Rule raise_nat := match raise nat as n return ?P with 0 => _ | S _ => _ end => raise ?P@{n := raise nat}. > ^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: This rewrite rule breaks subject reduction (universe inconsistency, missing constraints: Top.22 <= raise.u0). [rewrite-rules-break-SR,rewrite-rules,default]
Symbol id : forall (A : Type), A -> A.
id is declared
Rewrite Rule id_rew :=   id (forall (x : ?A), ?P) ?f => fun (x : ?A) => id ?P (?f x).

Universe polymorphic rules

Rewrite rules support universe and sort quality polymorphism. Universe levels and sort quality variables must be declared with the notation @{q1 q2|u1 u2+|+} (the same notation as universe instance declarations); each variable must appear exactly once in the pattern. If any universe level isn't bound in the rule, as is often the case with the level of a pattern variable when it is a type, you need to make the universe instance extensible (with the final +). Universe level constraints, as inferred from the pattern, must imply those given, which in turn must imply the constraints needed for the replacement. You can make the declared constraints extensible so all inferred constraints from the left-hand side are used for the replacement.

#[universes(polymorphic)] Symbol raise@{q|u|} : forall (A : Type@{q|u}), A.
raise is declared
Rewrite Rule raise_nat :=   @{q|u+|+} |- raise@{q|u} (forall (x : ?A), ?P) => fun (x : ?A) => raise@{q|u} ?P.

Rewrite rules, type preservation, confluence and termination

Currently, rewrite rules do not ensure that types must be preserved. There is a superficial check that the replacement needs to be typed against the type inferred for the pattern (for an unclear definition of type of a pattern), but it is known to be incomplete and only emits a warning if failed. This then means that reductions using rewrite rules have no reason to preserve well-typedness at all. The responsibility of ensuring type preservation falls on the user entirely.

Similarly, neither confluence nor termination are checked by the compiler.

There are future plans to add a check on confluence using the triangle criterion [CTW21] and a more complete check on type preservation.

Compatibility with the eta laws

Currently, pattern matching against rewrite rules pattern cannot do eta-expansion or contraction, which means that it cannot properly match against terms of functional types or primitive records. As with type preservation, a check is done to test whether this may happen, but it is not complete (false positives) and thus only emits a warning if failed.

Level of support

Rewrite rules have been integrated into the kernel and the most used parts of the upper layers. Notably, reduction machines simpl, cbn and cbv can reduce on rewrite rules, with some limitations (e.g. simpl cannot reduce on rules which contain a match). Also, regular unification can work with rewrite rules, as well as apply's unification mechanism in a limited manner (only if the pattern contains no match or projections).

On the other hand, some operations are not supported, such as declaring rules in sections and some interactions with modules. Since rewrite rules may introduce untyped terms, which the VM and native reduction machines don't support (risk of segfault or code injection), they are turned off when rewrite rules are enabled.