Examples that show paradoxes when using combinations of impredicative polymorphism + excluded middle + large elimination -- can only choose two

[catalin-hritcu]

Since this is an important discussion I'm splitting off a separate thread (previous one is https://github.com/FStarLang/FStar/issues/355#issuecomment-139806214).

It is folklore in the type theory world that mixing the following, very useful and apparently innocuous, ingredients leads to inconsistency:

impredicative polymorphism + excluded middle + large elimination => false

In particular, Berardi's paradox (the latest of a series of paradoxes starting with Russell's paradox) shows that

(1) impredicative polymorphism + excluded middle => proof irrelevance

Proof irrelevance says that all proofs of the same proposition are equal, or more generally that all inhabitants of the same type are equal. Proof irrelevance is a reasonable property, for instance Coq's sort Prop is impredicative and known to soundly admit proof irrelevance (and excluded middle too). Proof irrelevance is, however, clearly incompatible with anything that would allow distinguishing proofs, or generally type inhabitants. "Large elimination" is such a thing.

(2) proof irrelevance + large elimination => false

Coq enforces that values of types of sort Prop are not used for their informational content by imposing an elimination restriction: if a match expression matches on a value of a type of sort Prop, the return type of the match expression must itself also be of sort Prop. In other words, matching on proofs is allowed only to build other proofs. This restriction is strong. In particular, if Bool was defined in Prop, this restriction would prevent one from proving that true and false are distinct:

Inductive Bool : Prop := T : Bool | F : Bool.

Definition two_elements_Bool (H : T = F) : False :=
  match H in (_ = y0) return (match y0 with
                                | T => True
                                | F => False
                              end) with
    | eq_refl => I
  end.
(* Error: *)
(* Incorrect elimination of "y0" in the inductive type "Bool": *)
(* the return type has sort "Type" while it should be "Prop". *)
(* Elimination of an inductive object of sort Prop *)
(* is not allowed on a predicate in sort Type *)
(* because proofs can be eliminated only to build proofs. *)

As we see more pressure to deeply integrate classical proofs done with the SMT solver with manual constructive proofs in F*'s pure fragment, splitting up a separate kind Prop, that's a sub-kind of Type and that features impredicative polymorphism and excluded middle seems appealing. The key to doing this soundly seems adopting Coq's elimination restriction for Prop.

Summoning @nikswamy, @ckeller, @s-zanella, @aa755, and @maximedenes for this discussion.

Some references https://cstheory.stackexchange.com/questions/21836/why-does-coq-have-prop/21878#21878 http://people.cs.kuleuven.be/~bart.jacobs/coq-essence.pdf (Section 13 discusses sort Prop) https://coq.inria.fr/refman/Reference-Manual006.html#sec208 http://adam.chlipala.net/cpdt/html/Universes.html#lab77 https://coq.inria.fr/library/Coq.Logic.Berardi.html https://github.com/FStarLang/FStar/blob/master/examples/paradoxes/berardi_minimal.fst http://www.cs.nott.ac.uk/~txa/g53cfr/l20.html/l20.html

[aa755]

I'd like to see an example of a use of Prop that cannot be accomplished with just the erased type constructor. Like Props, erased types have proof irrelevance. For example, I think one cannot prove that hide 0 is different from hide 1 (in the type erased nat). I think we can safely assume an analog of excluded middle : forall T:Type, erased (either T (T-> Tot False)) . A similar rule (using squash types) is provably consistent with Nuprl. In fact, A \/ B could be defined as erased (either A B).

Perhaps the erased type constructor cannot be used to define impredicative constructs. I'd be curious to see if impredicativity is needed for anything other than proving consistency of very powerful theories.

[nikswamy]

Rejecting impredicativity is certainly an option we should keep on the table.

[catalin-hritcu]

I'd like to see an example of a use of Prop that cannot be accomplished with just the erased type constructor.

You're the expert in erased types, but I wouldn't be surprised if such examples existed.

Like Props, erased types have proof irrelevance. For example, I think one cannot prove that hide 0 is different from hide 1 (in the type erased nat).

Really? Here are two proofs that hide 0 and hide 1 are different, first one directly by SMT:

val hide0_hide1_smt : unit -> Lemma (ensures (~(hide 0 = hide 1)))
let hide0_hide1_smt () = ()

and also a constructive one in case you also find proofs by SMT shady in such cases:

assume val neq01 : ceq 0 1 -> Tot cfalse
// let neq01 h = let (Refl _) = h in 42 -- need empty pattern maching (#70) 

val reveal_hide : #a:Type -> x:a -> GTot (ceq (reveal (hide x)) x)
let reveal_hide (a:Type) x = Refl (reveal (hide x))

val hide0_hide1_constr : ceq (hide 0) (hide 1) -> GTot cfalse
let hide0_hide1_constr h =
  let h0 : (ceq (reveal (hide 0)) 0) = reveal_hide 0 in
  let h1 : (ceq (reveal (hide 1)) 1) = reveal_hide 1 in
  let h' : (ceq (reveal (hide 0))
                (reveal (hide 1))) = ceq_congruence h reveal in
  let h'' : (ceq 0 1) = ceq_trans (ceq_trans (ceq_symm h0) h') h1 in
  neq01 h''

Both these proofs are necessarily ghost, but so are many of our proofs. My impression is that ghost and erased could indeed be used to track proofs, but that's not enough for supporting proof irrelevance. Strong restrictions on the elimination (or impredicativity) of ghost would still be required for that. [Edit (addition): I have no clue what shape such elimination restrictions would take; as the example above shows it's clearly not enough to enforce that ghost things can only be used to compute other ghost things, since we already enforce that.]

I think we can safely assume an analog of excluded middle : forall T:Type, erased (either T (T-> Tot False)) . A similar rule (using squash types) is provably consistent with Nuprl. In fact, A \/ B could be defined as erased (either A B).

What's the status of polymorphism in Nuprl? Does it have any?

[Edit: google answered this for me, see next comment]

Perhaps the erased type constructor cannot be used to define impredicative constructs. I'd be curious to see if impredicativity is needed for anything other than proving consistency of very powerful theories.

In Coq the impredicativity of Prop is used all the time. When universally quantifying over a proposition the expectation is that another quantified proposition can be plugged in. My impression is that to allow this one would need at least universes. If additionally one wants to be able to plug in the original proposition one started with then one needs impredicativity. Bart Jacobs's book has a very simple example of this in the "12. Limitations of the Curry-Howard correspondence > 12.1 Propositions about propositions" section.

Inductive And(P Q: Type) := and_(p: P)(q: Q).
Definition P0: Type := forall (P : Type), P -> And P P.
Definition P0proof: P0 := fun (P: Type) (p: P) => and_ P P p p.
Definition AndP0P0proof: And P0 P0 := P0proof P0 P0proof.
(* Error: Universe inconsistency. *)

While one might argue that this example is contrived and one can live without impredicativity (e.g. Agda people do), one seems to need universes instead to be able to do simple logical proofs (Agda does have universes). My impression is that universes are not any simpler than impredicativity, on the contrary.

[catalin-hritcu]

Did a bit of googling and discovered that Nuprl has universes, both for Prop and for Type: http://www.cs.cornell.edu/info/people/sfa/nuprl/NuprlPrimitives/Xuniverse_doc.html http://www.cs.cornell.edu/info/people/sfa/nuprl/NuprlPrimitives/Xprop_levels_doc.html So yes, "rejecting impredicativity" usually means adding universes instead (i.e. going "predicative").

[aa755]

1) erased can should be defined in a way such that proof irrelevance is consistent or even provable for erased types. I don't know how opaque works, but it does seem to leak some implementation details. There should be an erased.fsi specifying erased, hide, reveal, emap e.t.c. axiomatically, and perhaps an implementation in erased.fst . Unless one explicitly puts anything else in the interface, erased.fsi, neither proof relevance, nor proof irrelevance should be provable.

2) Nuprl does NOT have any special universes for propositions. As long as I have used the system, Prop{i} has just been a notation for U{i}.

3) Adding a predicative hierarchy of universes might actually simplify some of the duplications of machinery for types (U0) and kinds (U1).

[catalin-hritcu]

@aa755 For point 1) it would be interesting to see if you could work out such interface. The interface would need to do something meaningful for reveal, without exposing that it simply cancels hide out?

For points 2) and 3), my impression is that universes would be a heavy solution to our problem, but we should definitely keep it on the list in case simpler solutions fail. An impredicative Prop + a Type a la System F-omega, with only simple inductives in Type, seems to me like a potential simpler solution.

[aa755]

Right. Putting anything sensible for reveal seems to contradict proof relevance. Sorry, it had nothing to do with opaque. We can still have hide and emap (('a->'b) -> erased 'a -> erased 'b). Indeed, I don't know of anything analogous to reveal in Nuprl, or even Coq, or HoTT. Proof irrelevance is provable in Nuprl (squash types) and HoTT (propositional truncations [1]), and consistent in Coq (Prop).

Even without reveal, I think that erased types might be useful for specifications, as long as proof irrelevance neither provable, nor falsifiable. For example, a while back, I played with a definition of erased in Coq: https://github.com/FStarLang/FStar/blob/9991ab0e22443e0415fa0454b845c41d0a70b555/examples/extraction/extTest.v#L222

If we want provable proof irrelevance, erased types may become totally useless for writing specs.

Perhaps, we should have two type constructors, one for erasure and the other (like quotient or squash) for proof irrelevance? Having same type constructor serve both purposes seems tricky/impossible.

I'm curious How would you have reveal in the Prop universe approach?

[1] : http://homotopytypetheory.org/2015/07/28/constructing-the-propositional-truncation-using-nonrecursive-hits/

[nikswamy]

Erased types were designed for erasure. I didn't have proof irrelevance in mind at all. I don't think we'd want something like reveal in Prop.

[aa755]

A problem with the Prop universe approach that once one defines something, e.g. inductively defined proposition, in the Prop universe, there is no way to use it in a constructive setting where proof relevance may be needed. For example, we wanted to define Nuprl predicatively in Coq and we had to duplicate a lot of the standard library of Coq. With the squash type constructor, there is no such dichotomy when defining something. One can just put a squash around existing definitions when proof irrelevance is needed. Also, perhaps no extension is needed to implement a squash type construct in F*

[s-zanella]

@aa755 Universe polymorphism is a solution, especially if the universe hierarchy goes beyond just Prop and Type_0.

[aa755]

I don't know if it is possible to be polymorphic over both Prop and Type_i, i.e., to quantify a variable, say T, in a way that it can be instantiated with both Prop and Type_i . AFAIK, Coq does not have it. Is it impossible? It does seem tricky to get right.

[s-zanella]

Coq universe polymorphism does allow writing definitions that abstract over variables that can be instantiated with both Prop and Type_i. It's fairly new and experimental, and it doesn't play well with tactics like vm_compute, but it works (see the interactive session below, and notice the eta-expansion of prod in contrast to prod2).

Welcome to Coq v8.5 (1bb47bf8f5d435b33b2bf5bd234e3eae372d99f6)
Coq < Definition id {A : Type} (a : A) := a.

Coq < Check id : Type -> Type.
id:Type -> Type
     : Type -> Type

Coq < Check id : Prop -> Prop.
id:Prop -> Prop
     : Prop -> Prop

Coq < Print prod.
Inductive prod (A B : Type) : Type :=  pair : A -> B -> A * B

Coq < Check prod : Prop -> Prop -> Prop.
(fun A B : Prop => (A * B)%type):Prop -> Prop -> Prop
     : Prop -> Prop -> Prop

Coq < Polymorphic Inductive prod2 (A B : Type) : Type :=  pair2 : A -> B -> prod2 A B.

Coq < Print prod2.
Polymorphic Inductive prod2 (A B : Type) : Type :=
    pair2 : A -> B -> prod2 A B

Coq < Check prod2 : Prop -> Prop -> Prop.
prod2:Prop -> Prop -> Prop
     : Prop -> Prop -> Prop

Coq < Print and.
Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B

Coq < Check and : Prop -> Prop -> Prop.
and:Prop -> Prop -> Prop
     : Prop -> Prop -> Prop

Coq < Check and : Type -> Type -> Type.
Toplevel input, characters 6-9:
> Check and : Type -> Type -> Type.
>       ^^^
Error:
The term "and" has type "Prop -> Prop -> Prop"
while it is expected to have type "Type -> Type -> Type"
(universe inconsistency).

Coq < Print sigT.
Inductive sigT (A : Type) (P : A -> Type) : Type :=
    existT : forall x : A, P x -> {x : A & P x}

Coq < Check sigT : forall (A:Prop), (A -> Prop) -> Prop.
(fun (A : Prop) (P : A -> Prop) => {x : A & P x})
:forall A : Prop, (A -> Prop) -> Prop
     : forall A : Prop, (A -> Prop) -> Prop

References: Universe Polymorphism in Coq The Rooster and the Syntactic Bracket Coq Refman

[catalin-hritcu]

Together with Nik, we followed Abhishek's suggestion and added a squashed types interface. https://github.com/FStarLang/FStar/blob/master/lib/squash.fsti The interface includes 3 axioms: get_proof, give_proof, and proof_irrelevance as well as a monad structure (return_squash,bind_squash, and map_squash). The monad functions are easily given a model by taking squash to be the identity type constructor (https://github.com/FStarLang/FStar/blob/master/lib/squash.fst), while the axioms are taken on faith. We actually tried to replay the Berardi proof to get proof_irrelevance but got stuck because of the squashes (https://github.com/FStarLang/FStar/blob/master/lib/squashproperties.fst#L107). Does anyone else want to try?

Unrelated: @s-zanella Maxime (@maximedenes) says that universe polymorphism over Prop is currently inconsistent and might be removed (https://coq.inria.fr/bugs/show_bug.cgi?id=4287).

[aa755]

Can this be squash t be defined as x : Unit{t} in file squash.fst? This might be how squash types were once defined in Nuprl. I think proof irrelevance will then be provable. The question is whether other existing things about squash remain provable.

Also, can the proof_irrelevance be defined as below?

val proof_irrelevance : p:Type -> x:squash p ->
                                  y:squash p -> Tot ((x = y))

Also, It should be consistent to add a squashed version of excluded middle: http://www.nuprl.org/html/verification/v1/html/raw/rules_classical.html

[nikswamy]

But if you chose that representation how would you implement map_squash?

[catalin-hritcu]

Both the partial model where squash t = t and the one where squash t = u:unit{t} seem rather lame. The first only models the monad operations while the second only models get_proof, give_proof, and proof_irrelevance. One difference is that the squash t = u:unit{t} doesn't require squash to be an abstract type, but that's not a big gain. By and large, this would be an axiomatic presentation of squash.

Just added one extra axiom to squash.fsti that seems needed (for proving things like forall_intro) but that doesn't seem to follow from the other axioms and that doesn't seem provable in neither of the partial models:

assume val squash_double_arrow : #a:Type -> #p:(a -> Type) ->
  =f:(squash (x:a -> Tot (squash (p x)))) -> Tot (squash (x:a -> Tot (p x)))

Is there something like the monadic structure or squash_double_arrow in Nuprl?

[s-zanella]

Some remarks:

return_squash is derivable from get_proof

val return_squash : #a:Type -> a -> Tot (squash a)
let return_squash (#a:Type) x = get_proof a

map_squash is derivable from get_proof and return_squash (get_proof):

val map_squash : #a:Type -> #b:Type -> squash a -> (a -> Tot b) -> Tot (squash b)
let map_squash s f = 
  let g = fun x -> return_squash (f x) in
  bind_squash s g

This answers Nikhil's question above about the definability of map_squash, but only partially because it shifts the problem to defining bind_squash. Still, I think this tips the balance in favour of the type squash (t:Type) = u:unit{t} model: of the original axioms, only bind_squash may need to be assumed. I feel this is also closer to the spirit of the squash operator in Nogin's quotient types paper.

On the other hand, the squash t = t model can be extended with give_proof:

val give_proof : #p:Type -> squash p ->
  Pure unit (requires True) (ensures (fun _ -> p))
let give_proof (#p:Type) (s:squash p) = ()

But this model is inconsistent because it assumes proof irrelevance for any type, so I don't know if it is valid.

[aa755]

I always thought of F's refinement types as set types of Nuprl. I am surprised that the following is not provable in F. Is this just a weakness in the SMT solver? or something goes wrong if it were provable?

val refmap : ('a -> Tot 'b) -> x:unit{'a} -> Tot (y:unit{'b})

bind_squash is provable in Nuprl.

[ckeller]

According to the paper A compact kernel for the calculus of inductive constructions describing the kernel of Matita, p.17, most Coq and Matita libraries need only 2 universes. For this reason, the current version of Matita does not implement universe inference (universes are fixed for each declaration).

[catalin-hritcu]

@aa755 You were right, by the way. You might notice an universes branch :)

[aa755]

Congrats on universes :)

[catalin-hritcu]

@nikswamy says

it would be great for someone to revisit Berardi, Russell etc. and try to replay them with --universes

Any takers? (it will take a while until I can get to this)

[s-zanella]

Revisiting means that we convince ourselves that they cannot be replayed? Or adding enough axioms so that they can?

Either way, this requires a means to denote universes beyond Type0, which is still pending in #505.

[catalin-hritcu]

Revisiting means that we convince ourselves that they cannot be replayed? Or adding enough axioms so that they can?

Both would be useful, once you can write higher universes.

[catalin-hritcu]

Kenji (@kyoDralliam) has implemented explicit universe syntax some months ago (https://github.com/FStarLang/FStar/wiki/Explicit-universes), so we should be able to bring back all these paradoxes with enough axioms.

[nikswamy]

Renaming the issue. Who wants to take on writing some of these examples? @kyoDralliam @s-zanella @catalin-hritcu ?

[catalin-hritcu]

Some related Twitter thread? https://twitter.com/yforster_cs/status/1564600813376479233