<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>Dear all,</p>
<p>CoqMT is not really Coq modulo rewriting but rather Coq modulo
decision procedures like linear arithmetic, etc. Unfortunately, it
is not developed anymore at the moment I think.<br>
</p>
<p>For a proof assistant with builtin rewriting, I invite you to
have a look at Dedukti, or rather its new interactive version,
Lambdapi (future Dedukti v3),
<a class="moz-txt-link-freetext" href="https://github.com/Deducteam/lambdapi">https://github.com/Deducteam/lambdapi</a>. See its documentation on
<a class="moz-txt-link-freetext" href="https://github.com/Deducteam/lambdapi/blob/master/doc/DOCUMENTATION.md">https://github.com/Deducteam/lambdapi/blob/master/doc/DOCUMENTATION.md</a>
. Lambdapi is still under development and misses a basic library
but this will be fixed in the next months. So stay tuned! You can
however have a look at some of the test files to see how it looks
like. For instance,
<a class="moz-txt-link-freetext" href="https://github.com/Deducteam/lambdapi/blob/master/tests/OK/rewrite.lp">https://github.com/Deducteam/lambdapi/blob/master/tests/OK/rewrite.lp</a>
,
<a class="moz-txt-link-freetext" href="https://github.com/Deducteam/lambdapi/blob/master/tests/OK/natproofs.lp">https://github.com/Deducteam/lambdapi/blob/master/tests/OK/natproofs.lp</a>
or
<a class="moz-txt-link-freetext" href="https://github.com/Deducteam/lambdapi/blob/master/tests/OK/245.lp">https://github.com/Deducteam/lambdapi/blob/master/tests/OK/245.lp</a>
.<br>
</p>
<p>Some new VSCode interface has been developed and should be
released in the next months (there are also simple interfaces with
vim and emacs). Its current set of tactics is very basic but
should be improved in the next months. Two important tactics are
much more advanced though: a rewriting tactic following the
SSReflect syntax and semantics, and a tactic for calling external
automated theorem/SAT/SMT provers through the Why3 library
(available in the next days).<br>
</p>
<p>Dedukti implements the lambda-Pi-calculus modulo user-defined
rewriting. See below for some references. In particular, adding
rewriting to dependent types allows to easily encode many other
systems: HOL, Matita, Coq, Isabelle or Agda (work in progress).<br>
</p>
<p>Dedukti includes a builtin subject-reduction checker (a new more
powerful algorithm based on Knuth-Bendix completion will be
released in the next months). For confluence, you can call
external confluence checkers like CSI^ho or other confluence
provers participating to the competition on confluence
(<a class="moz-txt-link-freetext" href="http://project-coco.uibk.ac.at/">http://project-coco.uibk.ac.at/</a>). Idem for termination using an
extension to dependent types of the format for termination
problems of the termination competition
(<a class="moz-txt-link-freetext" href="http://termination-portal.org/wiki/Termination_Competition">http://termination-portal.org/wiki/Termination_Competition</a>). See
<a class="moz-txt-link-freetext" href="https://github.com/Deducteam/lambdapi/blob/master/doc/sections/options.md">https://github.com/Deducteam/lambdapi/blob/master/doc/sections/options.md</a>
for more details. In particular, Guillaume Genestier developed a
termination checker prototype for Dedukti that could be extended
to Agda.<br>
</p>
<p>Some references (we could add more):<br>
</p>
<p>- Dedukti: a Logical Framework based on the lambda-Pi-Calculus
Modulo Theory, A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G.
Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R.
Saillard, <a class="moz-txt-link-freetext" href="http://www.lsv.fr/~dowek/Publi/expressing.pdf">http://www.lsv.fr/~dowek/Publi/expressing.pdf</a> ,
submitted.</p>
<p>- Dependency Pairs Termination in Dependent Type Theory Modulo
Rewriting, <a class="moz-txt-link-freetext" href="http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.9">http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.9</a> , 2019.</p>
<p>- Definitions by rewriting in the Calculus of Constructions,
<a class="moz-txt-link-freetext" href="https://doi.org/10.1017/S0960129504004426">https://doi.org/10.1017/S0960129504004426</a> , 2005.</p>
<p>- Dependent type theory with first-order parameterized data types
and well-founded recursion, D. Wahlstedt,
<a class="moz-txt-link-freetext" href="http://www.cse.chalmers.se/alumni/davidw/wdt_phd_printed_version.pdf">http://www.cse.chalmers.se/alumni/davidw/wdt_phd_printed_version.pdf</a>
, 2007.<br>
</p>
<p>- Type checking in the Lambda-Pi-calculus modulo: theory and
practice, PhD thesis, R. Saillard,
<a class="moz-txt-link-freetext" href="https://pastel.archives-ouvertes.fr/tel-01299180">https://pastel.archives-ouvertes.fr/tel-01299180</a> , 2015.</p>
<p>- Type theory and rewriting, PhD thesis,
<a class="moz-txt-link-freetext" href="http://hal.inria.fr/inria-00105525">http://hal.inria.fr/inria-00105525</a> , 2001.</p>
<p>- Modularity of strong normalization in the
algebraic-lambda-cube, F. Barbanera and M. Fernandez and H.
Geuvers, <a class="moz-txt-link-freetext" href="http://journals.cambridge.org/article_S095679689700289X">http://journals.cambridge.org/article_S095679689700289X</a> ,
1997.</p>
<p><br>
</p>
<div class="moz-cite-prefix">Le 21/10/2019 à 22:04, Bas Spitters a
écrit :<br>
</div>
<blockquote type="cite"
cite="mid:CAOoPQuR8AAKyKLQ-Dvk1Xr30G_qMZUNkz=nPVLgNMMGdnrMDNg@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>One development for such meta-theory is available for
CoqMT.<br>
</div>
<div><a href="https://hal.archives-ouvertes.fr/hal-01664457"
moz-do-not-send="true">https://hal.archives-ouvertes.fr/hal-01664457</a></div>
<div>I wonder about the relation with the rewriting technology
in Jesper's blog post.</div>
<div><br>
</div>
<div>Bas<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, Oct 21, 2019 at 9:36
PM Jon Sterling <<a href="mailto:jon@jonmsterling.com"
moz-do-not-send="true">jon@jonmsterling.com</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi
Jesper,<br>
<br>
I'm very pleased to hear that the confluence checker is coming
along! Once it is in place, what kind of syntactic guarantees
(relative to "pure Agda") can we expect to be available in the
presence of custom rewrite rules? <br>
<br>
The main one I'm asking about is transitivity: if judgmental
equality is transitive in plain Agda, then does one expect it
to be transitive in Agda mod T, for T a set of rewrite rules
that would accepted by the completed checker? If so, the
rewriting facility sounds totally amazing and really useful.<br>
<br>
Maybe in the future we can just use Agda to prototype most new
extensions to type theory, rather than writing our own
implementations right away. <br>
<br>
<br>
Best,<br>
Jon<br>
<br>
<br>
<br>
On Mon, Oct 21, 2019, at 12:14 PM, Jesper Cockx wrote:<br>
> Hi Apostolis,<br>
> <br>
> Excellent question! Unfortunately, the answer is not an
unqualified <br>
> 'yes'. It is true that using such rewrite rules always
preserves <br>
> soundness of the theory, since rewrite rules are in a
sense a limited <br>
> form of equality reflection, and equality reflection is
known to be <br>
> consistent.<br>
> <br>
> However, other more syntactic properties such as
confluence, <br>
> termination, and subject reduction (aka type
preservation) can still be <br>
> broken. In our 2014 paper, I give one such example: the
rewrite rules <br>
> `(suc x) * y == (x * y) + y` and `x * (suc y) == x + (x *
y)` are not <br>
> confluent unless you also have associativity of + as a
rewrite rule. <br>
> It's not very straightforward, but by tricking Agda's
constraint solver <br>
> to solve equations in a particular order, you can exploit
a <br>
> non-confluence like this to break subject reduction. This
manifests as <br>
> a type error complaining two things should be equal even
though they <br>
> are according to the rules.<br>
> <br>
> I have actually been working on implementing a confluence
checker for <br>
> rewrite rules (which I'm planning to talk about in an
upcoming post). <br>
> If you want, you can try it out by installing the current
master branch <br>
> of Agda and enabling the --confluence-check flag.<br>
> <br>
> Cheers,<br>
> Jesper<br>
> <br>
> On Mon, Oct 21, 2019 at 4:21 PM Apostolis Xekoukoulotakis
<br>
> <<a href="mailto:apostolis.xekoukoulotakis@gmail.com"
target="_blank" moz-do-not-send="true">apostolis.xekoukoulotakis@gmail.com</a>>
wrote:<br>
> > If you have proved the equality as in your 2nd
example, is there any reason not to use REWRITE? <br>
> > My impression is that I should use REWRITE
everywhere where I have proven a propositional equality so as
to make it definitional.<br>
> > <br>
> > Nice blog post, and a good reference to a book on
type theory. I was looking into a good introductory book that
would help me understand agda a bit better.<br>
> > <br>
> > On Mon, Oct 21, 2019 at 4:22 PM Jesper Cockx <<a
href="mailto:Jesper@sikanda.be" target="_blank"
moz-do-not-send="true">Jesper@sikanda.be</a>> wrote:<br>
> >> Hi Agda folks,<br>
> >> <br>
> >> I have another blog post for you on extending
Agda with rewrite rules, with no less than six examples of how
they can be used. You can read it at <a
href="https://jesper.sikanda.be/posts/hack-your-type-theory.html"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://jesper.sikanda.be/posts/hack-your-type-theory.html</a>.
Any comments are welcome here on the mailing list as usual.<br>
> >> <br>
> >> Cheers,<br>
> >> Jesper<br>
> >> _______________________________________________<br>
> >> Agda mailing list<br>
> >> <a href="mailto:Agda@lists.chalmers.se"
target="_blank" moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
> >> <a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
> <a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>