From 2bd36760f84f1d79af63cdee4d5d53f289a51204 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 12 Apr 2016 17:17:18 +0200 Subject: FIX: HTML version of Chapter 4 of the Reference Manual --- doc/common/macros.tex | 4 +- doc/refman/RefMan-cic.tex | 257 ++++++++++++++++++++++++++++++++++++---------- 2 files changed, 202 insertions(+), 59 deletions(-) diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 3b12f259b6..bbc78a8517 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -405,8 +405,8 @@ \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4 \,)\end{array}$}} %END LATEX -%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}} -%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}} +%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#2\,:=\,#3)$}} +%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](#3\,:=\,#4)$}} \newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4 \,)\end{array}$}} diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 50f4dc1330..b9c17d8148 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -544,14 +544,43 @@ $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of param \def\colon{@{\hskip.5em:\hskip.5em}} The declaration for parameterized lists is: +\begin{latexonly} \vskip.5em -\ind{1}{\List:\Set\ra\Set}{\left[\begin{array}{r \colon l} - \Nil & \forall A:\Set,\List~A \\ - \cons & \forall A:\Set, A \ra \List~A \ra \List~A - \end{array}\right]} +\ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r \colon l} + \Nil & \forall A:\Set,\List~A \\ + \cons & \forall A:\Set, A \ra \List~A \ra \List~A + \end{array} + \right]} \vskip.5em - +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎝		[ list : Set → Set ]:=⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
nil:=∀A : Set, list A
cons:=∀A : Set, A → list A → list A

+    		⎤
⎦		⎞
⎠
+\end{rawhtml} \noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive list (A:Set) : Set := @@ -559,16 +588,64 @@ Inductive list (A:Set) : Set := | cons : A -> list A -> list A. \end{coq_example*} -\noindent The declaration for a mutual inductive definition of forests and trees is: +\noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is: +\begin{latexonly} \vskip.5em -\ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]} - {\left[\begin{array}{r \colon l} - \node & \forest \ra \tree\\ - \emptyf & \forest\\ - \consf & \tree \ra \forest \ra \forest\\ - \end{array}\right]} +\ind{~}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]} + {\left[\begin{array}{r \colon l} + \node & \forest \ra \tree\\ + \emptyf & \forest\\ + \consf & \tree \ra \forest \ra \forest\\ + \end{array}\right]} \vskip.5em - +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎜
⎝		⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
tree:Set
forest:Set

+    		⎤
⎦		:=⎡
⎢
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
node:forest → tree
emptyf:forest
consf:tree → forest → forest

+    		⎤
⎥
⎦		⎞
⎟
⎠
+\end{rawhtml} \noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} @@ -579,7 +656,8 @@ with forest : Set := | consf : tree -> forest -> forest. \end{coq_example*} -\noindent The declaration for a mutual inductive definition of even and odd is: +\noindent The declaration for a mutual inductive definition of {\even} and {\odd} is: +\begin{latexonly} \newcommand\GammaI{\left[\begin{array}{r \colon l} \even & \nat\ra\Prop \\ \odd & \nat\ra\Prop @@ -594,6 +672,54 @@ with forest : Set := \vskip.5em \ind{1}{\GammaI}{\GammaC} \vskip.5em +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎜
⎝		⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
even:nat → Prop
odd:nat → Prop

+    		⎤
⎦		:=⎡
⎢
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
even_O:even O
even_S:∀n : nat, odd n → even (S n)
odd_S:∀n : nat, even n → odd (S n)

+    		⎤
⎥
⎦		⎞
⎟
⎠
+\end{rawhtml} \noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} @@ -610,9 +736,9 @@ contains an inductive declaration. \begin{description} \item[Ind] \index{Typing rules!Ind} - \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(a:A)\in\Gamma_I}{\WTEG{a}{A}}} + \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(a:A)\in\Gamma_I}{\WTEG{a}{A}}} \item[Constr] \index{Typing rules!Constr} - \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(c:C)\in\Gamma_C}{\WTEG{c}{C}}} + \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(c:C)\in\Gamma_C}{\WTEG{c}{C}}} \end{description} \begin{latexonly}% @@ -726,19 +852,16 @@ any $u_i$ the type $V$ satisfies the nested positivity condition for $X$ \end{itemize} -%% \begin{latexonly}% - \newcommand\vv{\textSFxi} % │ - \newcommand\hh{\textSFx} % ─ - \newcommand\vh{\textSFviii} % ├ - \newcommand\hv{\textSFii} % └ - \newlength\framecharacterwidth - \settowidth\framecharacterwidth{\hh} - \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth} - \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}} -%% \def\captionstrut{\vbox to 1.5em{}} +\newcommand\vv{\textSFxi} % │ +\newcommand\hh{\textSFx} % ─ +\newcommand\vh{\textSFviii} % ├ +\newcommand\hv{\textSFii} % └ +\newlength\framecharacterwidth +\settowidth\framecharacterwidth{\hh} +\newcommand\ws{\hbox{}\hskip\the\framecharacterwidth} +\newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}} -%% \begin{figure}[H] -For instance, if one considers the type +\noindent For instance, if one considers the type \begin{verbatim} Inductive tree (A:Type) : Type := @@ -746,29 +869,49 @@ Inductive tree (A:Type) : Type := | node : A -> (nat -> tree A) -> tree A \end{verbatim} -Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$ - +\begin{latexonly} +\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\ \noindent - \ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\ - \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\ - \ws\ws\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\ - \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\ - \ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1 -%% \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$} -%% \end{figure} -%% \end{latexonly}% +\ws\ws\vv\\ +\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\ +\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\ +\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\ +\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\ +\ws\ws\vv\\ +\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\ +\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\ +\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1 +\end{latexonly} +\begin{rawhtml} +
+Then every instantiated constructor of list A satisfies the nested positivity condition for list
+  │
+  ├─ concerning type list A of constructor nil:
+  │    Type list A of constructor nil satisfies the positivity condition for list
+  │    because list does not appear in any (real) arguments of the type of that constructor
+  │    (primarily because list does not have any (real) arguments) ... (bullet 1)
+  │
+  ╰─ concerning type ∀ A → list A → list A of constructor cons:
+       Type ∀ A : Type, A → list A → list A of constructor cons
+       satisfies the positivity condition for list because:
+       │
+       ├─ list occurs only strictly positively in Type ... (bullet 3)
+       │
+       ├─ list occurs only strictly positively in A ... (bullet 3)
+       │
+       ├─ list occurs only strictly positively in list A ... (bullet 4)
+       │
+       ╰─ list satisfies the positivity condition for list A ... (bullet 1)
+
+\end{rawhtml} \paragraph{Correctness rules.} We shall now describe the rules allowing the introduction of a new @@ -783,7 +926,7 @@ inductive definition. \inference{ \frac{ (\WTE{\Gamma_P}{A_j}{s'_j})_{j=1\ldots k} - ~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n} + ~~~~~~~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n} } {\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}} provided that the following side conditions hold: @@ -811,23 +954,23 @@ inductive definition. The following declaration introduces the second-order existential quantifier $\exists X.P(X)$. \begin{coq_example*} -Inductive exProp (P:Prop->Prop) : Prop - := exP_intro : forall X:Prop, P X -> exProp P. +Inductive exProp (P:Prop->Prop) : Prop := + exP_intro : forall X:Prop, P X -> exProp P. \end{coq_example*} The same definition on \Set{} is not allowed and fails: % (********** The following is not correct and should produce **********) % (*** Error: Large non-propositional inductive types must be in Type***) \begin{coq_example} -Fail Inductive exSet (P:Set->Prop) : Set - := exS_intro : forall X:Set, P X -> exSet P. +Fail Inductive exSet (P:Set->Prop) : Set := + exS_intro : forall X:Set, P X -> exSet P. \end{coq_example} It is possible to declare the same inductive definition in the universe \Type. The \texttt{exType} inductive definition has type $(\Type_i \ra\Prop)\ra \Type_j$ with the constraint that the parameter \texttt{X} of \texttt{exT\_intro} has type $\Type_k$ with $kProp) : Type - := exT_intro : forall X:Type, P X -> exType P. +Inductive exType (P:Type->Prop) : Type := + exT_intro : forall X:Type, P X -> exType P. \end{coq_example*} %We shall assume for the following definitions that, if necessary, we %annotated the type of constructors such that we know if the argument -- cgit v1.2.3