ceps
ceps copied to clipboard
coq
User-defined rewrite rules
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.
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.
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?
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.
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.
+doesn't stay a constant, it unfolds to afixterm.
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.
It never becomes a neutral term, as it unfolds to a
fixconstruct.
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.
For rewriting on already existing definitions, might be related to #45.
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)...
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.
-
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.
-
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).
-
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 = rhsinto an axiomAxiom 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 commandCheck (fun variables => eq_refl : forall variables, lhs = rhs).
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.
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.
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.
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 = rhsinto an axiomAxiom 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?)
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.
By the way, why make it an a posteriori check?
Indeed, we can force rewrite rules to already holds propositionally, and this is how it is implemented in Agda. But this will only deal with "propositional" realization, rewrite rules will still be able to add potential non-termination. But as I said, I think I am fine with this solution where constistency issue is explicit in axioms and potential non-termination only can be added by rewrite rules.
rewrite rules will still be able to add potential non-termination.
Sure, and that is perfectly fine with me, as long as we can promise soundness to our users. They can use Rewrite; it is only if they use the Axiom keyword that they are on their own. (This is the kind of property that really matters in a certification context. You do not want the ANSSI declaring that Rewrite is forbidden from Coq developments.)
Unfortunately, for reasons discussed above, the solution of requiring first an Axiom or a proof of equality, and then turning an equality into a rewrite rule is simply not possible.
Indeed, as our criterion requires freshness of the symbol, one would not have any chance of proving any equality about it. Furthermore, not only the equalities, but the symbols themselves have to be treated as axioms.
So I don't see any other way than having rewrite rules and their symbols flagged when Printing Assumptions.
Indeed, as our criterion requires freshness of the symbol, one would not have any chance of proving any equality about it.
I never suggested that the equalities had to be stated and proved about the symbol itself, but only about a realization of it. So, to quote my own example,
in the case of parallel plus, the user could use the lemmas on standard plus to realize the rewriting rules
this would give:
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.
(Contrary to popular belief and what the lemma names seem to imply, the addition from the standard library is actually named Nat.add.)
At no point does this block add the relation add = plus to the context, neither definitionally nor propositionally. These are completely separate symbols and the former is only used once to ensure the soundness of the latter.
Ah yes. I had misunderstood you, sorry. 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?
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.
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?
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.
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;
.
I vaguely remember reading ANSSI recommendations about
Axiomthat were sensibly more nuanced than "never use the feature ever"
So, let me remind those recommendations:
- Developers are only allowed to use the logical axioms defined in the
Coq.Logic.*modules of the Coq standard library. - 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.
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_plusbesidesplus_O_netc.
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?
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.
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.
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.
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.
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 falsewith a proof that reduces toeq_reflin each case, and hence we'd be able to provetrue = falsewith a proof that reduces toeq_refl.
There we wouldn't have confluence though, right?