**diff options**

author | Thomas Letan <lthms@soap.coffee> | 2020-07-14 11:26:58 +0200 |
---|---|---|

committer | Thomas Letan <lthms@soap.coffee> | 2020-07-14 11:26:58 +0200 |

commit | c62a61dba7285a034fc0405edbd47dcc48bf03f5 (patch) | |

tree | 994a21ae6741acb026e73a8d0e85933f04562732 /site/posts/RewritingInCoq.v | |

parent | Identify the creation and last update date from the revisions table (diff) |

Prepare the introduction of a RSS feed

Diffstat (limited to 'site/posts/RewritingInCoq.v')

-rw-r--r-- | site/posts/RewritingInCoq.v | 24 |

1 files changed, 10 insertions, 14 deletions

diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v index 9c2efaf..0020a3e 100644 --- a/site/posts/RewritingInCoq.v +++ b/site/posts/RewritingInCoq.v @@ -1,17 +1,13 @@ -(** * Rewriting in Coq - - This article has originally been published on #<span class="time">May 13, - 2017</span>.# *) - -(** I have to confess something. In the published codebase of SpecCert lies a - shameful secret. It takes the form of a set of axioms which are not - required. I thought they were when I wrote them, but it was before I heard - about “generalized rewriting,” setoids and morphisms. - - Now, I know the truth. I will have to update SpecCert eventually. But, - in the meantime, let me try to explain how it is possible to rewrite a - term in a proof using a ad-hoc equivalence relation and, when - necessary, a proper morphism. *) +(** * Rewriting in Coq *) + +(** I have to confess something. In the codebase of SpecCert lies a shameful + secret. It takes the form of a set of unnecessary axioms. I thought I + couldn’t avoid them at first, but it was before I heard about “generalized + rewriting,” setoids and morphisms. Now, I know the truth, and I will have + to update SpecCert eventually. But, in the meantime, let me try to explain + in this article originally published on #<span id="original-created-at">May + 13, 2017</span> how it is possible to rewrite a term in a proof using a + ad-hoc equivalence relation and, when necessary, a proper morphism. *) (** #<div id="generate-toc"></div># |