fix: section names

Author: FWuermse

docs/algorithm.typ

@@ -4,13 +4,7 @@
 
 As mentioned in @Introduction, we implemented both the `Rew` and the `ORew` algorithms in Lean 4 and compared the resulting constraints.
 
-Our implementation aligns closely with the algorithms seen in @rewalgo and @subterm. To keep track of which side of a rewrite theorem needs to unify, we carry along a variable for the direction mentioned in @PaperAlgo that we call `l2r`. This variable provides the context of which subterm of a rewrite theorem $rho : r space l space r$ must unify inside the unification function. The choice between $(<-)$ and $(->)$ is directed by the desired relation $r$ mentioned in @subterm. We also had to implement more logic for deeply nested rewrites of a function $f$ at the beginning of an application sequence. While the rewriting in Coq can usually recursively rewrite all occurrences of the respective left-hand side or right-hand side of a rewrite theorem, it is not able to do that on functions.
-
-In order to rewrite the function of an application in Coq, we have to define the according subrelation, pointwise relation, and relation constraints. Consider a rewrite theorem $rho : r space f space g$. $f$ and $g$ are of type $alpha -> mono("Prop") -> beta -> mono("Prop")$. Rewriting $f$ to $g$ in a term $f space a space (a = a) space b$ where $a$ is of type $alpha$ and $b$ of type $beta$ in Coq, the algorithm provides a proof e.g. with $(<-)$ as the desired relation for $f space a space (a = a) space b <- g space a space (a = a) space b$. In our `ORew` algorithm, we would enter the path starting at line 8 in @subterm and produce the according proof. However, when changing the term to $f space a space (f space a space (a = a) space b) space b$, Coq currently only provides a proof for $f space a space (f space a space (a = a) space b) space b <- g space a space (f space a space (a = a) space b) space b$. We can see that only the outer $f$ is rewritten by Coq's implementation, but the inner $f$ is unchanged. In the special case where $r$ is equality, Coq applies the algorithm for Leibniz Equality and replaces both occurrences of $f$.
-
-This inconsistency in the Coq implementation is a crucial difference to the `Rew` algorithm which would rewrite all occurrences of $f$ even when the relation is not equality. This is where we made some further changes to our by Coq-inspired `ORew` algorithm leveraging transitivity of implications (or open relations) as mentioned in @updatedalgo. As transitivity cannot be shown for possibly non-transitive rewrite relation $r$, we must perform a subrelation inference to the desired relation passed as argument to `ORew` immediately. This ensures that both terms are proofs over an identical relation which is required by the `Transitive` typeclass that we will need. When we operate on `Prop` directly, the inferred relation is either $(<-)$ or $(->)$ and therefore already transitive. In the other case, we are in a nested call of the application case and thus work with a metavariable of type $mono("relation " tau)$ that we can force to be transitive during the proof search. This does not change our invariants as we always treat relations general enough so that it does not matter whether we work with metavariables of type $mono("relation " tau)$ or given instances of that type.
-
-Once we inferred the relation to the desired transitive relation $r$, we can perform another rewrite on the updated term $u$. In the recursive call with $u$, the first occurrence was already replaced by $g$ and we follow the procedure for application arguments starting at line 13 in @subterm. This would invoke yet another recursive invocation where $f$ is again the function rewrite. This is how we can rewrite a term, for instance $f space a space (f space a space (f space a space (mono("True")) space b) space b) space b$, directly to $g space a space (g space a space (g space a space (mono("True")) space b) space b) space b$ and thus truly generate the same rewrites that `Rew` produces. The downside of this approach is that with many occurrences of $f$, we generate almost as many `Subrelation` metavariables as the `Rew` algorithm would for this example. The `Transitive` instances, however, are trivial to solve and can even be closed during the constraint generation as all implications are transitive.
+Our implementation aligns closely with the algorithms seen in @rewalgo and @subterm. To keep track of which side of a rewrite theorem needs to unify, we pass along a variable of type boolean for the direction mentioned in @PaperAlgo that we call `l2r`. This variable provides the context of which subterm of a rewrite theorem $rho : r space l space r$ must unify inside the unification function. The choice between $(<-)$ and $(->)$ is directed by the desired relation $r$ mentioned in @subterm. We also had to implement more logic compared to Coq's rewriting implementation for deeply nested rewrites of a function $f$ at the beginning of an application sequence. While the rewriting in Coq can usually recursively rewrite all occurrences of the respective left-hand side or right-hand side of a rewrite theorem, it is not able to do that on functions. By enabling our `ORew` algorithm to be fully consistant with `Rew` we had to support that feature that Coq does not support.
 
 It is a common use case to perform rewrites using existing theorems such as addition commutativity or `Nat.add_comm` ($forall n space m : NN, n + m = m + n$) or `Nat.right_distrib` ($forall n space m space k : NN, (n+m) dot k = n dot k + m dot k$). Both of those theorems are defined with universal quantifiers. During the execution of the algorithm for constraint generation, we are looking for unifications of the term $n + m$ for $rho := mono("Nat.add_comm")$ assuming a left-to-right rewrite. That means we have to go inside the $forall$-binder every time. As this information does not change during the execution, we wrapped the algorithm in a reader monad containing all relevant information about the theorem in the context. This is the carrier relation $=$, the left-hand side of $rho$, the right-hand side of $rho$, the proof $rho$, and the possible metavariables for unused binder variables. Those unused binder variables eventually become goals for the user to solve and will not be affected by the proof search.
 

docs/implementation.typ

@@ -5,7 +5,7 @@
 
 Rewriting in theorem provers is the process of replacing a subterm $t$ of inside an expression with another term $u$. In Lean, rewriting is possible when the two terms are equal, $t = u$, or when the two terms are propositions and imply each other $p <-> q$. This allows us to replace a term in a goal we want to solve or inside one of our hypotheses when reasoning in Lean.
 
-We can use the `rewrite` tactic in Lean to show the that two natural numbers are still then same when we add zero on one side. Consider the example theorem $1 = 1 + 0$ that we want to prove. We also assume that we have a hypothesis that states $forall n : NN, n + 1 = n$. We can then perform a left-to-right rewrite. By that we mean replacing occurrences of the left-hand-side of the theorem ($n + 1$) in the proof-goal with the right-hand-side of that theorem. Using this rewrite, we can alter the original goal $1 = 1 + 0$ to $1 = 1$ because $1 + 0$ is an occurrence of our theorems left-hand-side. The following example represents the rewrite in Lean's syntax:
+We can use the `rewrite` tactic in Lean to show the that two natural numbers are still then same when we add zero to one side. Consider the example theorem $1 = 1 + 0$ that we want to prove. We also assume that we have a hypothesis that states $forall n : NN, n + 1 = n$. We can then perform a left-to-right rewrite. By that we mean replacing occurrences of the left-hand-side of the theorem ($n + 1$) in the proof-goal with the right-hand-side of that theorem. Using this rewrite, we can alter the original goal $1 = 1 + 0$ to $1 = 1$ because $1 + 0$ is an occurrence of our theorems left-hand-side. The following example represents the rewrite in Lean's syntax:
 
 #show raw.where(block: true): code => {
   show raw.line: line => {
@@ -30,14 +30,14 @@ This form of rewriting only helps us to replace terms that are equal in Lean's t
 
 Let us consider the example of an implementation of a mathematical set in Lean that lets us examine and compare set members. We could start by reusing Lean's lists for our sets. Unlike sets, lists can have duplicate elements and the order of elements matters. If we want to reason about the equality of two sets $s_1$ and $s_2$ we could not simply check for equality as seen before. If $s_1$ has three elements $[1, 1, 2]$ and $s_2$ has only two elements $[2, 1]$ they would not be considered equal in Lean, although they should represent two equal sets.
 
-In order to compare $l_1$ and $l_2$ as actual sets we have to define a custom relation for their equality:
+In order to compare $l_1$ and $l_2$ as actual sets we have to define a custom relation for their equivalence:
 
 ```lean
 def setEq {α : Type} : List α → List α → Prop :=
   λ l1 l2 ⇒ ∀ x, x ∈ l1 ↔ x ∈ l2
 ```
 
-This definition ensures that we now represent set equality correctly. We can even show that `setEq` is an equivalence relation by proving the identity, symmetry, and transitivity properties. We can continue and define a function to add elements `addElem` that appends an element to the underlying list of our set representation:
+This definition ensures that we now represent set equality correctly. We can even show that `setEq` is an equivalence relation by proving the identity, symmetry, and transitivity properties. We can proceed by defining a function to add elements `addElem` that appends an element to the underlying list of our set representation:
 
 ```lean
 instance set_eq_equivalence {α : Type} : Equivalence (@setEq α) where
@@ -60,11 +60,11 @@ def addElem {α : Type} (x : α) (l : List α) : List α :=
   x :: l
 ```
 
-Furthermore, we can show that addition of two equivalent sets preserves the equivalence. We also refer to this behaviour as morphism for `setEq`. The Lean proof for this is tedious however. The relation `setEq` is not the same as equality and can thus not be rewritten. This means we would have to prove that addition preserves the set equivalence for every element we may want to add. To solve a goal, for instance the implication $mono("setEq") [1, 1, 2] space [2, 1] -> mono("setEq") (mono("addElem" 3 space [1, 1, 2]) space (mono("addElem") 3 space [2, 1]))$. As we know that our addition of elements is a morphism for set equivalence, we would like to be able to rewrite just as we did with equality. To do this, we need generalised rewriting.
+Furthermore, we can show that addition of the same element to two equivalent sets preserves the equivalence. We also refer to this behaviour as morphism for `setEq`. The Lean proof for this is tedious however. The relation `setEq` is not the same as equality and can thus not be rewritten. This means we would have to prove that addition preserves the set equivalence for every element we may want to add. Let us consider the goal $mono("setEq") [1, 1, 2] space [2, 1] -> mono("setEq") (mono("addElem" 3 space [1, 1, 2]) space (mono("addElem") 3 space [2, 1]))$. As we know that our addition of elements is a morphism for set equivalence, we would like to be able to rewrite just as we did with equality. To do this, we need generalised rewriting.
 
 Generalised rewriting is the ability to replace subterm $t$ with $u$ when they are related by an equivalence relation $r$ other than equality and bi-implication @sozeau:inria-00628904. In Type Theory, homogeneous binary relations are terms of type $alpha -> alpha -> mono("Prop")$ where $alpha$ can be an arbitrary type and `Prop` is the type of propositions. Equality ($=$) is of type $alpha -> alpha -> mono("Prop")$ in Lean and the bi-implication ($<->$) is of type $mono("Prop") -> mono("Prop") -> mono("Prop")$. We will also refer to relation types of $alpha -> alpha -> mono("Prop")$ as $mono("relation") alpha$.
 
-With generalised rewriting we could solve the above example by replacing the occurrence of $[1, 1, 2]$ in the proof goal by the right-hand-side of the rewrite theorem $[2, 1]$. A Lean proof where generalised rewriting is supported with a tactic `grewrite` would look like the following:
+With generalised rewriting we could solve the above example by replacing the occurrence of $[1, 1, 2]$ in the proof goal by the right-hand-side of the rewrite theorem $[2, 1]$. Lean 4 has currently no support for generalised rewriting. A Lean proof where generalised rewriting was supported with a tactic `grewrite` would ideally look like the following:
 
 ```lean
 example : setEq [1,1,2] [2,1] → setEq (addElem 4 [1,1,2])  (addElem 4 [2,1]) := by
@@ -79,6 +79,6 @@ The already present tactic for rewriting with equality and bi-implication in Lea
 
 In this thesis, we will take a deeper look at the algorithm for generalised rewriting in type theory proposed by Mattheiu Sozeau @sozeau:inria-00628904, compare it to the actual implementation of generalised rewriting in Coq, extract the differences between the two, and show that those algorithms provide the same rewrite proofs. The algorithm described in the literature consists of two parts. The first part generates the rewritten term and proof of the rewrite including holes (or subgoals) that cannot be known when exploring a term. We also refer to this part of the algorithm as constraint generation algorithm, as it leaves some open constraints. The second part of the algorithm solves those open subgoals (or constraints) using a proof search. Throughout this thesis, we will pay more attention to the constraint generation and assert the generated proofs and constraints.
 
-Our contributions to the research include two implementations of generalised rewriting algorithms in Lean 4. The first one is a reimplementation of the literature version by Mattheiu Sozeau @sozeau:inria-00628904. The second implementation considers all improvements that have evolved in the Coq code base over the last two decades. Therefore, we provide the first description of the actual Coq rewriting algorithm including all those improvements. Those algorithms follow same API as Lean's `rewrite` tactic. Our final contribution is an extension of the optimised Coq-inspired algorithm that makes the constraint generation more powerful than Coq's implementation and works for all cases described in the literature. This also includes a proof over the generated outputs of the algorithm. While our implementations generate the same proofs and constraints as the Coq's `rewrite` tactic does, our proof search is currently not as powerful as Coq's typeclass search. This may result in possible additional subgoals after performing certain rewrites.
+Our contributions to the research include two implementations of generalised rewriting algorithms in Lean 4. The first one is a reimplementation of the literature version by Mattheiu Sozeau @sozeau:inria-00628904. The second implementation considers all improvements that have evolved in the Coq code base over the last two decades. Therefore, we provide the first complete description of the actual Coq rewriting algorithm including all those improvements. Those implementations follow same API as Lean's `rewrite` tactic. Our final contribution is an extension of the optimised Coq-inspired algorithm that makes the constraint generation more powerful than Coq's implementation and works for all cases described in the literature. This also includes a proof over the generated outputs of the algorithm. While our implementations generate the same proofs and constraints as Coq's `rewrite` tactic does, our proof search, the second part of the generalised rewriting algorithm, is currently not as efficient as Coq's typeclass search. This may result in possible additional subgoals after performing certain rewrites.
 
-Notably, our Lean 4 implementation is the only rewriting library that achieves full consistency with Coq's constraint generation, making it the most reliable choice for formal proofs in Lean.
+Notably, our optimised implementation is the only generalised rewriting library for Lean 4 that achieves full consistency with Coq's constraint generation, making it the most reliable choice for formal proofs in Lean.