Add an example to motivate strictly positive occurrences check

1 files changed, 64 insertions, 0 deletions

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