User-defined rewrite rules

[TheoWinterhalter]

We propose an extension of Coq with user-defined rewrite rules, following our work on formalising rewrite rules in MetaCoq and the paper The Taming of the Rew.

Rendered here.

[silene]

Are the following two sentences not contradictory?

We could in principle allow for more terms to qualify as symbols such as definitions (constants).

Rewrite rules are triggered when a term is stuck with respect to the regular rules of Coq.

Also, the following part should really be emphasized:

uncareful rewrite rules could lead to [...] anomalies (by breaking subject reduction for instance)

The proposal would indeed make it trivial for a user to accidentally corrupt the memory of the Coq process.

[TheoWinterhalter]

It might be trickier to implement than in Agda but for your contradiction I meant using the already defined addition and add

Rewrite Rule ?n ?m ⊢ ?n + (S ?m) ⇒ S (n + m)

The rule would not trigger in the case of S n + S m because the natural reduction rule has priority, but it would trigger once the left-hand side becomes a neutral term.

As I was saying, in Agda where they have function symbols it seems easier, because here the unfolding rule would simply mean that the rewrite rule would never apply.

---

How do you suggest I emphasise more on the corruption part?

[SkySkimmer]

The rule would not trigger in the case of S n + S m because the natural reduction rule has priority, but it would trigger once the left-hand side becomes a neutral term.

+ doesn't stay a constant, it unfolds to a fix term.

[silene]

but it would trigger once the left-hand side becomes a neutral term.

It never becomes a neutral term, as it unfolds to a fix construct.

How do you suggest I emphasise more on the corruption part?

Not sure. For me, this is kind of a show stopper.

[TheoWinterhalter]

+ doesn't stay a constant, it unfolds to a fix term.

I know, I even said it in my own message…

---

Regarding the unsafe aspect, it seems that people would like to be able to do it anyway.
If this is not possible to add to Coq, then we could consider adding only safe rewrite rules as we do in MetaCoq, but that would require a lot more work.

[tabareau]

It never becomes a neutral term, as it unfolds to a fix construct.

Indeed, I think you are right, mentioning potential extension of definitions as symbols was a bad idea. The fact that it is possible in Agda is very specific to the system and I don't think it can be done in a similar way in Coq.

[TheoWinterhalter]

For rewriting on already existing definitions, might be related to #45.

[CohenCyril]

Since the word Rewrite is overloaded and for most end-user currently mean rewrite as in the tactic performing substitution of propositional equality, may I suggest this is not called Rewrite, but something else like Reduction, Conversion, or something with Rule inside (if you still want to appeal to rewrite systems backgrounds)...

[gasche]

In the case of Axiom, there is a clear notion of what it means to realize an axiom: provide a term of the axiomatized type . In some cases a development can be de-axiomatized after the fact by providing a model, terms for the axioms and proofs of their axiomatized properties.

I wonder (1) what is the natural countepart of axiom realization for rewrite blocks, (2) what are their theoretical properties, and (3) how one would check a realization in practice. I think that it may make sense to discuss these questions in the document.

My current understanding is as follows.

1. There are two natural notions of "realizing a rewrite block", propositional realization where we provide terms, and show propositional equalities between the lhs and rhs of each rule, and definitional realization, where we show definitional equalities. Propositional realization corresponds to the notion of instantiation of a rewrite block in the Taming of the Rew paper.

2. Propositional realization guarantees consistency, but it does not guarantee decidability and normalization. Definitional realization should guarantee decidability (there is a discussion in the "Abstracting over Rewrite Rules paragraph in Future Work, it's subtle but the current propsal should be okay).

3. With only the features proposed in the CEP, a user can manually check a candidate for a propositional realization. This amounts to translating each equation lhs = rhs into an axiom Axiom eqn: forall variables, lhs = rhs, and realizing it. It is also possible, but more cumbersome, to check a candidate for definitional realization, by turning each postulated equation into a command Check (fun variables => eq_refl : forall variables, lhs = rhs).

[TheoWinterhalter]

I am not sure realising with conversion is enough. Or at least, it is not obvious that it works, and it's partly what blocked us when trying to do that. Even in practice, it would be interesting to have a local counterpart to rewrite rules, like we have lambda-abstraction as a local version of Axiom somehow.
But since we're dealing with reduction, turning a reduction into a conversion might break properties like confluence of said reduction, termination etc.

[tabareau]

Thx @gasche for your feedback. All that you say here is fairly right, what I am missing is the motivation.

If you can inhabit an axiom within Coq, then it should not be considered as an axiom anymore, right ? The point of axioms is to go beyond the expressivity of your logic. Otherwise, they are just auxiliary assumptions that will be discarded later. It is the same for rewrite rules, if you postulate a rewrite rule R on an axiom C that you can inhabit later with a term such that R holds definitionally, then you can simply remove R from your development so there is no issue anymore.

Otherwise, you are postulating a rewrite rule that goes beyond the theory of Coq (such as for the parallel plus) and then you can just check that it is propositionally valid, by proving for instant that the usual plus that matches on the left validates the propositional equalities of parallel plus. Therefore, you get consistency (and confluence and SR) but you can only "observe" termination of the type checking algorithm, there is no way to be sure about it inside Coq. But I don't really see the problem ?

If you agree with this, of course we can make it more clear in the CEP/Documentation.

[gasche]

Sometimes we would sketch a development by axiomatizing a part of the theory, hoping to prove later than the axioms can in fact be realized. (In practice I think people use Admitted. much more than Axiom. in this scenario.)
There is also the situation where there are several possible models (for example: definitions of real numbers) and we want the development to be agnostic over the choice of model. (For this it is common to use Variable and the section mechanism, parametrized modules are out of fashion, and people also use type-classes.)

But rather than a strong practical motivation, my question was more from the language-design point of view: if we introduce a new mechanism for abstraction/parametrization/axiomatization, I think that it is interesting to understand what is the corresponding instantiation/realization operation, and in the present case the answer is not obvious.

[silene]

With only the features proposed in the CEP, a user can manually check a candidate for a propositional realization. This amounts to translating each equation lhs = rhs into an axiom Axiom eqn: forall variables, lhs = rhs

By the way, why make it an a posteriori check? Why not force the user to provide a proof term a priori for each rewrite rule? Obviously, the user could still "prove" these rules by stating the corresponding axioms, but then it becomes apparent what is an axiom in a Coq development. For example, in the case of parallel plus, the user could use the lemmas on standard plus to realize the rewriting rules, thus removing any axiom.

Or are there some cases where the user would not even be able to state axioms for these rewriting rules? (Universes?)

[tabareau]

Ok, so maybe the problem is rather the lack of abstraction/parametrization of our current version of rewrite rules. As you noticed in our paper, we have a paragraph "Abstracting over Rewrite Rules", but this is to say that we don't know how to justify the theory for the moment. Maybe what you suggest in the end is to solve this issue before looking for a concrete implementation in Coq ? Indeed, solving this issue will in particular provide a clear answer to your initial question I think.

[silene]

In cases where realisation is impossible because we want to extend the theory, then we might have to add as many axioms as there are symbols and rewrite rules however with this, right?

Right. But since those are actually axioms, the extra verbosity does not seem much of an issue. And if this happens too often (I doubt it, but maybe I am wrong), we could always devise another syntax, e.g., Axiom Rewrite instead of plain Rewrite.

[TheoWinterhalter]

Let's say we want to do it for Nat.add (we don't but let's assume so for the sake of the argument). We would then do

Axiom ax_plus : nat -> nat -> nat.
Axiom plus_O_n : ...
Axiom plus_Sn_m : ...
Axiom ...

Rewrite Block :=
  plus : nat -> nat -> nat ;
with rules
  plus 0 ?n := n ;
  plus ?n 0 := n ;
  plus (S ?n) ?m := S (plus n m) ;
  plus ?n (S ?m) := S (plus n m)
using ax_plus, plus_O_n, plus_n_O, plus_Sn_m, plus_n_Sm.

Then the plus from the rewrite rules is not the same as the ax_plus axiom.
If I understand correctly, then when printing the assumptions for plus or any term depending on it / and its rewrite rules, we would list ax_plus besides plus_O_n etc. All this in addition to saying the term might be typed using rewrite rules.

Would that be the plan?

[gasche]

For the record, I am not so convinced by @silene's point in general. It looks very cumbersome to have to first define one axiom per symbol and equation, and then restate them in a rewrite block. The CEP mentions that Print Assumptions would list assumptions arising from rewrite blocks, and I vaguely remember reading ANSSI recommendations about Axiom that were sensibly more nuanced than "never use the feature ever", so we could hope for a similar treatment here.

I do think it would be nice to have a syntax to give a propositional realization for parts of the rewrite block. Ideally it would be slightly more pleasant than the one proposed above, with each realizing term given (optionally, if available) at the point where the corresponding term or equation is introduced, and not all of them at the end.

[gasche]

So instead of

Rewrite Block :=
  plus : nat -> nat -> nat ;
with rules
  plus 0 ?n := n ;
  plus ?n 0 := n ;
  plus (S ?n) ?m := S (plus n m) ;
  plus ?n (S ?m) := S (plus n m)
using add, plus_O_n, plus_n_O, plus_Sn_m, plus_n_Sm.

that would be, maybe

Rewrite Block :=
  plus : nat -> nat -> nat    by add;
with rules
  plus 0 ?n := n    by plus_O_n;
  plus ?n 0 := n    by plus_n_O;
  plus (S ?n) ?m := S (plus n m)    by plus_Sn_m;
  plus ?n (S ?m) := S (plus n m)    by plus_n_Sm;
.

[silene]

I vaguely remember reading ANSSI recommendations about Axiom that were sensibly more nuanced than "never use the feature ever"

So, let me remind those recommendations:

1. Developers are only allowed to use the logical axioms defined in the Coq.Logic.* modules of the Coq standard library.
2. Developers shall provide a model —potentially trivial— which satisfies the hypotheses they introduce.

Point 2 is why I am insisting on the user having to realize the rewriting rules of a Rewrite block.

[silene]

If I understand correctly, then when printing the assumptions for plus or any term depending on it / and its rewrite rules, we would list ax_plus besides plus_O_n etc.

Yes. (Though, in the case of Nat.add, since it is already defined by the standard library, it would not appear as an axiom.)

All this in addition to saying the term might be typed using rewrite rules.

It depends. Do you think it matters whether a term is typed using rewriting rules or not?

[gares]

If the point is to have Axiom when something is assumed without any evidence, then maybe

Axiom plus : nat -> nat -> nat with
Rewrite Rules
  plus 0 ?n  ==> ?n.

Rewrite Rules for
  plus := add (* no type needed I guess, since they must match *)
with
  plus 0 ?n ==> ?n    by plus_0_n. (* or := plus_0_n 0 ?n *)

I took the liberty to ditch := which is not really suggesting an orientation.

[JasonGross]

Propositional realization guarantees consistency

Consistency with the base theory of Coq but not with consistent extensions, right? E.g., propositional realization is not enough to remain consistent with univalence, I think.

[TheoWinterhalter]

Propositional realization guarantees consistency

Consistency with the base theory of Coq but not with consistent extensions, right? E.g., propositional realization is not enough to remain consistent with univalence, I think.

I believe that it would work with 2-level type theory, using reflection on the strict equality.

[JasonGross]

Consider:

Definition foo (x y : nat) := existT (fun T => T) bool true.
Rewrite Block :=
  bar : nat -> nat -> { T : Type & T }    by foo;
with rules
  bar 0 ?n ==> existT _ bool true    by ltac:(reflexivity);
  bar ?n 0 ==> existT _ bool false    by proof_using_univalence;
.

Then I believe we'd be able to prove bar 0 0 = existT _ bool true = existT _ bool false with a proof that reduces to eq_refl in each case, and hence we'd be able to prove true = false with a proof that reduces to eq_refl.

[TheoWinterhalter]

Consider:

Definition foo (x y : nat) := existT (fun T => T) bool true.
Rewrite Block :=
  bar : nat -> nat -> { T : Type & T }    by foo;
with rules
  bar 0 ?n ==> existT _ bool true    by ltac:(reflexivity);
  bar ?n 0 ==> existT _ bool false    by proof_using_univalence;
.

Then I believe we'd be able to prove bar 0 0 = existT _ bool true = existT _ bool false with a proof that reduces to eq_refl in each case, and hence we'd be able to prove true = false with a proof that reduces to eq_refl.

There we wouldn't have confluence though, right?

[JasonGross]

There we wouldn't have confluence though, right?

Indeed, but you can still generate the requisite proof term by proving bar1 : forall n, bar 0 n = existT _ bool true by reflexivity, and bar2 : forall n, bar n 0 = existT _ bool false by reflexivity, and then you have eq_trans (eq_sym (bar1 0)) (bar2 0) : existT _ bool true = existT _ bool false and if you apply projT2_eq to this proof then you get a proof which reduces to eq_refl (without the use of any rewrite rules) with a type that reduces to true = false (again without the use of any rewrite rules).

Is there some way of guaranteeing confluence / checking for confluence built in here?

[TheoWinterhalter]

Rewrite rules are only safe if they preserve confluence. In our paper "The Taming of the Rew", this is what we propose.

[JasonGross]

Interesting. What about this? I think this is still confluent, and yet leads to inconsistency with univalence:

Rewrite Block :=
  prod' : Type -> Type -> Type  by prod;
  pair' : forall A B, A -> B -> prod' A B by pair;
  fst' : forall A B, prod' A B -> A by fst;
  snd' : forall A B, prod' A B -> B by snd;
with rules
  fst' (pair' ?x ?y) ==> x  by ltac:(reflexivity);
  snd' (pair' ?x ?y) ==> y  by ltac:(reflexivity);
  prod' bool nat ==> prod' unit nat  by proof_involving_univalence;
.

I think this set of rewrite rules is confluent? There might be some subtlety here in lack of confluence on terms that fail to typecheck at all in the absence of some of the rewrite rules?*

If so, I believe we can now prove prod' bool nat = prod' unit nat by eq_refl. This is a problem, though, because it gives an equivalence between bool * nat and unit * nat which is the identity on the second component, and hence leads to a proof that bool and unit are equivalent. (Roughly, since nat is inhabited, you get a proof that (x, 0) round-trips for all x.)

* It's not clear to me what exactly is being checked for confluence. But perhaps I am running into an assumption of the paper: "Note that in our more general setting with inductive types, the injectivity of inductive types can be formulated and proven in the same way."

Edited: Hm, I guess maybe I don't quite get that the equivalence is identity on the second component, because @snd' bool nat (@pair' unit nat tt 0) won't reduce to 0 because it doesn't match the given rewrite rule for snd'?

[TheoWinterhalter]

For now at least, in our formalism we don't consider type constructors as patterns, and, considering your example it seems that we might run into trouble by allowing them.

[JasonGross]

For now at least, in our formalism we don't consider type constructors as patterns, and, considering your example it seems that we might run into trouble by allowing them.

Does this mean that type constructors cannot appear anywhere in patterns?

[TheoWinterhalter]

I see that the CEP does mention inductive type constructors in patterns so I'm sorry. In the formalisation, we only deal with Coq's patterns. So I cannot really say for sure what would adding them cost.

[JasonGross]

For now at least, in our formalism we don't consider type constructors as patterns, and, considering your example it seems that we might run into trouble by allowing them.

Actually, I don't think this buys you anything, since we can just write

Rewrite Block :=
  prod' : Type -> Type -> Type  by prod;
  pair' : forall A B, A -> B -> prod' A B by pair;
  fst' : forall A B, prod' A B -> A by fst;
  snd' : forall A B, prod' A B -> B by snd;
  nat' : Set by nat;
  bool' : Set by bool;
  nat'_eq : nat' = nat by eq_refl nat;
  bool'_eq : bool' = bool by eq_refl bool;
with rules
  fst' (pair' ?x ?y) ==> x  by ltac:(reflexivity);
  snd' (pair' ?x ?y) ==> y  by ltac:(reflexivity);
  prod' bool' nat' ==> prod' unit nat'  by proof_involving_univalence;
.

[TheoWinterhalter]

Even in the current CEP we don't consider symbols as patterns. In the formalisation it's really only constructors of inductives types and pattern variables.

[Blaisorblade]

Looking at the examples, it'd be nice if this proposal didn't duplicate the features from module types. Module Types cannot express of course an interface with arbitrary definitional equalities; however, checking propositional realization amounts to converting the rules to a Module Type and providing an implementing Module.

And it seems that you could just as well allow marking equations in module types as rewrite rules. It seems you want the user to use one pragma to mention a symbol and the associated rules, instead of an attribute on the axioms; still, that per se doesn't mean you need yet another way to introduce axioms.

That seems generally more orthogonal, and could enable reusing various features of the module system.

• Import/Export
• module abstractions via
• you could more easily abstract over an arbitrary instantiation of the module, instead of fixing one in advance and needing to add extra boilerplate to do the abstraction yourself.

The downside might be that more feature interaction are possible and need to be tested.

[Alizter]

I quite like @Blaisorblade's suggestion here. It also means that things like confluence checking can be delayed to the closing of a module. It would also make the interactive development of proving rewrite rules much easier than having to specify them all at once.

[TheoWinterhalter]

We haven't updated this in a long while but we are in the process of reviving it with also @mattam82 and @yannl35133. For now the plan is to have something in an experimental branch/fork of Coq so that we (and users) can test it without committing to anything. This experimental version will not support any check for confluence, subject reduction or termination for now.

For now we're going with the possibility to add rewrite rules on axioms (only) using equalities to describe rewrite rules (similarly to Agda).

[Alizter]

Something interesting to note that I have been thinking about. If we have the ability to define rewrite rules in module signatures, then this could allow us to faithfully implement #62. We would be able to allow the user to abstract the types and terms appearing in a module, and furthermore specify how things compute.

[TheoWinterhalter]

Ideally yes, but I'm not expert enough in modules to sell you this. I will say that I'm also working on local rewrite rules, ie that you can instantiate either by objects that very the equations with conversion, or propositionally. The latter being much harder. This should in principle help go in the direction of that. And also make it possible to get rid of rewrite rules in a development so as to satisfy eg the ANSSI rules. But we're not there yet.

(Edit: sorry for the close/open, it was a misclick.)