Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix pdf links #41

Merged
merged 5 commits into from
Jun 30, 2021
Merged

Fix pdf links #41

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
62f8c7f
update Definition to On_Generic
start974 Jun 4, 2021
931fffa
update on Omega link
start974 Jun 4, 2021
d583db9
fix link On_plus in pdf
start974 Jun 4, 2021
8d8188e
fix link in pdf
start974 Jun 29, 2021
69f5250
resolve mistakes
start974 Jun 30, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 27 additions & 27 deletions doc/chapter-powers.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ \section{Some basic implementations}


\emph{From Module
\href{../theories/html/hydras.additions.FirstSteps.html}{\texttt{additions.FirstSteps}}}
\href{../theories/html/additions.FirstSteps.html}{\texttt{additions.FirstSteps}}}
\label{sect: power-definitions}

\begin{Coqsrc}
Expand Down Expand Up @@ -155,7 +155,7 @@ \subsection{A logarithmic exponentiation function}
\vspace{4pt}

\emph{From Module
\href{../theories/html/hydras.additions.FirstSteps.html}{additions.FirstSteps}}
\href{../theories/html/additions.FirstSteps.html}{additions.FirstSteps}}


\begin{Coqsrc}
Expand Down Expand Up @@ -313,7 +313,7 @@ \subsection{Computing Fibonacci numbers}
In \coq{}, one can define this function by simple recursion.

\emph{From Library
\href{../theories/html/hydras.additions.Fib2.html}{additions.Fib2}}
\href{../theories/html/additions.Fib2.html}{additions.Fib2}}

\begin{Coqsrc}
Fixpoint fib (n:nat) : N :=
Expand Down Expand Up @@ -439,7 +439,7 @@ \subsubsection{Removing duplicate computations}


\emph{From Library
\href{../theories/html/hydras.additions.Fib2.html}{additions.Fib2}}
\href{../theories/html/additions.Fib2.html}{additions.Fib2}}

\emph{The \texttt{Monoid} type class is defined
page~\pageref{sect:monoid-def}.}
Expand Down Expand Up @@ -646,7 +646,7 @@ \subsection{A common notation for multiplication}
First, we associate a class to the notion of \emph{multiplication}
on any type $A$.

\emph{From Module \href{../theories/html/hydras.additions.Monoid_def.html}{additions/Monoid\_def.v}.}
\emph{From Module \href{../theories/html/additions.Monoid_def.html}{additions/Monoid\_def.v}.}

\begin{Coqsrc}
Class Mult_op (A:Type) := mult_op : A -> A -> A.
Expand Down Expand Up @@ -698,7 +698,7 @@ \subsubsection{Multiplication on Peano numbers}
this term is convertible with \texttt{Nat.mul 3 4}, as shown by the
interaction below.

\emph{From Module \href{../theories/html/hydras.additions.Monoid_def.html}{additions.Monoid\_def}}
\emph{From Module \href{../theories/html/additions.Monoid_def.html}{additions.Monoid\_def}}

\begin{Coqsrc}
Set Printing All.
Expand All @@ -723,7 +723,7 @@ \subsubsection{String concatenation}
\texttt{string\_op}.


\emph{From Module \href{../theories/html/hydras.additions.Monoid_def.html}{additions.Monoid\_def}}
\emph{From Module \href{../theories/html/additions.Monoid_def.html}{additions.Monoid\_def}}

\begin{Coqsrc}
Require Import String.
Expand Down Expand Up @@ -751,7 +751,7 @@ \subsection{The Monoid type class}
We are now ready to give a definition of the \texttt{Monoid} class, using
\texttt{*} as an infix operator in scope \coqscope{M} for the monoid multiplication.

The following class definition, from Module \href{../theories/html/hydras.additions.Monoid_def.html}{additions.Monoid\_def},
The following class definition, from Module \href{../theories/html/additions.Monoid_def.html}{additions.Monoid\_def},
is parameterized with some type $A$,
a multiplication (called \texttt{op} in the definition), and a neutral element
$\mathds{1}$ (called \texttt{one} in the definition).
Expand Down Expand Up @@ -779,7 +779,7 @@ \subsection{Building instances of \texttt{Monoid}}

Let us show various instances, which will be used in further proofs and examples.
Complete definitions and proofs are given in
File~\href{../theories/html/hydras.additions.Monoid_instances.html}{additions/Monoid\_instances.v}.
File~\href{../theories/html/additions.Monoid_instances.html}{additions/Monoid\_instances.v}.


\subsubsection{Monoid on \texttt{Z}}
Expand Down Expand Up @@ -961,7 +961,7 @@ \subsection{Monoids and equivalence relations}
\vspace{4pt}

\noindent
\emph{From Module \href{../theories/html/hydras.additions.Monoid_def.html}{additions.Monoid\_def}}
\emph{From Module \href{../theories/html/additions.Monoid_def.html}{additions.Monoid\_def}}

\begin{Coqsrc}
Class Equiv A := equiv : relation A.
Expand Down Expand Up @@ -1039,7 +1039,7 @@ \subsubsection{Coercion from Monoid to EMonoid}

%ici%

\emph{From Module \href{../theories/html/hydras.additions.Monoid_instances.html}{additions.Monoid\_instances}}
\emph{From Module \href{../theories/html/additions.Monoid_instances.html}{additions.Monoid\_instances}}

\begin{Coqsrc}
Check NMult : EMonoid N.mul 1%N eq.
Expand Down Expand Up @@ -1130,7 +1130,7 @@ \subsubsection{Example : Arithmetic modulo $m$}

\section{Computing powers in any EMonoid}

The module \href{../theories/html/hydras.additions.Pow.html}{additions.Pow} defines two functions for exponentiation on any
The module \href{../theories/html/additions.Pow.html}{additions.Pow} defines two functions for exponentiation on any
\texttt{EMonoid} on carrier $A$.
They are essentially the same as in Sect.~\vref{sect: power-definitions}. The main difference lies in the arguments of the functions, which now contain
an instance~\texttt{M} of class \texttt{EMonoid}.
Expand Down Expand Up @@ -1182,7 +1182,7 @@ \subsubsection{Examples of computation}

\vspace{4pt}

From Module~\href{../theories/html/hydras.additions.Demo_power.html}{additions.Demo\_power}
From Module~\href{../theories/html/additions.Demo_power.html}{additions.Demo\_power}



Expand Down Expand Up @@ -1218,7 +1218,7 @@ \subsection{The binary exponentiation algorithm}
% associated with equalities \ref{binary-eq4} to \ref{binary-eq6} and a main function \texttt{Pos\_bpow} associated with equalities \ref{binary-eq1} to \ref{binary-eq3}.

\vspace{4pt}
\emph{From Module~\href{../theories/html/hydras.additions.Pow.html}{additions.Pow}}
\emph{From Module~\href{../theories/html/additions.Pow.html}{additions.Pow}}

\begin{Coqsrc}
Fixpoint binary_power_mult `{M: @EMonoid A E_op E_one E_eq}
Expand All @@ -1244,7 +1244,7 @@ \subsection{The binary exponentiation algorithm}
natural numbers:

\vspace{4pt}
From Module~\href{../theories/html/hydras.additions.Pow.html}{additions.Pow}
From Module~\href{../theories/html/additions.Pow.html}{additions.Pow}

\begin{Coqsrc}
Definition N_bpow {A} `{M: @EMonoid A E_op E_one E_eq} x (n:N) :=
Expand Down Expand Up @@ -1273,7 +1273,7 @@ \subsection{Refinement and correctness}


\vspace{4pt}
From Module~\href{../theories/html/hydras.additions.Pow.html}{additions.Pow}
From Module~\href{../theories/html/additions.Pow.html}{additions.Pow}

\begin{Coqsrc}
Lemma N_bpow_ok :
Expand All @@ -1293,7 +1293,7 @@ \subsection{Refinement and correctness}

\subsection{Proof of correctness of binary exponentiation w.r.t. the function \texttt{power}}
Section \texttt{M\_given} of Module
~\href{../theories/html/hydras.additions.Pow.html}{additions.Pow} is devoted to the proof
~\href{../theories/html/additions.Pow.html}{additions.Pow} is devoted to the proof
of properties of the functions above.
Note that properties of \texttt{power} refer to the \emph{specification} of exponentiation, and can be applied for proving correctness of any implementation.

Expand Down Expand Up @@ -1379,7 +1379,7 @@ \subsection{Equivalence of the two exponentiation functions}
along \texttt{positive}'s constructors.

\vspace{4pt}
\emph{From Module~\href{../theories/html/hydras.additions.Pow.html}{additions.Pow}}
\emph{From Module~\href{../theories/html/additions.Pow.html}{additions.Pow}}

\begin{Coqsrc}
Lemma binary_power_mult_ok :
Expand Down Expand Up @@ -1704,7 +1704,7 @@ \subsubsection{Definition}



From Module~\href{../theories/html/hydras.additions.Addition_Chains.html}{additions.Addition\_Chains}
From Module~\href{../theories/html/additions.Addition_Chains.html}{additions.Addition\_Chains}

\begin{Coqsrc}
Inductive computation {A:Type} : Type :=
Expand Down Expand Up @@ -1940,7 +1940,7 @@ \subsubsection*{Examples:}
\end{Coqanswer}


\textbf{Note} A first solution (in ~\href{../theories/html/hydras.additions.Trace_exercise.html}{additions.Trace\_exercise}) consists in the definition of
\textbf{Note} A first solution (in ~\href{../theories/html/additions.Trace_exercise.html}{additions.Trace\_exercise}) consists in the definition of
a (non-associative) multiplication over a type of trace, and apply the function
\texttt{chain\_execute} as if it were computing a power of \texttt{(1,Init)}.

Expand Down Expand Up @@ -2297,7 +2297,7 @@ \subsubsection{Example}
\end{Coqsrc}

This tactic is not adapted to much bigger exponents. In \linebreak
Module~\href{../theories/html/hydras.additions.Euclidean_Chains.html}{Euclidean\_Chains},
Module~\href{../theories/html/additions.Euclidean_Chains.html}{Euclidean\_Chains},
for instance, we tried to apply this tactic for proving the correctness
of a chain associated with the exponent $45319$.
We had to interrupt the prover, which
Expand Down Expand Up @@ -2862,7 +2862,7 @@ \section{Euclidean Chains}

\paragraph{Note:}
All the \coq{} material described in this section is available on
Module~\href{../theories/html/hydras.additions.Euclidean_Chains.html}{additions/Euclidean\_Chains.v}
Module~\href{../theories/html/additions.Euclidean_Chains.html}{additions/Euclidean\_Chains.v}

\subsection{Chains and continuations : f-chains}

Expand Down Expand Up @@ -4098,7 +4098,7 @@ \subsection{Generation of chains using Euclidean Dibision}

\vspace{4pt}
\noindent
From ~\href{../theories/html/hydras.additions.Dichotomy.html}{additions.Dichotomy}.
From ~\href{../theories/html/additions.Dichotomy.html}{additions.Dichotomy}.
\begin{Coqsrc}
Class Strategy (gamma : positive -> positive):=
{
Expand All @@ -4123,7 +4123,7 @@ \subsection{The dichotomic strategy}
and a chain that raises its argument to its $8-th$ power.


This strategy is defined in Module ~\href{../theories/html/hydras.additions.Dichotomy.html}{additions.Dichotomy}.
This strategy is defined in Module ~\href{../theories/html/additions.Dichotomy.html}{additions.Dichotomy}.


\begin{Coqsrc}
Expand All @@ -4145,7 +4145,7 @@ \subsection{The dichotomic strategy}
\subsection{Other strategies}
For comparison's sake, we define two other strategies, much simpler but statically less efficient than the dichotomic strategy.

\emph{From Module~\href{../theories/html/hydras.additions.BinaryStrat.html}{additions.BinaryStrat}.}
\emph{From Module~\href{../theories/html/additions.BinaryStrat.html}{additions.BinaryStrat}.}

\begin{Coqsrc}
Definition half (p:positive) :=
Expand Down Expand Up @@ -4491,7 +4491,7 @@ \subsection{A data structure for Euclidean chains}

In \coq{}, we define the instructions as the four constructors of an inductive type.

From Module~\href{../theories/html/hydras.additions.AM.html}{additions.AM}
From Module~\href{../theories/html/additions.AM.html}{additions.AM}

\begin{Coqsrc}
(** basic instructions *)
Expand Down Expand Up @@ -4538,7 +4538,7 @@ \subsection{A data structure for Euclidean chains}
\end{Coqsrc}


In the library~\href{../theories/html/hydras.additions.AM.html}{additions.AM},
In the library~\href{../theories/html/additions.AM.html}{additions.AM},
we define a chain generator for this data structure.
Please note that many proof scripts are copied verbatim from
\texttt{Euclidean\_Chains} into \texttt{AM}. Removing such redundancies is left as a project.
Expand Down
23 changes: 12 additions & 11 deletions doc/chapter-primrec.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -412,7 +412,7 @@ \subsubsection{Elementary proofs of \texttt{isPR} statements}
The constructors \texttt{zeroFunc}, \texttt{succFunc}, and \texttt{projFunc} of type
\texttt{PrimRec} allows us to write trivial proofs of primitive recursivity.
Although the following lemmas are already proven in
\href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec.v},
\href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec},
we wrote alternate proofs in
\href{../theories/html/hydras.MoreAck.PrimRecExamples.html}%
{Ackermann.MoreAck.PrimRecExamples.v}, in order to illustrate the main proof patterns.
Expand Down Expand Up @@ -460,7 +460,7 @@ \subsubsection{Elementary proofs of \texttt{isPR} statements}
\end{Coqsrc}

Projections are proved primitive recursive, case by case (many examples in
\href{../theories/html/hydras.primRec.html}{Ackermann.primRec.v}).
\href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec}).
\emph{Please notice again that the name of the projection follows the mathematical tradition,
whilst the arguments of \texttt{projFunc} use another convention (\emph{cf} remark~\vref{projFunc-order-of-args}).}

Expand All @@ -479,7 +479,7 @@ \subsubsection{Elementary proofs of \texttt{isPR} statements}

\vspace{4pt}
\noindent
\emph{From \href{../theories/html/hydras.primRec.html}{Ackermann.primRec}.}
\emph{From \href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec}.}

\begin{Coqsrc}
Lemma idIsPR : isPR 1 (fun x : nat => x).
Expand Down Expand Up @@ -531,7 +531,7 @@ \subsubsection{Using function composition}

\subsubsection{Proving that \texttt{plus} is primitive recursive}

The lemma \texttt{plusIsPR} is already proven in \href{../theories/html/hydras.primRec.html}{Ackermann.primRec}. We present in
The lemma \texttt{plusIsPR} is already proven in \href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec}. We present in
\href{../theories/html/hydras.MoreAck.PrimRecExamples.html}{MoreAck.PrimRecExamples}
a commented version of this proof,

Expand Down Expand Up @@ -693,7 +693,7 @@ \subsubsection{More examples}
\textbf{Hint:} You may have to look again at the lemmas of the library
\href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec} if you meet some difficulty.
You may start this exercise with the file
\url{../exercises/primrec/MorePRExamples.v}.
\href{https://https://github.com/coq-community/hydra-battles/blob/master/exercises/primrec/MorePRExamples.v}{exercises/primrec/MorePRExamples.v}.
\end{exercise}


Expand All @@ -704,7 +704,7 @@ \subsubsection{More examples}
recursive.

\emph{You may start this exercise with
\url{../exercises/primrec/MinPR.v}.}
\href{https://https://github.com/coq-community/hydra-battles/blob/master/exercises/primrec/MinPR.v}{exercises/primrec/MinPR.v}.}

\end{exercise}

Expand All @@ -729,7 +729,7 @@ \subsubsection{More examples}
the definition of the encoding of $\mathbb{N}^2$ into $\mathbb{N}$, and the proofs that
the associated constructor and projections are primitive recursive.
\emph{You may start this exercise with the file
\url{../exercises/primrec/FibonacciPR.v}.}
\href{https://github.com/coq-community/hydra-battles/blob/master/exercises/primrec/FibonacciPR.v}{exercises/primrec/FibonacciPR.v}.}

\end{exercise}

Expand All @@ -752,7 +752,7 @@ \subsubsection{More examples}
Prove that the function which returns the integer square root of any natural number is primitive recursive.

\emph{You may start this exercise with the file
\url{../exercises/primrec/isqrt.v}.}
\href{https://github.com/coq-community/hydra-battles/blob/master/exercises/primrec/isqrt.v}{exercises/primrec/isqrt.v}.}

\end{exercise}

Expand Down Expand Up @@ -1234,7 +1234,8 @@ \subsection{Looking for a contradiction}
: exists (n:nat), forall x y, f x y <= Ack n (max x y).
\end{Coqsrc}

We prove also a strict version of this lemma, thanks to the following property (proved in Library\href{../theories/html/hydras.MoreAck.Ack.html}{MoreAck.Ack}~).
We prove also a strict version of this lemma, thanks to the following property (proved in Library
\href{../theories/html/hydras.MoreAck.Ack.html}{MoreAck.Ack}~).

\begin{Coqsrc}
Lemma Ack_strict_mono_l : forall n m p, n < m ->
Expand All @@ -1243,7 +1244,7 @@ \subsection{Looking for a contradiction}

\vspace{4pt}
\noindent
\emph{From \href{../theories/html/hydras.MoreAck.AcknotPR.html}{MoreAck.AckNotPR}.}
\emph{From \href{../theories/html/hydras.MoreAck.AckNotPR.html}{MoreAck.AckNotPR}.}

\begin{Coqsrc}
Lemma majorPR2_strict (f: naryFunc 2)(Hf : isPR 2 f):
Expand Down Expand Up @@ -1417,7 +1418,7 @@ \subsubsection{Comparison between $F$ and $H'$}


Looking for lemmas of the form $H'_\beta(k)\leq H'_\alpha(k)$, we find this one (from our library
\href{../theories/html/hydras.Epsilon0.Hprimehtml}{Epsilon0.Hprime}):
\href{../theories/html/hydras.Epsilon0.Hprime.html}{Epsilon0.Hprime}):

\begin{Coqanswer}
H'_restricted_mono_l :
Expand Down
Loading