From 0f34ee172f1d0f8c68ed8ac590e3fd3a30c4d4e8 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Thu, 14 Jan 2021 16:16:38 +0100 Subject: [PATCH 1/4] removed last marginpars --- tex/chProofLanguage.tex | 8 ++++++-- tex/chProofs.tex | 3 +-- tex/chTT.tex | 3 --- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tex/chProofLanguage.tex b/tex/chProofLanguage.tex index 2378c8e1..36963756 100644 --- a/tex/chProofLanguage.tex +++ b/tex/chProofLanguage.tex @@ -247,8 +247,12 @@ \subsection{Pulling from the stack} new variable (the predecessor of what used to be called \C{y}). Since \C{y} is destructed we could have reused that name for its predecessor, as it is often done in the \mcbMC{} library. -Recall the definition of \C{odd} \marginpar{odd is never given}: -when applied to \C{z.+1} it simplifies to \C{\~\~ odd z}. +In fact, the boolean predicate \C{odd} is defined by case analysis, +and induction, on its argument of type \C{nat}: +\begin{coq}{}{} +Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false. +\end{coq} +Therefore, when applied to \C{z.+1}, it simplifies to \C{\~\~ odd z}. Now, the fact that \C{z} is even is not needed to conclude, so we can discard it by giving it the \C{\_} dummy name.~\footnote{ diff --git a/tex/chProofs.tex b/tex/chProofs.tex index 591bac09..803b41af 100644 --- a/tex/chProofs.tex +++ b/tex/chProofs.tex @@ -1554,8 +1554,7 @@ \subsection{Using lemmas in proofs} \end{coq} \coqrun{name=testexp}{ssr,exp,abort} -where \D{p \%| m`!} stands for ``\C{p} divides the factorial of \C{m}''.\marginpar{there is a problem with the factorial notation at the beginning -of this line} +where \D{p \%| m`!} stands for ``\C{p} divides the factorial of \C{m}''. The first step of our formal proof will be to give a name to the hypothesis \C{(prime p)}, which means that we add it to the diff --git a/tex/chTT.tex b/tex/chTT.tex index f7a195ad..a18baa75 100644 --- a/tex/chTT.tex +++ b/tex/chTT.tex @@ -171,7 +171,6 @@ \section{Propositions as types, proofs as programs}\label{sec:patpap} term of the corresponding type. Objects of the formalism are programs, and proofs are themselves objects of the formalism. -% \marginpar{meta is condusing here: take more time to talk about this} In this setting the analogue of ``a proposition has a proof'' is that ``a term has a given type''. Such a statement, called a \emph{typing judgment}, is a ternary relation written as follows: @@ -732,8 +731,6 @@ \section{Conversion}\label{sec:conv} homonymous algebraic structure~\cite{gregoire:hal-00819484}. -%\marginpar{Say here that computation can be used for automation? and -% simpl? and that controlling it is a delicate issue?} % One can also benefit from convertibility whenever one applies a lemma; From 56f98aee0fe7ccd90ad2731c6978459e96b61ba6 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Thu, 14 Jan 2021 16:25:48 +0100 Subject: [PATCH 2/4] fixed tcolorboxes (color+spacing_ --- tex/chSigmaBool.tex | 3 ++- tex/chTypeInference.tex | 9 ++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/tex/chSigmaBool.tex b/tex/chSigmaBool.tex index de650803..c9dbfa53 100644 --- a/tex/chSigmaBool.tex +++ b/tex/chSigmaBool.tex @@ -264,8 +264,9 @@ \section{$n$-tuples, lists with an invariant on the length} The global table of canonical solutions is extended as follows. +\vspace{1ex} \noindent -\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=Canonical Structures Index] +\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=Canonical Structures Index] projection & value & solution & combines solutions for \\ \hline \lstinline/tval N A/ & \lstinline/rev A S/ & \lstinline/rev_tuple N A T/ & \lstinline/T/ $\leftarrow$ (\lstinline/tval N A/, \lstinline/S/) \\ diff --git a/tex/chTypeInference.tex b/tex/chTypeInference.tex index 5497b22d..f0a65438 100644 --- a/tex/chTypeInference.tex +++ b/tex/chTypeInference.tex @@ -612,7 +612,8 @@ \section{Records as relations}\label{sec:eqtype} Whenever a record instance is declared as canonical \Coq{} adds to such table an entry for each field of the record type. -\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index] +\vspace{1ex} +\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index] projection & value & solution \\ \hline \lstinline/sort/ & \lstinline/nat/ & \lstinline/nat_eqType/ \\ \lstinline/sort/ & \lstinline/bool/ & \lstinline/bool_eqType/ \\ @@ -727,8 +728,9 @@ \section{Records as relations}\label{sec:eqtype} The global table of canonical solutions is extended as follows. +\vspace{1ex} \noindent -\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=canonical structures Index] +\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,center title,tabularx={ll|l|l},fonttitle=\sffamily\bfseries,title=canonical structures Index] projection & value & solution & combines solutions for \\ \hline \lstinline/sort/ & \lstinline/nat/ & \lstinline/nat_eqType/ & \\ \lstinline/sort/ & \lstinline/bool/ & \lstinline/bool_eqType/ & \\ @@ -1531,8 +1533,9 @@ \subsection{Assumptions of a bigop lemma}\label{sec:bigoplemmas} This command adds the following rule to the canonical structures index: +\vspace{1ex} \noindent -\begin{tcolorbox}[colframe=blue!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index] +\begin{tcolorbox}[colframe=orange!60!white,before=\hfill,after=\hfill,width=8cm,center title,tabularx={ll|l},fonttitle=\sffamily\bfseries,title=canonical structures Index] projection & value & solution \\ \hline \lstinline/Monoid.operator/ & \lstinline/addn/ & \lstinline/addn_monoid/ \\ \hline From 9b980dca79b7824b5fafbe2098a4fcf1b47bfb29 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Thu, 14 Jan 2021 16:29:01 +0100 Subject: [PATCH 3/4] fixing toc depth --- tex/main.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/tex/main.tex b/tex/main.tex index 51b0d232..2f1542e8 100755 --- a/tex/main.tex +++ b/tex/main.tex @@ -127,6 +127,7 @@ \pagestyle{empty} % No headers +\setcounter{tocdepth}{1} \tableofcontents % Print the table of contents itself \cleardoublepage{} % Forces the first chapter to start on an odd page so it's on the right From d34ce5233c60ee7e1aad90ccd671e6828dcf1896 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Thu, 14 Jan 2021 16:49:13 +0100 Subject: [PATCH 4/4] uniformization of capitaliztion in part/section titles --- tex/chProgramming.tex | 2 +- tex/chProofLanguage.tex | 4 ++-- tex/chProofs.tex | 2 +- tex/chSigmaBool.tex | 2 +- tex/chSpecification.tex | 2 +- tex/chTT.tex | 2 +- tex/chTypeInference.tex | 4 ++-- tex/main.tex | 4 ++-- 8 files changed, 11 insertions(+), 11 deletions(-) diff --git a/tex/chProgramming.tex b/tex/chProgramming.tex index 8066a712..80e2f326 100644 --- a/tex/chProgramming.tex +++ b/tex/chProgramming.tex @@ -12,7 +12,7 @@ . \end{coqdef} -\chapter{Functions and Computation}\label{ch:prog} +\chapter{Functions and computation}\label{ch:prog} In the formalism underlying the \Coq{} system, functions play a central role akin to the one of sets in set theory. However, diff --git a/tex/chProofLanguage.tex b/tex/chProofLanguage.tex index 36963756..b02e0f45 100644 --- a/tex/chProofLanguage.tex +++ b/tex/chProofLanguage.tex @@ -1,4 +1,4 @@ -\chapter{A Proof Language for Formal Proofs}{} +\chapter{A proof language for formal proofs}{} \label{ch:script} @@ -87,7 +87,7 @@ \chapter{A Proof Language for Formal Proofs}{} %\section{Managing the proof context} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Bookkeeping: Goals as stacks}\label{ssec:stack} +\section{Bookkeeping: goals as stacks}\label{ssec:stack} \index[concept]{goal stack model} The presentation we gave so far of proof commands like \C{case: n => [|m]} diff --git a/tex/chProofs.tex b/tex/chProofs.tex index 803b41af..1b74e773 100644 --- a/tex/chProofs.tex +++ b/tex/chProofs.tex @@ -31,7 +31,7 @@ \end{coqdef} -\chapter{First Steps in Formal Proofs}{} +\chapter{First steps in formal proofs}{} \label{ch:proofs} % In this chapter we explain how to state a lemma, % how to prove it, and how to search existing, loaded library. diff --git a/tex/chSigmaBool.tex b/tex/chSigmaBool.tex index c9dbfa53..2fabae12 100644 --- a/tex/chSigmaBool.tex +++ b/tex/chSigmaBool.tex @@ -19,7 +19,7 @@ Require Import tuple. \end{coqdef} -\chapter{Sub-Types}{}\label{ch:sigmabool} +\chapter{Sub-types}{}\label{ch:sigmabool} Inductive data types have been used to both code data, like lists, and logical connectives, like the existential quantifier. diff --git a/tex/chSpecification.tex b/tex/chSpecification.tex index da122499..ca7e2363 100644 --- a/tex/chSpecification.tex +++ b/tex/chSpecification.tex @@ -1,4 +1,4 @@ -\chapter{Inductive Specifications}{} +\chapter{Inductive specifications}{} \label{ch:boolrefl} % in addition to the photos: diff --git a/tex/chTT.tex b/tex/chTT.tex index a18baa75..9587c659 100644 --- a/tex/chTT.tex +++ b/tex/chTT.tex @@ -1,4 +1,4 @@ -\chapter{Dependent Type Theory}{} +\chapter{Dependent type theory}{} \label{ch:ttch} %% Summary of the 22/02 discussion: diff --git a/tex/chTypeInference.tex b/tex/chTypeInference.tex index f0a65438..f6b683c1 100644 --- a/tex/chTypeInference.tex +++ b/tex/chTypeInference.tex @@ -12,7 +12,7 @@ Abort. \end{coqdef} -\chapter{Implicit Parameters}{} +\chapter{Implicit parameters}{} The rules of the \mcbCIC{}, as the ones sketched in~\ref{ch:ttch}, are expressed on the syntax of terms and @@ -91,7 +91,7 @@ \chapter{Implicit Parameters}{} %\mcbLEARN{HO unif is hard} %\mcbREQUIRE{} %\mcbPROVIDE{terminology} -\section{Type inference and Higher-Order unification}\label{sec:hounif} +\section{Type inference and higher-order unification}\label{sec:hounif} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The type inference algorithm is quite similar to the type checking diff --git a/tex/main.tex b/tex/main.tex index 2f1542e8..a57badbf 100755 --- a/tex/main.tex +++ b/tex/main.tex @@ -58,8 +58,8 @@ \makeindex[name=coq,title=Definitions and Notations,intoc] \makeindex[name=vernac,title=Coq Commands,intoc] -\newcommand{\partonename}{Languages for writing Formal Mathematics} -\newcommand{\parttwoname}{Crafting a Formal Library} +\newcommand{\partonename}{Languages for writing formal mathematics} +\newcommand{\parttwoname}{Crafting a formal library}