chore: update headings

Author: FWuermse

docs/algorithm.typ

@@ -2,15 +2,15 @@
 #import "./template.typ": *
 #import "./theme.typ": *
 #import "@preview/algo:0.3.4": algo, i, d, comment, code
-= Simple Algorithm for Rewriting <PaperAlgo>
+= 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.
 
-== Lean Terms
+== Terms in Lean
 
 In this section we will clarify the terms goal, subgoal, Lean term, and constraint by explaining the nature of Lean expressions.
 
-A term (or expression) in Lean 4 can be represented as any of the following variants `const`, `sort`, `fvar`, `mvar`, `app`, `lam`, `bvar`, `forallE`, `letE`, `lit`, `mdata`, or `proj`. They each represent a unique constructor of Lean's expression (`Expr`) type:
+A term (or expression) in Lean 4 can be represented as any of the following variants `const`, `sort`, `fvar`, `mvar`, `app`, `lam`, `bvar`, `forallE`, `letE`, `lit`, `mdata`, or `proj`. They esentially corresponds to an extension of the simply typed λ-calculus @lambdacalc. Those variants each represent a unique constructor of Lean's expression (`Expr`) type:
 
 ```lean
 inductive Expr : Type where
@@ -43,15 +43,15 @@ Note that some constructors of the `Expr` type contain references to Expr itself
 - Expr.mdata is the expression for annotations.
 - Expr.proj is a more efficient notation for product types in Lean.
 
-Expressions of type `mvar` are the kind of Lean expressions that also represent the goals and subgoals that we want to prove. In Lean's tactic mode we always have one active main goal that we need to solve first. Metavariables are called existential variables in Coq and are a crucial part of the algorithm for generalised rewriting. The constraints we mentioned earlier are synonymous for metavariables. However, during the rewriting process, we usually inspect them prior to becoming goals for the user to solve.
+Expressions of type `mvar` are the kind of Lean expressions that also represent the goals and subgoals that we want to prove. In Lean's tactic mode we always have one active main goal that we need to solve first. Metavariables are called existential variables in Coq and are a crucial part of the algorithm for generalised rewriting. The constraints we mentioned earlier are synonymous for metavariables. However, during the rewriting process, we usually inspect them prior to becoming goals for the user to solve @metaprogrammingbook.
 
-Metavariables of a certain type $Gamma tack tau$ can be assigned with any value $Gamma tack e : tau$ in the context $Gamma$ (hypotheses, theorems, etc.). Both $Gamma$ and $tau$ are part of that metavariable. When we assign a metavariable that represents a goal, we also close the goal. Another way to leverage metavariables is to use them as placeholders in any given Lean term when the value is unknown at the time of creation. It is also possible to share a metavariable $?_x$ across multiple terms. Assigning such a metavariable with a value $v$ also assigns every occurrence of $?_x$ with $v$. Whenever we choose variable names starting with a question mark in this thesis, we refer to metavariables.
+Metavariables of a certain type $Gamma tack tau$ can be assigned with any value $Gamma tack e : tau$ in the context $Gamma$ (hypotheses, theorems, etc.). Both $Gamma$ and $tau$ are part of that metavariable. When we assign a metavariable that represents a goal, we also close the goal. Another way to leverage metavariables is to use them as placeholders in any given Lean term when the value is unknown at the time of creation. It is also possible to share a metavariable $?_x$ across multiple terms. Assigning such a metavariable with a value $v$ also assigns every occurrence of $?_x$ with $v$. Whenever we choose variable names starting with a question mark in this thesis, we refer to metavariables @metaprogrammingbook.
 
-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 @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 `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.
+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 `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 Strategy for Rewriting
+== 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")$ and 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 imply 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$.
 
@@ -194,7 +194,7 @@ algo(
   return ?s t u p
 ], caption: [Algorithm for relation inference.]) <infersub>
 
-== Example <examplesection>
+#example("Simple Rewrite") <examplesection>
 
 To demonstrate an example where we can see multiple different subterms but still keep an overview over the generated constraints, we choose a rather untypical rewrite. We want to rewrite a proposition in a conjunction using bi-implication. The algorithm rewrites $p and q$ to $q and q$ for a given relation $r$ that is a subrelation of $(<-)$ and a given proof $h : r space p space q$. The algorithm first tries to unify the entire term $p and q$ with the left-hand side of our proof ($p$). Conjunctions in Lean are defined by the `And` structure. Thus, our term $t$ is interpreted as $mono("And") p space q$ which must be read as $(mono("And") space p) space q$. This falls into the `app` case such that we first interpret $(mono("And") p)$ followed by $q$. Again the term $(mono("And") p)$ doesn't unify with $p$, and the algorithm follows another `app` iteration for the terms `And` and $p$. `And` itself does not unify and does not match any other category. Therefore, the algorithm treats it as an atom (`const`) and generates a metavariable $?_(mono("And")_r) : mono("relation") (mono("relation Prop"))$ and passes ($?_(mono("And")_m) : mono("Proper") (mono("relation") mono("Prop")) space ?_(mono("And")_r) mono("And")$) for the proof of identity. The next term we consider, $p$, does indeed unify with $p$ and is therefore replaced with $q$. For now, the return value for the proof will be just $h$. After the two recursive `Rew`-invocations terminate, we combine the proofs and carrier relations for a proof of $r space (mono("And") space p) space (mono("And") space q)$. We start with another hole $?_(mono("And")_p) : "Subrelation" ?_(mono("And")_r) (r ==> (?_T : "relation (Prop" -> "Prop)"))$. Recall that `Subrelation` is a typeclass with only constructor `subrelation`. Thus, any metavariable of type `Subrelation` must be of that constructor and eventually unfolds to $forall r_1 space r_2, ?_"rel" space r_1 space r_2 -> forall x space y, r space x space y -> ?_T space x space y -> ?_T (r_1 space x) space (r_2 space y)$. This allows us to construct the desired proof by carefully applying the arguments $?_(mono("And")_p) mono("And") mono("And") space ?_(mono("And")_m) space p space q space h$. By instantiating $r_1$ and $r_2$ with the `And` relation and $x$ and $y$ with $p$ and $q$, we receive our desired rewrite proof for this part of the term $?_(mono("And")_T) $.
 

docs/main.typ

@@ -21,6 +21,7 @@
 #set page(numbering : "1")
 
 #counter(page).update(1)
+#set cite(style: "institute-of-physics-numeric")
 
 #include "introduction.typ"
 

docs/optimisations.typ

@@ -3,11 +3,11 @@
 
 #pagebreak()
 
-= Optimised Algorithm for Rewriting
+= Algorithm Optimisations
 
 The actual Coq implementation of generalised rewriting contains a few optimisations that were not mentioned in the paper or documentation. Through reverse engineering a large amount of the Coq core module, we were able to extract the most crucial optimisations and applied them to our imperative algorithm specification. Thus, we represent the first complete documentation of the Coq's implementation for generalised rewriting in this chapter. The algorithm we have seen so far stresses the rewriting of applications and aims to convert other terms into application terms. Therefore, most of the following optimisations focus on simplifying rewrite proofs for application terms.
 
-== Identity and Success Status <idsuccstatus>
+== Status for Identity Rewrites <idsuccstatus>
 
 In our examples, we saw that many terms do not contain the left-hand side term of the rewrite theorem $rho$. However, we would still examine those terms and produce two metavariables just to create a proof of identity $h : t <- t$. This can be simplified by classifying subterms depending on whether they can be directly or recursively rewritten or remain the same. We change the output type of the algorithm to a sum type with two variants. The `identity` variant carries no further information and signals that a term cannot be rewritten. The other variant `success` carries the same information as seen before, in essence, the carrier relation, the updated term, and the proof of the rewrite. Now every time all the recursive invocations result in identity rewrites, the current rewrite will also be an identity rewrite. For instance, when both recursive calls $"Rew"_rho (Psi, f)$ and $"Rew"_rho (Psi, e)$ of an application $f space e$ result in identity rewrites, then the result for $"Rew"_rho (Psi, f space e)$ will also result in an identity rewrite. When considering a term $q and q and p and q and q$ given $h : p <-> q$, we would only consider the $p$ in the middle and would not create proofs and nested carrier relations for the four conjunction atoms and the four $q$s. The worst case complexity is still the same here. However, in practice, we usually have many cases that cannot be rewritten especially as we indirectly transform non-dependent function and Pi types to identity applications as well.
 
@@ -19,7 +19,7 @@ Let us consider a simple rewrite of an application $f space e$ where $e$ can be
 
 For this optimisation to work, however, we still have to create metavariables whenever the desired relation changes. This happens when we break the term $t$ further down. For instance, when recursively rewriting a function argument, its type is different from the type of the whole application. In that case, we create a metavariable of the given type and pass it down. In some cases, we cannot leverage the provided relation and have to fall back on at most one final subrelation inference. For instance, this can happen when the input term directly unifies and returns without creating any constraints.
 
-== Applications as Sequence
+== Function Applications as Sequence
 
 When introducing the `Proper` and `respectful` definitions, we gave an example for a possible rewrite proof of $p and q -> q and q$ using $mono("Proper") ((=) ==> (<->) ==> (<-)) space (and)$. This is a very compact proof for such a rewrite. However, the above algorithm would not be able to directly produce a respectful chain with three arguments due to the fact that applications are treated as binary applications and thus result in no more than one respectful arrow $(==>)$ wrapped in subrelations. This can be improved by considering the entire sequence of applications. This helps us to simplify the two `Proper` proofs connected with a `Subrelation` proof that we have seen for the $p and q -> q and q$ rewrite (See @examplesection) to a single proper instance with two arrows. In combination with using a `success`/`identity` status, this gives us more context for an entire sequence of applications. For instance, we know that the entire application is an `identity` rewrite by iterating over the function and each argument. In that case, we ultimately just return `identity`. We can also use this in combination with the top-down approach for relation passing to insert the desired implication for a specific rewrite (e.g., $(<-$)) at the end and the relation $r$ representing the rewrite argument as the source. Such a proof for $mono("Proper") (r ==> dots ==> (<-)) space (f : mono("Prop") -> dots -> mono("Prop"))$ leads directly to the desired right-to-left implication and does not require a final subrelation over the outcome of $mono("Rew"_rho) (Psi, f space e_0 space dots space e_n, r)$.
 

docs/proof.typ

@@ -1,8 +1,9 @@
 #import "./template.typ": *
 #import "./theme.typ": *
-= Equality of the Generated Proofs
 
-We saw that, in the typical case, the improved algorithm generates significantly fewer constraints and leads to more concise proofs. In the following, we want to show that the two proposed algorithms for constraint generation `Rew` and `ORew` provide the same rewrite proofs although with different metavariables.
+= Equivalence of the Generated Rewrite Proofs
+
+We saw that, in the typical case, the improved algorithm generates significantly fewer constraints and leads to more concise proofs. In the following, we want to show that the two proposed algorithms for constraint generation `Rew` and `ORew` provide the same rewrite proofs although with different constraints. The constraints still consist of metavariables of the types `relation`, `pointwiseRelation`, `Subrelation`, and `Proper` but in a more consise way.
 
 #theorem()[When the algorithm $mono("Rew")_rho (t : tau)$ provides a proof for $?_r space t space u$ where $?_r$ is of type $mono("relation") space tau$ and $t != u$ for any given $tau$ and $rho$, then the modified algorithm $mono("ORew")_rho (t, ?_r)$ provides either *(1)* a proof for $?_r space t space u$ if the relation inference $?_r$ succeeds (see @updatedalgo) or *(2)* otherwise a proof of $?_r' space t space u$ where $?_r' : mono("relation" space tau)$ is a fresh metavariable of the same type $mono("relation") space tau$. If $t = u$, the $mono("ORew")$ algorithm with the same arguments returns just the flag `identity` whereas the $mono("Rew")$ algorithm provides a proof $p : ?_r space t space t$ *(3)*.] <theorem1>
 
@@ -93,7 +94,7 @@ We saw that, in the typical case, the improved algorithm generates significantly
     We must now also show that:\ $(Psi', r, e_0 ' space dots space e_(n+1) ', p : r space (e_0 space dots space e_(n+1)) space (e_0 ' space dots e_(n+1) ')) := mono("Rew"_rho) (e_0 space dots space e_(n+1) ')$ implies:\
     $(Psi'', r', e_0 ' space dots space e_(n+1) ', p' : r' space (e_0 space dots space e_(n+1)) space (e_0 ' space dots space e_(n+1) ')) := mono("ORew"_rho) (e_0 space dots space e_(n+1), r)$ \ if $e_0 space dots space e_(n+1) != e_0 ' space dots space e_(n+1) '$ and $(Psi'', mono("identity")) := mono("ORew"_rho) (e_0 space dots space e_(n+1), r)$ otherwise.
 
-    There are four cases for the inductive step. Given the previous sequence was an identity rewrite, we must divide between another identity rewrite or a successful rewrite. If the previous sequence contains at least one successful rewrite, we also have the scenarios of another rewrite or a final identity. This differentiation is crucial to align with the Leading Identity Rewrite and the Identity and Success Status optimisations.
+    There are four cases for the inductive step. Given the previous sequence was an identity rewrite, we must divide between another identity rewrite or a successful rewrite. If the previous sequence contains at least one successful rewrite, we also have the scenarios of another rewrite or a final identity. This differentiation is crucial to align with the optimisations for Leading Identity Rewrites and Status for Identity Rewrites.
 
   - *Case $e_0 space dots space e_n space e_(n+1)$ where we rewrote $e_0 space dots space e_n$ and $e_(n+1)$ unifies with $rho_"lhs"$*