diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_8785.v | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v new file mode 100644 index 0000000000..b10569499e --- /dev/null +++ b/test-suite/bugs/closed/bug_8785.v @@ -0,0 +1,44 @@ +Universe u v w. +Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := . + +Inductive FiniteT : Type -> Prop := + | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T) + | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X -> + invertible f -> FiniteT Y. + +Set Printing Universes. + +Axiom a : False. +(* +Constraint v <= u. +Constraint v <= w. +*) +Lemma finite_subtype: forall (X:Type) (P:X->Prop), + FiniteT X -> (forall x:X, P x \/ ~ P x) -> + FiniteT {x:X | P x}. +Proof. +intros. +induction H. + +destruct (H0 None). +elim a. + +pose (g := fun (x:{x:T | P (Some x)}) => + match x return {x:option T | P x} with + | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +pose (g := fun (x:{x:X | P (f x)}) => + match x with + | exist _ x0 i => exist (fun x:Y => P x) (f x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +Qed. |