Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Modernize the Coq strict positivity example #17

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Modernize the Coq strict positivity example #17

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 15 additions & 20 deletions src/strict-positivity.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,31 +49,26 @@ and reproduced here:
(* Phi is a positive, but not strictly positive, operator. *)
Definition Phi (a : Type) := (a -> Prop) -> Prop.

(* If we were allowed to form the inductive type
Inductive A: Type :=
introA : Phi A -> A.
then among other things, we would get the following. *)
Axiom A : Type.
Axiom introA : Phi A -> A.
Axiom matchA : A -> Phi A.
Axiom beta : forall x, matchA (introA x) = x.

(* In particular, introA is an injection. *)
#[bypass_check(positivity = yes)]
Inductive A: Type :=
introA : Phi A -> A.

(* If we were allowed to form the inductive type A above (unsoundly bypassing
the positivity restriction), then we get an injective constructor
introA : Phi A -> A *)
Lemma introA_injective : forall p p', introA p = introA p' -> p = p'.
Proof.
intros.
assert (matchA (introA p) = (matchA (introA p'))) as H1 by congruence.
now repeat rewrite beta in H1.
inversion 1; subst; reflexivity.
Qed.

(* However, ... *)
(* However, ... *)

(* Proposition: For any type A, there cannot be an injection
from Phi(A) to A. *)

(* For any type X, there is an injection from X to (X->Prop),
which is λx.(λy.x=y) . *)
Definition i {X:Type} : X -> (X -> Prop) :=
Definition i {X:Type} : X -> (X -> Prop) :=
fun x y => x=y.

Lemma i_injective : forall X (x x' :X), i x = i x' -> x = x'.
Expand All @@ -84,10 +79,10 @@ Proof.
symmetry.
rewrite <- H1.
reflexivity.
Qed.
Qed.

(* Hence, by composition, we get an injection f from A->Prop to A. *)
Definition f : (A->Prop) -> A
Definition f : (A->Prop) -> A
:= fun p => introA (i p).

Lemma f_injective : forall p p', f p = f p' -> p = p'.
Expand All @@ -99,7 +94,7 @@ Qed.
(* We are now back to the usual Cantor-Russel paradox. *)
(* We can define *)
Definition P0 : A -> Prop
:= fun x =>
:= fun x =>
exists (P:A->Prop), f P = x /\ ~ P x.
(* i.e., P0 x := x codes a set P such that x∉P. *)

Expand Down Expand Up @@ -151,10 +146,10 @@ three are necessary:

[^colog88]: Section 3.1 of "Inductively defined types", Thierry Coquand and Christine Paulin, 1988.

[^sjöberg]: [Why must inductive types be strictly positive?](http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/), Vilhelm Sjöberg (2015)
[^sjöberg]: [Why must inductive types be strictly positive?](http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/), Vilhelm Sjöberg (2015)

[^hofmann]: [Martin Hofmann’s Case for Non-Strictly Positive Data Types](https://hal.archives-ouvertes.fr/hal-02365814), Ulrich Berger, Ralph Matthes and Anton Setzer (2018)

[^abel]: Section 7.1 of [A Semantic Analysis of Structural Recursion](http://www.cs.cmu.edu/~abel/publications.html), Andreas Abel (1999)

[^blanqui]: [Inductive types in the Calculus of Algebraic Constructions](https://arxiv.org/abs/cs/0610070), Frédéric Blanqui (2006)
[^blanqui]: [Inductive types in the Calculus of Algebraic Constructions](https://arxiv.org/abs/cs/0610070), Frédéric Blanqui (2006)