diff options
| -rw-r--r-- | doc/sphinx/language/cic.rst | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index c08a9ed0e6..6410620b40 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1046,6 +1046,67 @@ between universes for inductive types in the Type hierarchy. exT_intro : forall X:Type, P X -> exType P. +.. example:: Negative occurrence (first example) + + 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 : I -> ~ I := fun i => + match i with not_I_I not_I => not_I end. + + .. 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. + +.. 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: |