From 650ed1278160c2d6dae7914703c8755ab54e095c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Oct 2015 21:16:17 +0200 Subject: RefMan, ch. 4: Reformulating introduction of the chapter on CIC, being clearer that the version depends on the version of Coq. Also renouncing to the "Predicative" and "(Co)" in the name, since after all, usage seems to continue calling the language of Coq Calculus of Inductive Constructions and to consider the Set predicative vs Set impredicative, as well as the presence of coinduction, as flavors of the CIC. --- doc/common/macros.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 0e820008ed..573c3c812e 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -97,8 +97,7 @@ \newcommand{\camlpppp}{\textsc{Camlp4}} \newcommand{\emacs}{\textsc{GNU Emacs}} \newcommand{\ProofGeneral}{\textsc{Proof General}} -\newcommand{\CIC}{\pCIC} -\newcommand{\pCIC}{p\textsc{Cic}} +\newcommand{\CIC}{\textsc{Cic}} \newcommand{\iCIC}{\textsc{Cic}} \newcommand{\FW}{\ensuremath{F_{\omega}}} \newcommand{\Program}{\textsc{Program}} -- cgit v1.2.3 From e7c38a5516246b751b89535594075f6f95a243fd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Oct 2015 22:17:46 +0200 Subject: RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a local context for discharge in global declarations. Discharge now done on a global declaration. Hence removed Def and Assum which were only partially used (e.g. in rules Def and Assum but not in delta-conversion, nor in rule Const). Added discharge rule over definitions using let-in. It replaces the "substitution" rule since about 7.0. --- doc/common/macros.tex | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 573c3c812e..f785a85bbc 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -412,6 +412,7 @@ \newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}} \newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}} \newcommand{\With}[2]{\mbox{\tt ~with~}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}} \newcommand{\Sort}{\mbox{$\cal S$}} -- cgit v1.2.3 From 8654b03544f0efe4b418a0afdc871ff84784ff83 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 9 Oct 2015 15:57:52 +0200 Subject: RefMan, ch. 4: Adding discharging of inductive types. --- doc/common/macros.tex | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index f785a85bbc..88770affbc 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -363,6 +363,7 @@ \newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3} \newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2} \newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}} +\newcommand{\WFTWOLINES}[2]{\ensuremath{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} -- cgit v1.2.3 From b94bdd32024675b546642c710539f8d583df4e94 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 18 Oct 2015 21:07:27 +0200 Subject: RefMan, ch. 4: Removing the local context of inductive definitions. --- doc/common/macros.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 88770affbc..ff13ec4557 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -393,9 +393,9 @@ \newcommand{\CIPI}[1]{\CIP{#1}{I}{P}} \newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}} %BEGIN LATEX -\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{@{}l}#2:=#3 +\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(\begin{array}[t]{@{}l}#2:=#3 \,)\end{array}$}} -\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{@{}l@{}}#3:=#4 +\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\,)$}} -- cgit v1.2.3 From 47377fa44143d409331dd7d0c662e6ebb34d9f4f Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 2 Nov 2015 14:41:37 +0100 Subject: ENH: The beginning of Section 4.5 (Inductive declarations) was changed in order to make it more concrete and more comprehensible. This ver --- doc/common/macros.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index ff13ec4557..fb9190a162 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -260,7 +260,7 @@ \newcommand{\Length}{\mbox{\textsf{Length}}} \newcommand{\length}{\mbox{\textsf{length}}} \newcommand{\LengthA}{\mbox {\textsf{Length\_A}}} -\newcommand{\List}{\mbox{\textsf{List}}} +\newcommand{\List}{\mbox{\textsf{list}}} \newcommand{\ListA}{\mbox{\textsf{List\_A}}} \newcommand{\LNil}{\mbox{\textsf{Lnil}}} \newcommand{\LCons}{\mbox{\textsf{Lcons}}} -- cgit v1.2.3 From 6a66f087bdb773465ce55f8cac040158f07c8d5c Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 3 Nov 2015 10:07:16 +0100 Subject: ALPHA-CONVERSION: s/Length/has_length/g --- doc/common/macros.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index fb9190a162..1ac29b1553 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -257,13 +257,13 @@ \newcommand{\forest}{\mbox{\textsf{forest}}} \newcommand{\from}{\mbox{\textsf{from}}} \newcommand{\hd}{\mbox{\textsf{hd}}} -\newcommand{\Length}{\mbox{\textsf{Length}}} +\newcommand{\haslength}{\mbox{\textsf{has\_length}}} \newcommand{\length}{\mbox{\textsf{length}}} -\newcommand{\LengthA}{\mbox {\textsf{Length\_A}}} +\newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}} \newcommand{\List}{\mbox{\textsf{list}}} \newcommand{\ListA}{\mbox{\textsf{List\_A}}} -\newcommand{\LNil}{\mbox{\textsf{Lnil}}} -\newcommand{\LCons}{\mbox{\textsf{Lcons}}} +\newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}} +\newcommand{\conshl}{\mbox{\textsf{cons\_hl}}} \newcommand{\nat}{\mbox{\textsf{nat}}} \newcommand{\nO}{\mbox{\textsf{O}}} \newcommand{\nS}{\mbox{\textsf{S}}} -- cgit v1.2.3 From 754bc95497ccf903391e5aa1cfda45cb59ad7927 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 3 Nov 2015 10:23:19 +0100 Subject: ENH: new example: "even" --- doc/common/macros.tex | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 1ac29b1553..0ea2ed650b 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -280,6 +280,11 @@ \newcommand{\Type}{\mbox{\textsf{Type}}} \newcommand{\unfold}{\mbox{\textsf{unfold}}} \newcommand{\zeros}{\mbox{\textsf{zeros}}} +\newcommand{\even}{\mbox{\textsf{even}}} +\newcommand{\odd}{\mbox{\textsf{even}}} +\newcommand{\evenO}{\mbox{\textsf{even\_O}}} +\newcommand{\evenS}{\mbox{\textsf{even\_S}}} +\newcommand{\oddS}{\mbox{\textsf{odd\_S}}} %%%%%%%%% % Misc. % -- cgit v1.2.3 From 6c9f5450f476da94aa70df93c5a6368b98e73e90 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 3 Nov 2015 10:37:16 +0100 Subject: CLEANUP: superfluous examples were removed --- doc/common/macros.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 0ea2ed650b..a6240ad284 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -281,7 +281,7 @@ \newcommand{\unfold}{\mbox{\textsf{unfold}}} \newcommand{\zeros}{\mbox{\textsf{zeros}}} \newcommand{\even}{\mbox{\textsf{even}}} -\newcommand{\odd}{\mbox{\textsf{even}}} +\newcommand{\odd}{\mbox{\textsf{odd}}} \newcommand{\evenO}{\mbox{\textsf{even\_O}}} \newcommand{\evenS}{\mbox{\textsf{even\_S}}} \newcommand{\oddS}{\mbox{\textsf{odd\_S}}} -- cgit v1.2.3 From fc73973844f848fafb61b6aa39a327e95f09c129 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 3 Nov 2015 13:28:57 +0100 Subject: CLEANUP: s/List_A/List~A/g --- doc/common/macros.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index a6240ad284..2271a8f134 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -261,7 +261,7 @@ \newcommand{\length}{\mbox{\textsf{length}}} \newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}} \newcommand{\List}{\mbox{\textsf{list}}} -\newcommand{\ListA}{\mbox{\textsf{List\_A}}} +\newcommand{\ListA}{\mbox{\textsf{List}~A}} \newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}} \newcommand{\conshl}{\mbox{\textsf{cons\_hl}}} \newcommand{\nat}{\mbox{\textsf{nat}}} -- cgit v1.2.3 From c5a7d2bec3232625dcb50cfc3a3d6d5abcb81ff0 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 3 Nov 2015 16:59:08 +0100 Subject: ENH: examples for 'strict positivity' were expanded --- doc/common/macros.tex | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'doc/common') diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 2271a8f134..3b12f259b6 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -261,7 +261,7 @@ \newcommand{\length}{\mbox{\textsf{length}}} \newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}} \newcommand{\List}{\mbox{\textsf{list}}} -\newcommand{\ListA}{\mbox{\textsf{List}~A}} +\newcommand{\ListA}{\mbox{\textsf{list}}~\ensuremath{A}} \newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}} \newcommand{\conshl}{\mbox{\textsf{cons\_hl}}} \newcommand{\nat}{\mbox{\textsf{nat}}} @@ -285,6 +285,8 @@ \newcommand{\evenO}{\mbox{\textsf{even\_O}}} \newcommand{\evenS}{\mbox{\textsf{even\_S}}} \newcommand{\oddS}{\mbox{\textsf{odd\_S}}} +\newcommand{\Prod}{\mbox{\textsf{prod}}} +\newcommand{\Pair}{\mbox{\textsf{pair}}} %%%%%%%%% % Misc. % -- cgit v1.2.3