From a4213c93fb8997e1f6a1f6ff0adcf4e4119b1bbd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Jun 2014 11:47:18 +0200 Subject: Bug #3301 is closed, the projection cannot be defined anymore. --- test-suite/bugs/closed/3301.v | 105 ++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/3301.v | 120 ------------------------------------------ 2 files changed, 105 insertions(+), 120 deletions(-) create mode 100644 test-suite/bugs/closed/3301.v delete mode 100644 test-suite/bugs/opened/3301.v diff --git a/test-suite/bugs/closed/3301.v b/test-suite/bugs/closed/3301.v new file mode 100644 index 0000000000..fca47b43c2 --- /dev/null +++ b/test-suite/bugs/closed/3301.v @@ -0,0 +1,105 @@ +Section Hurkens. + +Definition Type2 := Type. +Definition Type1 := Type : Type2. + +(** Assumption of a retract from Type into Prop *) + +Variable down : Type1 -> Prop. +Variable up : Prop -> Type1. + +Hypothesis back : forall A, up (down A) -> A. + +Hypothesis forth : forall A, A -> up (down A). + +Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A), + P (back A (forth A a)) -> P a. + +Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A), + P a -> P (back A (forth A a)). + +(** Proof *) + +Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop. +Definition U : Type1 := V -> Prop. + +Definition sb (z:V) : V := fun A r a => r (z A r) a. +Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)). +Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x). +Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x). +Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))). +Definition I (x:U) : Prop := + (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False. + +Lemma Omega : forall i:U -> Prop, induct i -> up (i WF). +Proof. +intros i y. +apply y. +unfold le, WF, induct. +apply forth. +intros x H0. +apply y. +unfold sb, le', le. +compute. +apply backforth_r. +exact H0. +Qed. + +Lemma lemma1 : induct (fun u => down (I u)). +Proof. +unfold induct. +intros x p. +apply forth. +intro q. +generalize (q (fun u => down (I u)) p). +intro r. +apply back in r. +apply r. +intros i j. +unfold le, sb, le', le in j |-. +apply backforth in j. +specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))). +apply q. +exact j. +Qed. + +Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False. +Proof. +intro x. +generalize (x (fun u => down (I u)) lemma1). +intro r; apply back in r. +apply r. +intros i H0. +apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))). +unfold le, WF in H0. +apply back in H0. +exact H0. +Qed. + +Theorem paradox : False. +Proof. +exact (lemma2 Omega). +Qed. + +End Hurkens. + +Definition informative (x : bool) := + match x with + | true => Type + | false => Prop + end. + +Definition depsort (T : Type) (x : bool) : informative x := + match x with + | true => T + | false => True + end. + +(* The projection prop should not be definable *) +Set Primitive Projections. +Record Box (T : Type) : Prop := wrap {prop : T}. + +Definition down (x : Type) : Prop := Box x. +Definition up (x : Prop) : Type := x. + +Fail Definition back A : up (down A) -> A := @prop A. diff --git a/test-suite/bugs/opened/3301.v b/test-suite/bugs/opened/3301.v deleted file mode 100644 index 955cfc3aa0..0000000000 --- a/test-suite/bugs/opened/3301.v +++ /dev/null @@ -1,120 +0,0 @@ -Section Hurkens. - -Definition Type2 := Type. -Definition Type1 := Type : Type2. - -(** Assumption of a retract from Type into Prop *) - -Variable down : Type1 -> Prop. -Variable up : Prop -> Type1. - -Hypothesis back : forall A, up (down A) -> A. - -Hypothesis forth : forall A, A -> up (down A). - -Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A), - P (back A (forth A a)) -> P a. - -Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A), - P a -> P (back A (forth A a)). - -(** Proof *) - -Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop. -Definition U : Type1 := V -> Prop. - -Definition sb (z:V) : V := fun A r a => r (z A r) a. -Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)). -Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x). -Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x). -Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))). -Definition I (x:U) : Prop := - (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False. - -Lemma Omega : forall i:U -> Prop, induct i -> up (i WF). -Proof. -intros i y. -apply y. -unfold le, WF, induct. -apply forth. -intros x H0. -apply y. -unfold sb, le', le. -compute. -apply backforth_r. -exact H0. -Qed. - -Lemma lemma1 : induct (fun u => down (I u)). -Proof. -unfold induct. -intros x p. -apply forth. -intro q. -generalize (q (fun u => down (I u)) p). -intro r. -apply back in r. -apply r. -intros i j. -unfold le, sb, le', le in j |-. -apply backforth in j. -specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))). -apply q. -exact j. -Qed. - -Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False. -Proof. -intro x. -generalize (x (fun u => down (I u)) lemma1). -intro r; apply back in r. -apply r. -intros i H0. -apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))). -unfold le, WF in H0. -apply back in H0. -exact H0. -Qed. - -Theorem paradox : False. -Proof. -exact (lemma2 Omega). -Qed. - -End Hurkens. - -Definition informative (x : bool) := - match x with - | true => Type - | false => Prop - end. - -Definition depsort (T : Type) (x : bool) : informative x := - match x with - | true => T - | false => True - end. - -(* The projection prop should not be definable *) -Set Primitive Projections. -Record Box (T : Type) : Prop := wrap {prop : T}. - -Definition down (x : Type) : Prop := Box x. -Definition up (x : Prop) : Type := x. - -Definition back A : up (down A) -> A := @prop A. - -Definition forth A : A -> up (down A) := wrap A. - -Definition backforth (A:Type) (P:A->Type) (a:A) : - P (back A (forth A a)) -> P a := fun H => H. - -Definition backforth_r (A:Type) (P:A->Type) (a:A) : - P a -> P (back A (forth A a)) := fun H => H. - -Theorem pandora : False. -apply (paradox down up back forth backforth backforth_r). -Qed. - -Print Assumptions pandora. -(* Closed under the global context *) -- cgit v1.2.3