Quelle bug_4287.v Sprache: Coq

Unset Strict Universe Declaration.

Universe b.

Universe c.

Definition UU : Type@{b} := Type@{c}.

Module Type MT.

Definition T := Prop.
End MT.

Module M : MT.
   Definition T := Type@{b}.

Print Universes.
Fail End M.

  Reset T.
  Definition T := Prop.
End M.

Set Universe Polymorphism.

(* This is a modified version of Hurkens with all universes floating *)
Section Hurkens.

Variable down : Type -> Type.
Variable up : Type -> Type.

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 : Type := forall A:Type, ((up A -> Type) -> up A -> Type) -> up A -> Type.
Definition U : Type := V -> Type.

Definition sb (z:V) : V := fun A r a => r (z A r) a.
Definition le (i:U -> Type) (x:U) : Type := x (fun A r a => i (fun v => sb v A r a)).
Definition le' (i:up (down U) -> Type) (x:up (down U)) : Type := le (fun a:U => i (forth _ a)) (back _ x).
Definition induct (i:U -> Type) : Type := 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) : Type :=
  (forall i:U -> Type, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False.

Lemma Omega : forall i:U -> Type, 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 -> Type, 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.

Polymorphic Record box (T : Type) := wrap {unwrap : T}.

(* Here we instantiate to Set *)

Fail Definition down (x : Type) : Prop := box x.
Definition up (x : Prop) : Type := x.

Fail Definition back A : up (down A) -> A := unwrap A.

Fail Definition forth A : A -> up (down A) := wrap A.

Definition id {A : Type} (a : A) := a.
Definition setlt (A : Type@{i}) :=
  let foo := Type@{i} : Type@{j} in True.

Definition setle (B : Type@{i}) :=
  let foo (A : Type@{j}) := A in foo B.

Fail Check @setlt@{j Prop}.
Fail Definition foo := @setle@{j Prop}.
Check setlt@{Set i}.
Check setlt@{Set j}.

quality99%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.