From 8c2bd9df97972d47554a87c36f5397b514d30cde Mon Sep 17 00:00:00 2001
From: Quentin Carbonneaux
Date: Wed, 6 May 2020 23:18:12 +0200
Subject: Add an example to motivate strictly positive occurrences check

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

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index e5af39c8fb..c36911e576 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1108,6 +1108,70 @@ between universes for inductive types in the Type hierarchy.
 
       Check infinite_loop (lam (@id Lam)) : False.
 
+.. example:: Non strictly positive occurrence
+
+   It is less obvious why inductive definitions with occurences
+   that are positive but not strictly positive are harmful.
+   We will see that in presence of an impredicative type they
+   are unsound:
+
+   .. coqtop:: all
+
+      Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
+
+   If we were to accept this definition we could derive a
+   contradiction by creating an injective function from
+   :math:`A → \Prop` to :math:`A`.
+
+   .. coqtop:: none
+
+      Unset Positivity Checking.
+      Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
+      Set Positivity Checking.
+
+   To make this injection we compose the (injective) constructor of
+   the type :math:`A` with the injective function :math:`λz. z = x`.
+
+   .. coqtop:: all
+
+      Definition f (x: A -> Prop): A := introA (fun z => z = x).
+
+      Lemma f_inj: forall x y, f x = f y -> x = y.
+      Proof.
+        unfold f. intros ? ? H. injection H.
+        set (F := fun z => z = y). intro HF.
+        symmetry. replace (y = x) with (F y).
+        + unfold F. reflexivity.
+        + rewrite <- HF. reflexivity.
+      Qed.
+
+   The type :math:`A → \Prop` can be understood as the powerset
+   of the type :math:`A`. To derive a contradiction from the
+   injective function :math:`f` we use Cantor's classic diagonal
+   argument.
+
+   .. coqtop:: all
+
+      Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x.
+      Definition fd: A := f d.
+
+      Lemma cantor: (d fd) <-> ~(d fd).
+      Proof.
+        split.
+        + intros [s [H1 H2]]. unfold fd in H1.
+          replace d with s. assumption.
+          apply f_inj. congruence.
+        + intro. exists d. split. reflexivity. assumption.
+      Qed.
+
+      Lemma bad: False.
+      Proof.
+        pose cantor. tauto.
+      Qed.
+
+   This derivation was first presented by Thierry Coquand and Christine
+   Paulin in :cite:`CP90`.
+
 .. _Template-polymorphism:
 
 Template polymorphism
-- 
cgit v1.2.3


From bec12fd4c5126987229716d6ca1fb73be458e903 Mon Sep 17 00:00:00 2001
From: Quentin Carbonneaux
Date: Thu, 7 May 2020 10:43:14 +0200
Subject: Drop some the coqtop output, rephrase a bit

---
 doc/sphinx/language/cic.rst | 39 ++++++++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 17 deletions(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index c36911e576..b125d21a3c 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1110,7 +1110,7 @@ between universes for inductive types in the Type hierarchy.
 
 .. example:: Non strictly positive occurrence
 
-   It is less obvious why inductive definitions with occurences
+   It is less obvious why inductive type definitions with occurences
    that are positive but not strictly positive are harmful.
    We will see that in presence of an impredicative type they
    are unsound:
@@ -1119,9 +1119,12 @@ between universes for inductive types in the Type hierarchy.
 
       Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
 
-   If we were to accept this definition we could derive a
-   contradiction by creating an injective function from
-   :math:`A → \Prop` to :math:`A`.
+   If we were to accept this definition we could derive a contradiction
+   by creating an injective function from :math:`A → \Prop` to :math:`A`.
+
+   This function is defined by composing the injective constructor of
+   the type :math:`A` with the function :math:`λx. λz. z = x` injecting
+   any type :math:`T` into :math:`T → \Prop`.
 
    .. coqtop:: none
 
@@ -1129,20 +1132,19 @@ between universes for inductive types in the Type hierarchy.
       Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
       Set Positivity Checking.
 
-   To make this injection we compose the (injective) constructor of
-   the type :math:`A` with the injective function :math:`λz. z = x`.
-
    .. coqtop:: all
 
       Definition f (x: A -> Prop): A := introA (fun z => z = x).
 
+   .. coqtop:: in
+
       Lemma f_inj: forall x y, f x = f y -> x = y.
       Proof.
-        unfold f. intros ? ? H. injection H.
-        set (F := fun z => z = y). intro HF.
-        symmetry. replace (y = x) with (F y).
-        + unfold F. reflexivity.
-        + rewrite <- HF. reflexivity.
+        unfold f; intros ? ? H; injection H.
+        set (F := fun z => z = y); intro HF.
+        symmetry; replace (y = x) with (F y).
+        + unfold F; reflexivity.
+        + rewrite <- HF; reflexivity.
       Qed.
 
    The type :math:`A → \Prop` can be understood as the powerset
@@ -1155,18 +1157,21 @@ between universes for inductive types in the Type hierarchy.
       Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x.
       Definition fd: A := f d.
 
+   .. coqtop:: in
+
       Lemma cantor: (d fd) <-> ~(d fd).
       Proof.
         split.
-        + intros [s [H1 H2]]. unfold fd in H1.
-          replace d with s. assumption.
-          apply f_inj. congruence.
-        + intro. exists d. split. reflexivity. assumption.
+        + intros [s [H1 H2]]; unfold fd in H1.
+          replace d with s.
+          * assumption.
+          * apply f_inj; congruence.
+        + intro; exists d; tauto.
       Qed.
 
       Lemma bad: False.
       Proof.
-        pose cantor. tauto.
+        pose cantor; tauto.
       Qed.
 
    This derivation was first presented by Thierry Coquand and Christine
-- 
cgit v1.2.3