<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>