From 5a7ca0b267e8531137d302b9c54b41bed097085f Mon Sep 17 00:00:00 2001 From: jkloos Date: Wed, 18 Oct 2017 19:55:16 +0200 Subject: Fix #5763: Strictly positive example is out of order. I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example. --- doc/refman/RefMan-cic.tex | 60 +++++++++++++++++++++++++---------------------- 1 file changed, 32 insertions(+), 28 deletions(-) diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 0dbfe05d48..542fdf51ec 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -883,56 +883,60 @@ the type $V$ satisfies the nested positivity condition for $X$ \settowidth\framecharacterwidth{\hh} \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth} \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}} +\newcommand{\Tree}{\mbox{\textsf{nattree}}} +\newcommand{\TreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}} +\newcommand{\cnode}{\mbox{\textsf{node}}} +\newcommand{\cleaf}{\mbox{\textsf{leaf}}} -\noindent For instance, if one considers the type +\noindent For instance, if one considers the following variant of a tree type branching over the natural numbers \begin{verbatim} -Inductive tree (A:Type) : Type := - | leaf : list A - | node : A -> (nat -> tree A) -> tree A +Inductive nattree (A:Type) : Type := + | leaf : nattree A + | node : A -> (nat -> nattree A) -> nattree A \end{verbatim} \begin{latexonly} -\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\ +\noindent Then every instantiated constructor of $\TreeA$ satisfies the nested positivity condition for $\Tree$\\ \noindent \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\vh\hh\ws concerning type $\TreeA$ of constructor $\cleaf$:\\ +\ws\ws\vv\ws\ws\ws\ws Type $\TreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\Tree$\\ +\ws\ws\vv\ws\ws\ws\ws because $\Tree$ does not appear in any (real) arguments of the type of that constructor\\ +\ws\ws\vv\ws\ws\ws\ws (primarily because $\Tree$ 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\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\TreeA)\ra\TreeA$ of constructor $\cnode$:\\ + \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\TreeA)\ra\TreeA$ of constructor $\cnode$\\ +\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\Tree$ 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\vh\hh\ws $\Tree$ occurs only strictly positively in $\Type$\ruleref1\\ \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\vh\hh\ws $\Tree$ occurs only strictly positively in $A$\ruleref1\\ \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\vh\hh\ws $\Tree$ occurs only strictly positively in $\NN\ra\TreeA$\ruleref{3+2}\\ \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 +\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\Tree$ satisfies the positivity condition for $\TreeA$\ruleref1 \end{latexonly} \begin{rawhtml} 
-Then every instantiated constructor of list A satisfies the nested positivity condition for list
+Then every instantiated constructor of nattree A satisfies the nested positivity condition for nattree
   │
-  ├─ 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 nattree A of constructor nil:
+  │    Type nattree A of constructor nil satisfies the positivity condition for nattree
+  │    because nattree does not appear in any (real) arguments of the type of that constructor
+  │    (primarily because nattree 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:
+  ╰─ concerning type ∀ A → (nat → nattree A) → nattree A of constructor cons:
+       Type ∀ A : Type, A → (nat → nattree A) → nattree A of constructor cons
+       satisfies the positivity condition for nattree because:
        │
-       ├─ list occurs only strictly positively in Type ... (bullet 3)
+       ├─ nattree occurs only strictly positively in Type ... (bullet 1)
        │
-       ├─ list occurs only strictly positively in A ... (bullet 3)
+       ├─ nattree occurs only strictly positively in A ... (bullet 1)
        │
-       ├─ list occurs only strictly positively in list A ... (bullet 4)
+       ├─ nattree occurs only strictly positively in nat → nattree A ... (bullet 3+2)
        │
-       ╰─ list satisfies the positivity condition for list A ... (bullet 1)
+       ╰─ nattree satisfies the positivity condition for nattree A ... (bullet 1)
\end{rawhtml} -- cgit v1.2.3