From d7bacbba67e9242faa24bc6ff34dede1dbe30ed3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 30 Oct 2019 16:01:02 +0100
Subject: [refman] Give an example of contradiction when positivity checking is
 disabled.

---
 doc/sphinx/language/cic.rst | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index c08a9ed0e6..b8c1c523b7 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1046,6 +1046,38 @@ between universes for inductive types in the Type hierarchy.
       exT_intro : forall X:Type, P X -> exType P.
 
 
+.. example:: Negative occurrence
+
+   The following inductive definition is rejected because it does not
+   satisfy the positivity condition:
+
+   .. coqtop:: all
+
+      Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I.
+
+   If we were to accept such definition, we could derive a
+   contradiction from it (we can test this by disabling the
+   :flag:`Positivity Checking` flag):
+
+   .. coqtop:: none
+
+      Unset Positivity Checking.
+      Inductive I : Prop := not_I_I (not_I : I -> False) : I.
+      Set Positivity Checking.
+
+   .. coqtop:: all
+
+      Definition I_not_I '(not_I_I not_I : I) : ~ I := not_I.
+
+   .. coqtop:: in
+
+      Lemma contradiction : False.
+      Proof.
+      enough (I /\ ~ I) as [] by contradiction.
+      split.
+      apply not_I_I; intro; now apply I_not_I.
+      intro; now apply I_not_I.
+      Qed.
 
 .. _Template-polymorphism:
 
-- 
cgit v1.2.3


From 201f31d3cdb1cd30646a622ec4b46d7cbcb24e20 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 30 Oct 2019 17:06:26 +0100
Subject: [refman] Add a second example of contradiction when positivity
 checking is disabled.

---
 doc/sphinx/language/cic.rst | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index b8c1c523b7..ef896b6f03 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1046,7 +1046,7 @@ between universes for inductive types in the Type hierarchy.
       exT_intro : forall X:Type, P X -> exType P.
 
 
-.. example:: Negative occurrence
+.. example:: Negative occurrence (first example)
 
    The following inductive definition is rejected because it does not
    satisfy the positivity condition:
@@ -1079,6 +1079,31 @@ between universes for inductive types in the Type hierarchy.
       intro; now apply I_not_I.
       Qed.
 
+.. example:: Negative occurrence (second example)
+
+   Here is another example of an inductive definition which is
+   rejected because it does not satify the positivity condition:
+
+   .. coqtop:: all
+
+      Fail Inductive Lam := lam (_ : Lam -> Lam).
+
+   Again, if we were to accept it, we could derive a contradiction
+   (this time through a non-terminating recursive function):
+
+   .. coqtop:: none
+
+      Unset Positivity Checking.
+      Inductive Lam := lam (_ : Lam -> Lam).
+      Set Positivity Checking.
+
+   .. coqtop:: all
+
+      Fixpoint infinite_loop l : False :=
+        match l with lam x => infinite_loop (x l) end.
+
+      Check infinite_loop (lam (@id Lam)) : False.
+
 .. _Template-polymorphism:
 
 Template polymorphism
-- 
cgit v1.2.3


From 5d1f7461f74f727d0394e904c3ee820134b22c64 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 30 Oct 2019 17:08:51 +0100
Subject: Use explicit match as suggested by Clément.

---
 doc/sphinx/language/cic.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index ef896b6f03..9e4210793e 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1067,7 +1067,8 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: all
 
-      Definition I_not_I '(not_I_I not_I : I) : ~ I := not_I.
+      Definition I_not_I : I -> ~ I := fun i =>
+        match i with not_I_I not_I => not_I end.
 
    .. coqtop:: in
 
-- 
cgit v1.2.3


From fa822f0762df1c46d8e179afb9b408a927fff149 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 30 Oct 2019 17:10:05 +0100
Subject: Use bullets and indentation (but the result rendering is weird).

---
 doc/sphinx/language/cic.rst | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 9e4210793e..6410620b40 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1074,10 +1074,13 @@ between universes for inductive types in the Type hierarchy.
 
       Lemma contradiction : False.
       Proof.
-      enough (I /\ ~ I) as [] by contradiction.
-      split.
-      apply not_I_I; intro; now apply I_not_I.
-      intro; now apply I_not_I.
+        enough (I /\ ~ I) as [] by contradiction.
+        split.
+        - apply not_I_I.
+          intro.
+          now apply I_not_I.
+        - intro.
+          now apply I_not_I.
       Qed.
 
 .. example:: Negative occurrence (second example)
-- 
cgit v1.2.3