From 84916b37627cce78a313f850ecbcff1c3b8c3d49 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 4 Sep 2014 11:24:40 +0200 Subject: Fix bug #3559, ensuring a canonical order of universe level quantifications when introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet. --- test-suite/bugs/closed/3559.v | 88 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 test-suite/bugs/closed/3559.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v new file mode 100644 index 000000000..a193f3888 --- /dev/null +++ b/test-suite/bugs/closed/3559.v @@ -0,0 +1,88 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *) +(* File reduced by coq-bug-finder from original input, then from 8657 lines to +4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines, +then from 51 lines to 37 lines, then from 43 lines to 30 lines *) +(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml +4.01.0 + coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk +(437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *) +Require Import Coq.Init.Notations. +Set Universe Polymorphism. +Generalizable All Variables. +Record prod A B := pair { fst : A ; snd : B }. +Arguments pair {_ _} _ _. +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Reserved Notation "x <-> y" (at level 95, no associativity). +Reserved Notation "x = y" (at level 70, no associativity). +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Open Scope type_scope. + +Definition iff A B := prod (A -> B) (B -> A). +Infix "<->" := iff : type_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = +y" := (@paths _ x y) : type_scope. +Class Contr_internal (A : Type) := { center : A ; contr : (forall y : A, center += y) }. +Inductive trunc_index : Type := minus_two | trunc_S (_ : trunc_index). +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type@{i}) : Type@{i} := + match n with + | minus_two => Contr_internal A + | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) + end. +Notation minus_one:=(trunc_S minus_two). +Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : +IsTrunc_internal n A. +Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) : +IsTrunc n (x = y) := H x y. + +Axiom cheat : forall {A}, A. + +Lemma paths_lift (A : Type@{i}) (x y : A) (p : x = y) : paths@{j} x y. +Proof. + destruct p. apply idpath. +Defined. + +Lemma paths_change (A : Type@{i}) (x y : A) : paths@{j} x y = paths@{i} x y. +Proof. (* require Univalence *) + apply cheat. +Defined. + +Lemma IsTrunc_lift (n : trunc_index) : + forall (A : Type@{i}), IsTrunc_internal@{i} n A -> IsTrunc_internal@{j} n A. +Proof. + induction n; simpl; intros. + destruct X. exists center0. intros. apply (paths_lift _ _ _ (contr0 y)). + + rewrite paths_change. + apply IHn, X. +Defined. + +Notation IsHProp := (IsTrunc minus_one). +(* Record hProp := hp { hproptype :> Type ; isp : IsTrunc minus_one hproptype}. *) +(* Make the truncation proof polymorphic, i.e., available at any level greater or equal + to the carrier type level j *) +Record hProp := hp { hproptype :> Type@{j} ; isp : IsTrunc minus_one hproptype}. +Axiom path_iff_hprop_uncurried : forall `{IsHProp A, IsHProp B}, (A <-> B) -> A += B. +Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V. +Axiom is0trunc_V : IsTrunc (trunc_S (trunc_S minus_two)) V. +Axiom bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}. +Axiom bisimulation_refl : forall (v : V), bisimulation v v. +Axiom bisimulation_eq : forall (u v : V), bisimulation u v -> u = v. +Notation "u ~~ v" := (bisimulation u v) (at level 30). +Lemma bisimulation_equals_id : forall u v : V@{i j}, (u = v) = (u ~~ v). +Proof. + intros u v. + refine (@path_iff_hprop_uncurried _ _ _ _ _). +(* path_iff_hprop_uncurried : *) +(* forall A : Type@{Top.74}, *) +(* IsHProp A -> forall B : Type@{Top.74}, IsHProp B -> A <-> B -> A = B *) +(* (* Top.74 *) +(* Top.78 |= Top.74 < Top.78 *) +(* *) *) + + Show Universes. + exact (isp _). + split; intros. destruct X. apply bisimulation_refl. + apply bisimulation_eq, X. +Defined. -- cgit v1.2.3