exploit.v

(*
Copyright 2009 IMDEA Software Institute
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
    http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)

From Stdlib Require Import ssreflect ssrbool Logic.Hurkens.

(* This file shows the unsoundness of the axiom pack_injective assumed in *)
(* the implementation of Ynot2.0. The proof relies on the lemma of        *)
(* Coquand shown in his 'Mathematical Investigations of a Calculus of     *)
(* Constructions'. Coquand's paper is available at                        *)
(* http://www.cs.chalmers.se/~coquand/meta.pdf. The lemma is stated in    *)
(* several forms on page 15. The proof reduces in a few steps to          *)
(* unsoundness of Girard's system U.                                      *)

(* A simplification of Girard's paradox is given by Hurkens, who ultimately *)
(* proves the same lemma as Coquand. The nice thing is that his proof is    *)
(* available as a Coq library in Coq.Logic.Hurkens, so we can directly use  *)
(* it here.                                                                 *)

Definition pack_injective := forall T (x y : T), inhabits x = inhabits y -> x = y.

Lemma coquand : forall (B : Prop) (E : B -> Prop) (e : Prop -> B)
                       (H : forall A : Prop, A <-> E (e A)), False.
Proof.
by move=>B E e H; apply: (NoRetractFromSmallPropositionToProp.paradox B e E)=>A; move: (H A)=>[H1] H2.
Qed.

Lemma pack_noninjective : pack_injective -> False.
Proof.
pose B := inhabited Prop.
pose e := @inhabits Prop.
pose E x := exists A, (e A = x) /\ A.
move/(_ Prop)=>H.
by apply: (@coquand B E e)=>A; split; [move=>x; exists A | move=>[A'][]; move/H=>->].
Qed.