The Coq mailing list

[Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg AT strath.ac.uk>]

Dear Stefan,

On 17/03/2020 21:43, you wrote:
> Would it be possible to define an injective function from `X : Type` to
> `X → Prop` if it weren't for Coq's impredicative treatment of indices?

You can use Leibniz equality, which lives in Prop thanks
to impredicativity:

  Definition leibniz {X : Type}(a b:X) : Prop := forall P:X -> Prop, P a -> P 
b.

Hence already impredicativity + non-strictly positive types
is inconsistent, even in the absence of any notion of inductively
defined propositional equality; just repeat the construction with
Leibniz equality everywhere (see adapted Coq code below). In fact, going
back to the paywalled Coquand Paulin-Mohring paper now, this is the only
notion of equality they use.

Note that just choosing i = leibniz and still formulating eg injectivity
using a non-Prop inductively defined equality does not work: to prove
that i is injective this way, we need to instantiate P : X -> Prop with
equality, which only works if it lives in Prop. But since the paradox is
not using the full J rule, Leibniz equality is enough.

Best wishes,
Fred

(*******************************************)

Definition leibniz {X : Type}(a b:X) : Prop := forall P:X -> Prop, P a -> P b.

Lemma leibniz_refl {X : Type}(x : X) : leibniz x x.
Proof.
 unfold leibniz.
 auto.
Qed.

Lemma leibniz_trans {X : Type}{x y z : X} : leibniz x y -> leibniz y z -> 
leibniz x z.
Proof.
 intros Hxy Hyz.
 unfold leibniz.
 intros P Px.
 apply Hyz.
 apply (Hxy P Px).
Qed.

Lemma leibniz_sym {X : Type}{x y : X} : leibniz x y -> leibniz y x.
Proof.
 unfold leibniz.
 intros H P Py.
 apply (H (fun z => P z -> P x)).
 auto.
 assumption.
Qed.

Lemma leibniz_f_equal {X Y : Type}(f : X -> Y){x x' : X} : leibniz x x' -> 
leibniz (f x) (f x').
Proof.
 intro H.
 unfold leibniz.
 intros P H1.
 apply (H (fun y => P (f y))).
 assumption.
Qed.  

Definition Phi (a : Type) := (a -> Prop) -> Prop.

Axiom A : Type.
Axiom introA : Phi A -> A.
Axiom matchA : A -> Phi A.
Axiom beta : forall x, matchA (introA x) = x.

(* We need beta for Leibniz equality, but there is no harm in
   formulating it using propositional equality (even if it does
   not live in Prop), as we can always go from x = y to leibniz x y.
   (The other direction only works if x = y lives in Prop.)
*)

Lemma eq_leibniz {X : Type}{x y : X} : x = y -> leibniz x y.
Proof.
 intro H.
 elim H.
 apply leibniz_refl.
Qed.

Lemma beta' : forall x, leibniz (matchA (introA x)) x.
Proof.
 intro x.
 apply (eq_leibniz (beta x)).
Qed.
 

Lemma introA_injective : forall p p', leibniz (introA p) (introA p') -> 
leibniz p p'.
Proof.
 intros. 
 assert (leibniz (matchA (introA p)) (matchA (introA p'))) as H1 by (apply 
leibniz_f_equal; assumption).
 apply (leibniz_trans (leibniz_sym (beta' p))).
 apply (leibniz_trans H1).
 apply (leibniz_trans (beta' p')).
 apply leibniz_refl.
Qed.

Definition i {X:Type} : X -> (X -> Prop) := leibniz.

Lemma i_injective : forall X (x x' :X), leibniz (i x) (i x') -> leibniz x x'.
Proof.
 intros.
 assert (leibniz (i x x) (i x' x)) as H1 by (apply (leibniz_f_equal (fun y => 
y x)); assumption).
 apply (H1 (fun y => y)).
 apply leibniz_refl.
 apply leibniz_refl.
Qed.

Definition f : (A->Prop) -> A 
  := fun p => introA (i p).

Lemma f_injective : forall p p', leibniz (f p) (f p') -> leibniz p p'.
Proof.
 unfold f. intros.
 apply introA_injective in H. apply i_injective in H. assumption.
Qed.


Definition P0 : A -> Prop
  := fun x => 
       exists (P:A->Prop), leibniz (f P) x /\ ~ P x.

Definition x0 := f P0.

Lemma bad : (P0 x0) <-> ~(P0 x0).
Proof.
split.
  * intros [P [H1 H2]] H.
    change x0 with (f P0) in H1.
    apply f_injective in H1.
    assert (P0 x0 -> P x0) by apply (leibniz_sym H1 (fun y => y x0)).
    auto.
  * intros.
    exists P0.
    split.
      apply leibniz_refl.
      assumption.
Qed.

Theorem worse : False.
 pose bad. tauto.
Qed.

(*******************************************)

On 17/03/2020 21:43, Stefan Monnier wrote:
> According to the paper "Inductively Defined Types", Coq requires
> *strictly* positive types because non-strictly positive types can be
> used together with impredicativity to introduce a Russel-style paradox.
> 
> More specifically, the paradox goes along the lines of
> [ I here work off of
>    
> http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/
>    rather than Coquand and Paulin(-Mohring)'s paper since that paper is
>    behind a paywall.  ]
> 
> - Define `Inductive A : Type = introA : ((A → Prop) → Prop) → A`.
> - Introduce an injective function `i : ∀X, X → (X → Prop)`.
> - By composing `i` and `introA` we get an injective `f : (A → Prop) → A`.
> - Define a suitable `P0 : A → Prop` and show that `P0 (f P0)` is both
>    true and not.
> 
> In the development, the definition used for `P0` would live in Type if
> it weren't for impredicativity.  Which seems like "the culprit".
> 
> But I also notice that the development defines `i` as an alias for Coq's
> equality type.  But this also only works because Coq's equality type
> always lives in Prop, contrary to Agda and HoTT where it would live in
> Type (because it's an equality between objects that themselves live in
> Type).  This is linked to the treatment of inductive type's indices
> which are treated "impredicatively" in Coq but not in Agda.
> 
> Would it be possible to define an injective function from `X : Type` to
> `X → Prop` if it weren't for Coq's impredicative treatment of indices?
> 
> If not, would that imply that non-strictly positive inductive types
> would be safe even in the presence of Prop-style impredicativity?
> 
> 
>          Stefan
>