feat: submission

Author: FWuermse

docs/algorithm.typ

@@ -2,6 +2,7 @@
 #import "./template.typ": *
 #import "./theme.typ": *
 #import "@preview/algo:0.3.4": algo, i, d, comment, code
+#pagebreak()
 = Generalised Rewriting in Literature <PaperAlgo>
 
 We briefly mentioned that the literature algorithm about generalised rewriting consists of two parts. To understand the proof and constraint generation section of that algorithm, we will start by introducing Lean expressions, explain Coq's morphism framework, and finally provide the algorithm specification.
@@ -49,8 +50,6 @@ Metavariables of a certain type $Gamma tack tau$ can be assigned with any value
 
 Another concept frequently used in the rewriting algorithm we propose is unification. In Lean 4, unification refers to the assignments of metavariables so that two terms $t$ and $u$ containing them become definitionally equal @ullrich @carneiro2019type. We will refer to two different functions for unification. Given a term $rho : r space a space a'$ with $r : alpha -> alpha -> mono("Prop")$ and $a space a' : alpha$, the function $mono("unify")_rho (t)$ tries to unify t with the left-hand side of $rho$'s applied relation. The function also introduces local hypotheses for bound variables of possible `forallE` or `lam` expressions in $t$, in which case unification is evaluated on the according body. The $mono("unify")$ function returns tuple $(Psi, r, u, b)$. The first element is a set $Psi$ of hypotheses corresponding to the newly introduced binder variables that were not reassigned during unification. The relation $r$ represents the relation over the successful unification and is typically the relation used in $rho$. The term $u$ is the term that was made equal through unification, typically the right-hand side of $rho$. The last argument $b$ is a boolean value that is `true` when unification succeeded and is `false` otherwise. The modified version $mono("unify"^"*")_rho (t)$ has the same behaviour but tries unification on all subterms and succeeds if at least one unification does @sozeau:inria-00628904.
 
-#pagebreak()
-
 == Proof Strategies for Rewriting
 
 We mentioned that every rewrite must be justified by a proof and the rewrite tactic must provide that proof. When we want to prove a goal $P space t : mono("Prop")$ where the function $P : alpha -> mono("Prop")$ is applied to the argument $t : alpha$ and we have a hypothesis $h$ of type $r space t space u$ given $r$ is a relation $alpha arrow alpha arrow mono("Prop")$, we can prove a rewrite from $t$ to $u$ given we have the additional information that $P$ is preserved by $r$. In order to generate a rewrite proof for that, $r$ must be an equivalence relation or lead to the implication relation ($<-$). Essentially, this means ($<-$) is a direct subrelation of $r$ or a transitive subrelation. When those hypotheses are in place, the proof is straight forward for this minimal example. By Lean's definition of subrelations, it suffices to show $r space (P space t) space ?_t$ and $?_t$. We can assign $?_t$ with $P space u$ can eventually proceed to obtaining a proof for the rewrite $P space t <- P space u$.

docs/conclusion.typ

@@ -9,4 +9,4 @@ Our custom extensible proof search does not find assignments for all constraints
 
 = Acknowledgements
 
-I would like to thank Jannis Limperg for his supervision and useful support with Lean 4 metaprogramming and assistance with making the automated proof search extensible. Furthermore I want to thank Matthieu Sozeau for his helpful comments about Coq's rewriting implementation on the Coq Zulip chat.
+I would like to thank Jannis Limperg for his supervision and useful support with the Lean 4 metaprogramming and assistance with making the automated proof search extensible. Furthermore, I would like to thank Matthieu Sozeau for his helpful comments about Coq's rewriting implementation on the Coq Zulip chat.

docs/graph.typ

@@ -345,14 +345,14 @@ digraph G {
     G [label=<
         <TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0">
             <TR>
-                <TD WIDTH="10" HEIGHT="30">p</TD>
-                <TD WIDTH="10">
+                <TD WIDTH="20" HEIGHT="30">p</TD>
+                <TD WIDTH="20">
                     <TABLE BORDER="0" CELLBORDER="0" CELLSPACING="0">
                         <TR><TD HEIGHT="15">=</TD></TR>
                         <TR><TD HEIGHT="15">h</TD></TR>
                     </TABLE>
                 </TD>
-                <TD WIDTH="10">q</TD>
+                <TD WIDTH="20">q</TD>
             </TR>
             <TR>
                 <TD COLSPAN="3" HEIGHT="10">&#936; := {}</TD>
@@ -387,14 +387,14 @@ digraph G {
     K [label=<
         <TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0">
             <TR>
-                <TD WIDTH="10" HEIGHT="30">p</TD>
-                <TD WIDTH="10">
+                <TD WIDTH="20" HEIGHT="30">p</TD>
+                <TD WIDTH="20">
                     <TABLE BORDER="0" CELLBORDER="0" CELLSPACING="0">
                         <TR><TD HEIGHT="15">=</TD></TR>
                         <TR><TD HEIGHT="15">h</TD></TR>
                     </TABLE>
                 </TD>
-                <TD WIDTH="10">q</TD>
+                <TD WIDTH="20">q</TD>
             </TR>
             <TR>
                 <TD COLSPAN="3" HEIGHT="5">&#936; := {}</TD>

docs/main.typ

@@ -15,10 +15,6 @@
   supervisor: "Prof. Dr. Jasmin Blanchette"
 )
 
-#show heading: set block(below: 1.5em, above: 2em)
-
-#show figure: set block(below: 1.5em, above: 2em)
-
 #set page(numbering : "1")
 
 #counter(page).update(1)

docs/template.typ

@@ -21,7 +21,6 @@
   inset: (x: 1.2em, top: 1em)
 )
 
-
 #let example = thmplain("example", "Example").with(number: none)
 #let proof = thmproof("proof", "Proof").with(number: none)
 
@@ -53,7 +52,6 @@
 
   body
 }
-
 #let notes(
   title: "Some Notes",
   author: "Florian Würmseer",
@@ -143,12 +141,26 @@
   v(5%)
 
   pagebreak()
+show heading: set block(below: 1.5em, above: 2em)
+
+show figure: set block(below: 1.5em, above: 2em)
+[
+#show heading.where(level: 1): set heading(numbering: none)
+= Abstract
+
+Rewriting is a crucial concept for both automated and interactive theorem proving. The Coq theorem prover is prominent for its implementation of generalised rewriting that can rewrite with equivalence relations but also just symmetric or transitive relations. In this thesis, we aim to reconstruct and document the algorithm for generalised rewriting that is deeply embedded in Coq’s core modules to reveal the valuable and previously undocumented optimisations that enhance the efficiency of rewriting in Coq. We want to present a general algorithm specification that can easily be reimplemented in any theorem prover to rewrite with relations other than equality and bi-implication. To demonstrate the algorithm specification, we implemented this algorithm in the Lean 4 theorem prover which previously did not have a tactic for generalised rewriting. We verified that our algorithm produces the same proofs for rewrites as mentioned in previous research. Further improvements to the user experience such as solving all constraints generated by the algorithm prior to the user encountering them would be required to simplify a considerable amount of Lean's mathematics library with that tactic.]
+
+pagebreak()
 
   if show-outline {
     show outline.entry: it => {
-      if it.body() != [Acknowledgements] {
+      if it.body() == [Acknowledgements] {
+        return []
+      } else if it.body() == [Abstract] {
+        return []
+      } else {
         return it
-      } else []
+      }
     }
 
     outline()

docs/updated-algorithm.typ

@@ -3,6 +3,7 @@
 #import "./theme.typ": *
 #import "./graph.typ": *
 
+#pagebreak()
 = Optimised Algorithm for Rewriting
 
 We have seen five improvements to the `Rew` algorithm for constraint and proof generation of a rewrite. We will now propose an updated algorithm that combines all mentioned optimisations. This roughly resembles the algorithm that has evolved in the Coq core library over the last decade by combining the algorithms for Leibniz Equality rewriting, rewriting under binders, generalised rewriting, and the `setoid_rewrite` module.
@@ -19,7 +20,7 @@ If the rewrite does not occur in the rewrite function of the topmost application
 
 Once we start iterating over non-identity arguments, we collect the recursive proofs and carrier relation types retrieved in line 18 in the variables named `proofs` and `types`. Both of those variables in line 13 represent lists. Whenever we reach recursive identity rewrites after successfully rewriting at least one argument, we create `ProperProxy` metavariables as mentioned in the last section. We explicitly extend the constraint set $Psi$ by the relation and proof metavariables of the identity rewrites. In the case of successful rewrites, we already obtained the constraint set $Psi''$ which contains $r_i$ and $p_i$ at this point.
 
-Finally, all collected types and proofs can be applied to the `Proper` metavariable $?p : mono("Proper") ("types[0]" ==> dots ==> "types[len(types) - 1]" ==> r) mono("fn")$ to generate the rewrite proof. Note that $mono("proofs[0]")$ does not neccessarily refer to the first rewrite, and `fn` does not neccessarily refer to the argument $e_0$ in case there were identity rewrites. In this algorithm, we also use the simplified notation of metavariable application in which we refer to the only constructor `Proper.proper`.
+Finally, all collected types and proofs can be applied to the `Proper` metavariable $?p : mono("Proper") ("types[0]" ==> dots ==> "types[len(types) - 1]" ==> r) mono("fn")$ to generate the rewrite proof. Note that $mono("proofs[0]")$ does not neccessarily refer to the first rewrite, and `fn` does not neccessarily refer to the argument $e_0$ in case there were identity rewrites.
 
 We mentioned cases where we cannot infer the relation and thus have to fall back on the use of `Subrelation`. This can happen in two cases. The first case is when we do not enter any match-arm because we immediately unify. In this case, our proof is merely the input theorem $rho$. The type of $rho$ is $r space t space u$ for a rewrite relation $r$, the initial term $t$, and the output term $u$. The desired relation in @subterm is thus unused, and we have to infer the implication for the final rewrite using a subrelation $mono("Subrelation") r space (<-)$.