Skip to content

Commit

Permalink
Change ref to cref
Browse files Browse the repository at this point in the history
  • Loading branch information
@vikraman
vikraman committed Feb 29, 2024
1 parent 58c6205 commit 2369024
Show file tree
Hide file tree
Showing 8 changed files with 43 additions and 43 deletions.
18 changes: 9 additions & 9 deletions papers/icfp24/formalization.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,15 @@ \section{Formalization}
\begin{tabular}{lll}
\hline
\textbf{Code} & \textbf{Description} & \textbf{Reference} \\ \hline
\texttt{Cubical.Structures.Free} & Free algebras & (Section~\ref{sec:universal-algebra}) \\
\texttt{Cubical.Structures.Set.Mon.List} & $\term{List}$ & (Section~\ref{mon:lists}) \\
\texttt{Cubical.Structures.Set.Mon.Array} & $\term{Array}$ & (Section~\ref{mon:array})\\
\texttt{Cubical.Structures.Set.CMon.QFreeMon} & Quotiented-free monoid & (Section~\ref{cmon:qfreemon}) \\
\texttt{Cubical.Structures.Set.CMon.PList} & Quotiented-list & (Section~\ref{cmon:plist}) \\
\texttt{Cubical.Structures.Set.CMon.SList} & Swapped-list & (Section~\ref{cmon:slist}) \\
\texttt{Cubical.Structures.Set.CMon.Bag} & Bag & (Section~\ref{cmon:bag}) \\
\texttt{Cubical.Structures.Set.CMon.SList.Sort} & Sort and order relationship & (Section~\ref{sec:sorting}) \\
\texttt{Cubical.Structures.Set.CMon.SList.Sort.Equiv} & Sort and order equivalence & (Section~\ref{sort:main}) \\
\texttt{Cubical.Structures.Free} & Free algebras & (Section~\cref{sec:universal-algebra}) \\
\texttt{Cubical.Structures.Set.Mon.List} & $\term{List}$ & (Section~\cref{mon:lists}) \\
\texttt{Cubical.Structures.Set.Mon.Array} & $\term{Array}$ & (Section~\cref{mon:array})\\
\texttt{Cubical.Structures.Set.CMon.QFreeMon} & Quotiented-free monoid & (Section~\cref{cmon:qfreemon}) \\
\texttt{Cubical.Structures.Set.CMon.PList} & Quotiented-list & (Section~\cref{cmon:plist}) \\
\texttt{Cubical.Structures.Set.CMon.SList} & Swapped-list & (Section~\cref{cmon:slist}) \\
\texttt{Cubical.Structures.Set.CMon.Bag} & Bag & (Section~\cref{cmon:bag}) \\
\texttt{Cubical.Structures.Set.CMon.SList.Sort} & Sort and order relationship & (Section~\cref{sec:sorting}) \\
\texttt{Cubical.Structures.Set.CMon.SList.Sort.Equiv} & Sort and order equivalence & (Section~\cref{sort:main}) \\
\hline
\end{tabular}
\caption{Status of formalised results}
Expand Down
26 changes: 13 additions & 13 deletions papers/icfp24/free-commutative-monoids.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -143,8 +143,8 @@ \subsection{Lists quotiented by permutation}\label{cmon:plist}
\end{code}
\end{definition}

We have already given a proof of $\List$ being the free monoid in~\ref{mon:lists}.
By~\ref{cmon:qfreemon} it suffices to show $\Perm$ satisfies the axioms of permutation relation
We have already given a proof of $\List$ being the free monoid in~\cref{mon:lists}.
By~\cref{cmon:qfreemon} it suffices to show $\Perm$ satisfies the axioms of permutation relation
to show $\PList$ is the free commutative monoid.

It is trivial to see how $\Perm$ satisfies reflexivity, symmetry, transitivity.
Expand Down Expand Up @@ -190,7 +190,7 @@ \subsubsection{Representation}\label{plist:rep}
the function respects $\Perm$, i.e. $\Perm as\,bs \to f(as) = f(bs)$. This can be annoying because
of the many auxiliary variables in the constructor $\term{perm-swap}$, namely $xs$, $ys$, $zs$.
We need to show $f$ would respect a swap in the list anywhere between $xs$ and $ys$, which can
unnecessarily complicate the proof. For example in the inductive step of~\ref{plist:sharp-sat},
unnecessarily complicate the proof. For example in the inductive step of~\cref{plist:sharp-sat},
$\ext{f}((z :: zs)\,\doubleplus\,x :: y :: ys) = \ext{f}([ z ]) \mult \ext{f}(zs\,\doubleplus\,x :: y :: ys)$,
to actually prove this in Cubical Agda would involve first applying associativity to prove
$(z :: zs)\,\doubleplus\,x :: y :: ys = z :: (zs\,\doubleplus\,x :: y :: ys)$, before we can actually
Expand Down Expand Up @@ -248,7 +248,7 @@ \subsection{Swap-List}\label{cmon:slist}
\end{theorem}

\begin{proof}
By induction on $xs$ we can iteratively apply~\ref{slist:cons} to move all elements of $xs$
By induction on $xs$ we can iteratively apply~\cref{slist:cons} to move all elements of $xs$
to after $ys$. This would move $ys$ to the head and $xs$ to the end, thereby proving
$xs \doubleplus ys = ys \doubleplus xs$.
\end{proof}
Expand All @@ -257,7 +257,7 @@ \subsubsection{Representation}\label{slist:rep}
Much like $\PList$ and $\List$, $\SList$ is inductively defined, therefore making it very intuitive to reason
with when defining inductive operations or inductive proofs on $\SList$, however difficult to reason with
when defining operations that involve arbitrary partitioning, for reasons similar to those given
in~\ref{plist:rep}.
in~\cref{plist:rep}.

Unlike $\PList$ which is defined as a set quotient, this is defined as a HIT, therefore handling equalities
between $\SList$ is much simpler than $\PList$. We would still need to prove a function $f$ respects
Expand Down Expand Up @@ -292,8 +292,8 @@ \subsection{Bag}\label{cmon:bag}
Note that by the pigeonhole principle, $\sigma$ can only be constructed when $n = m$. Conceptually,
we are quotienting array by a permutation or an automorphism on the index.

We have already given a proof of $\Array$ being the free monoid in~\ref{mon:array}.
By~\ref{cmon:qfreemon} it suffices to show $\approx$ satisfies the axioms of permutation relation
We have already given a proof of $\Array$ being the free monoid in~\cref{mon:array}.
By~\cref{cmon:qfreemon} it suffices to show $\approx$ satisfies the axioms of permutation relation
to show $\Bag$ is the free commutative monoid.

\begin{proposition}
Expand Down Expand Up @@ -450,10 +450,10 @@ \subsection{Bag}\label{cmon:bag}
\item On $n = S(m)$,
\begin{align*}
& \ext{f}(S(m), i \circ \phi) \\
& = \ext{f}(S(m), i \circ \tau) & \text{by~\ref{bag:tau}} \\
& = \ext{f}(S(m), i \circ \tau) & \text{by~\cref{bag:tau}} \\
& = f(i(\tau(0))) \mult \ext{f}(m, i \circ \tau \circ S) & \text{by definition of $\ext{(\blank)}$} \\
& = f(i(0)) \mult \ext{f}(m, i \circ \tau \circ S) & \text{by construction of $\tau$} \\
& = f(i(0)) \mult \ext{f}(m, i \circ S \circ \psi) & \text{by~\ref{bag:punch}} \\
& = f(i(0)) \mult \ext{f}(m, i \circ S \circ \psi) & \text{by~\cref{bag:punch}} \\
& = f(i(0)) \mult \ext{f}(m, i \circ S) & \text{induction} \\
& = \ext{f}(S(m), i) & \text{by definition of $\ext{(\blank)}$}
\end{align*}
Expand All @@ -463,13 +463,13 @@ \subsection{Bag}\label{cmon:bag}
\subsubsection{Representation}\label{bag:rep}
Unlike $\PList$ and $\SList$, $\Bag$ and its underlying construction $\Array$ are not inductively defined,
making it difficult to work with when trying to do induction on them. For example,
in the proof~\ref{array:univ}, two lemmas~\ref{array:eta-suc} and~\ref{array:split} are needed to do
in the proof~\cref{array:univ}, two lemmas~\cref{array:eta-suc} and~\cref{array:split} are needed to do
induction on $\Array$, as opposed to $\List$ and its quotients, where we can do induction simply by
pattern matching. Much like $\PList$, when defining functions on $\Bag$, we need to show they respect
$\approx$, i.e. $as \approx bs \to f(as) = f(bs)$. This is notably much more difficult than
$\PList$ and $\SList$, because whereas with $\PList$ and $\SList$ we only need to consider "small permutations"
(i.e. swapping adjacent elements), with $\Bag$ we need to consider all possible permutations. For example,
in the proof of~\ref{bag:perm-sat}, we need to first construct a $\tau$ which satisfies $\tau(0) = 0$ and prove
in the proof of~\cref{bag:perm-sat}, we need to first construct a $\tau$ which satisfies $\tau(0) = 0$ and prove
$\ext{f}(n, i \comp \sigma) = \ext{f}(n, i \comp \tau)$ before we can apply induction.

Also, on a more technical note, since $\Array$ and $\Bag$ are not simple data types, the definition of
Expand All @@ -483,7 +483,7 @@ \subsubsection{Representation}\label{bag:rep}
However, performing arbitrary partitioning with $\Array$ and $\Bag$ is much easier than
$\List$, $\SList$, $\PList$. For example,
one can simply use the combinator $\Fin[n+m] \xto{\sim} \Fin[n] + \Fin[m]$ to partition the array,
then perform operations on the partitions such as swapping in~\ref{bag:comm},
or perform operations on the partitions individually such as two individual permutation in~\ref{bag:cong}.
then perform operations on the partitions such as swapping in~\cref{bag:comm},
or perform operations on the partitions individually such as two individual permutation in~\cref{bag:cong}.
This makes it such that when defining divide-and-conquer algorithms such as merge sort,
$\Bag$ and $\Array$ are more natural to work with than $\List$, $\SList$, and $\PList$.
12 changes: 6 additions & 6 deletions papers/icfp24/free-monoids.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ \section{Construction of Free Monoids}
(fold) operation.
%
Using fold allows us to structure our programs in an elegant way, and also exploit the properties of homomorphisms,
which is used in~\ref{sec:combinatorics}.
which is used in~\cref{sec:combinatorics}.

\subsection{Lists}
\label{mon:lists}
Expand Down Expand Up @@ -346,7 +346,7 @@ \subsection{Array}\label{mon:array}
We can do so by induction on $xs$.

Case $(0, g)$:
We have $g = \lambda\{\}$ by~\ref{array:zero-is-id}.
We have $g = \lambda\{\}$ by~\cref{array:zero-is-id}.
$\ext{f}((0, \lambda\{\}) \doubleplus ys) = \ext{f}(ys)$ by left unit,
and $\ext{f}(0, \lambda\{\}) \mult \ext{f}(ys) = e \mult \ext{f}(ys) = \ext{f}(ys)$
by definition of $\ext{(\blank)}$. Therefore,
Expand All @@ -358,7 +358,7 @@ \subsection{Array}\label{mon:array}
& = \ext{f}(S(n + m), g \oplus h) & \text{by definition of concatenation} \\
& = f((g \oplus h)(0)) \mult \ext{f}(n + m, (g \oplus h) \comp S) & \text{by definition of $\ext{(\blank)}$} \\
& = f(g(0)) \mult \ext{f}(n + m, (g \oplus h) \comp S) & \text{by definition of $\oplus$, and $0 < S(n)$} \\
& = f(g(0)) \mult \ext{f}((n, g \comp S) \doubleplus (m, h)) & \text{by~\ref{array:split}} \\
& = f(g(0)) \mult \ext{f}((n, g \comp S) \doubleplus (m, h)) & \text{by~\cref{array:split}} \\
& = f(g(0)) \mult (\ext{f}(n, g \comp S) \mult \ext{f}(m, h))) & \text{by induction} \\
& = (f(g(0)) \mult \ext{f}(n, g \comp S)) \mult \ext{f}(m, h)) & \text{by associativity} \\
& = \ext{f}(S(n), g) \mult \ext{f}(m, h)) & \text{by definition of $\ext{(\blank)}$} \\
Expand All @@ -376,7 +376,7 @@ \subsection{Array}\label{mon:array}
It is trivial to see $\ext{f} \comp \eta_A = f$ for all set functions $f : A \to X$.
To show $\ext{(f \comp \eta_A)} = f$ for all monoid homomorphism $f : \Array(A) \to \mathfrak{X}$,
we need to show $\forall xs.\, \ext{(f \comp \eta_A)}(xs) = f(xs)$.
Lemma \ref{array:eta-suc} and \ref{array:split} allow us to perform induction on arrays,
Lemma \cref{array:eta-suc} and \cref{array:split} allow us to perform induction on arrays,
therefore we can prove $\forall xs.\, \ext{(f \comp \eta_A)}(xs) = f(xs)$ by induction on $xs$,
very similarly to how this was proved for $\List$.
\end{proofsketch}
Expand All @@ -393,15 +393,15 @@ \subsection{Array}\label{mon:array}
We can do so by induction on $xs$.

Case $(0, g)$:
By~\ref{array:zero-is-id} we have $g = \lambda\{\}$.
By~\cref{array:zero-is-id} we have $g = \lambda\{\}$.
$\ext{(f \comp \eta_A)}(0, \lambda\{\}) = e$ by definition of the $\ext{(\blank)}$ operation,
and $f(0, \lambda\{\}) = e$ by homomorphism properties of $f$.
Therefore, $\ext{(f \comp \eta_A)}(0, g) = f(0, g)$.

Case $(S(n), g)$, we prove it in reverse:
\begin{align*}
& f(S(n), g) \\
& = f(\eta_A(g(0)) \doubleplus (n, g \comp S)) & \text{by~\ref{array:eta-suc}} \\
& = f(\eta_A(g(0)) \doubleplus (n, g \comp S)) & \text{by~\cref{array:eta-suc}} \\
& = f(\eta_A(g(0))) \mult f(n, g \comp S) & \text{by homomorphism properties of $f$} \\
& = (f \comp \eta_A)(g(0)) \mult \ext{(f \comp \eta_A)}(n, g \comp S) & \text{by induction} \\
& = \ext{(f \comp \eta_A)}(S(n), g) & \text{by definition of $\ext{(\blank)}$}
Expand Down
Binary file modified papers/icfp24/icfp24-sort-submission.pdf
View file
Binary file not shown.
Binary file modified papers/icfp24/icfp24-sort.pdf
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion papers/icfp24/introduction.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ \section{Introduction}
is that Cubical Type Theory allows us to enjoy the full power of univalence given by Homotopy Type Theory,
without losing canonicity and computational content of the proofs. This means that proofs and functions
transported by univalence actually compute!
We give a table of our formalization in~\ref{sec:formalization}.
We give a table of our formalization in~\cref{sec:formalization}.

% MOVE SOME OF THESE TO DISCUSSION AND OTHER SECTIONS

Expand Down
18 changes: 9 additions & 9 deletions papers/icfp24/sorting.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ \section{Total orders and Sorting}
\end{figure}

Since free commutative monoid is the quotient of free monoid by a permutation relation
(which we have proven in~\ref{cmon:qfreemon}), a section $s$ to $q$ would pick a canonical representation
(which we have proven in~\cref{cmon:qfreemon}), a section $s$ to $q$ would pick a canonical representation
out of the equivalence class generated by permutation.
Using $\SList$ as an example, $s(x :: y :: xs) = s(y :: x :: xs)$ for any $x, y : A$ and $xs : \SList(A)$,
and since it must also respect $\forall xs.\,q(s(xs)) = xs$, $s$ must preserve all content of $xs$,
Expand Down Expand Up @@ -60,7 +60,7 @@ \section{Total orders and Sorting}
We can easily construct such a section by any sorting algorithm. In our formalization we chose
insertion sort $\SList(A) \to \List(A)$ due to its inductive properties and simple definition.
However, if we want to define other sorting algorithms, e.g. merge-sort,
other representations such as $\Bag \to \Array$ would be more suitable as we have explained in~\ref{bag:rep}.
other representations such as $\Bag \to \Array$ would be more suitable as we have explained in~\cref{bag:rep}.
It is easy to see how this
proposition holds: $q(s(xs))$ orders an unordered list $xs$ by $s$, and re-discard the order again by
$q$, the act of imposing then forgetting an order on $xs$ does nothing, therefore $q(s(xs)) = xs$ holds.
Expand Down Expand Up @@ -143,7 +143,7 @@ \subsection{Order from section}
A section $s$ to $q$ satisfies $\isheadleast$ iff
$\forall x\, y\, xs.\, \issorted(x :: xs) \land y \in (x :: xs) \to \issorted([x,y])$.
\end{definition}
Here we use the definition of $\in$ from~\ref{comb:member}. Informally,
Here we use the definition of $\in$ from~\cref{comb:member}. Informally,
if we assume $s$ is a sort function, this states if
$x$ is the smallest element of a sorted list $ys$, then for any element $y \in ys$,
$[x, y]$ should be a sorted list. This ensures that $s$ would correctly sort 2-element lists.
Expand All @@ -155,7 +155,7 @@ \subsection{Order from section}
We use a weaker version of the axiom where $x :: xs$ is fixed to have length of 3.
We are given $x \preccurlyeq y$ and $y \preccurlyeq z$, we want to show $x \preccurlyeq z$.
Consider the 3-element $\{x,y,z\} : \MM(A)$. Let $u$ be $\term{least}(\{x,y,z\})$,
by~\ref{sort:head-least} and~\ref{sort:sort-to-order},
by~\cref{sort:head-least} and~\cref{sort:sort-to-order},
we have $u \preccurlyeq x \land u \preccurlyeq y \land u \preccurlyeq z$.
Since $u \in \{x,y,z\}$, $u$ must be one of the element. We prove transitivity by case splitting.
If $u = x$ we have $x \preccurlyeq z$. If $u = y$ we have $y \preccurlyeq x$, and since
Expand Down Expand Up @@ -184,7 +184,7 @@ \subsection{Embedding of order into sections}
Let $\term{sort} : \MM(A) \to \LL(A)$ be insertion sort defined on $A$ by $\leq$.
We define $\term{sort}$ to be our section $s$ which satisfy $\isheadleast$.
It is trivial to see $\issortedany_{\term{sort}}([x, y])$ iff $x \leq y$ by the definition
of insertion sort. By~\ref{sort:sort-to-order} we can see $x \preccurlyeq y$ iff $x \leq y$.
of insertion sort. By~\cref{sort:sort-to-order} we can see $x \preccurlyeq y$ iff $x \leq y$.
We now have a total order $x \preccurlyeq y$ equivalent to $x \leq y$.

To show $x \preccurlyeq y$ is also decidable, we need to show $A$ has decidable equality.
Expand Down Expand Up @@ -228,7 +228,7 @@ \subsection{Equivalence of order and sections}
s(\{2,3,1\}) & = [1, 3, 2] \\
s(\{2,3\}) & = [2, 3] \\
\end{align*}
By~\ref{sort:o2s2o} we can use $\term{sort}$ to construct $\preccurlyeq$ which would be
By~\cref{sort:o2s2o} we can use $\term{sort}$ to construct $\preccurlyeq$ which would be
equivalent to $\leq$. However, the $\preccurlyeq$ constructed by $s$ would also be equivalent
to $\leq$. This is because $s$ sorts 2-element list correctly, despite $s \neq \term{sort}$.
Since two different sections satisfying $\isheadleast$ maps to the same total order,
Expand Down Expand Up @@ -280,7 +280,7 @@ \subsection{Equivalence of order and sections}
From $s$ we can construct a decidable total order $\preccurlyeq$ since $s$ satisfies
$\isheadleast$ and $A$ has decidable equality by assumption.
We construct $t$ as insertion sort parameterized by $\preccurlyeq$ constructed from $s$.
By~\ref{sort:sort-uniq} it remains to show $\forall xs.\,\term{Sorted}_{\preccurlyeq}(s(xs))$.
By~\cref{sort:sort-uniq} it remains to show $\forall xs.\,\term{Sorted}_{\preccurlyeq}(s(xs))$.
For lists of length 0 and 1 this is trivial. For further cases we need to prove by induction:
given a $xs : \MM(A)$ of length $\geq 2$, let $s(xs) = x :: y :: ys$. We need to show
$x \preccurlyeq y \land \term{Sorted}_{\preccurlyeq}(y :: ys)$ to construct
Expand Down Expand Up @@ -314,8 +314,8 @@ \subsection{Equivalence of order and sections}
is an equivalence.
\end{theorem}
\begin{proof}
By~\ref{sort:o2s2o} we show a decidable total order on $A$ implies a sort function
By~\cref{sort:o2s2o} we show a decidable total order on $A$ implies a sort function
on $A$ and that $A$ has decidable equality.
By~\ref{sort:s2o2s} we show a sort function on $A$ assuming $A$ has decidable equality
By~\cref{sort:s2o2s} we show a sort function on $A$ assuming $A$ has decidable equality
implies a decidable total order on $A$.
\end{proof}
Loading

0 comments on commit 2369024

Please sign in to comment.