diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/HoTT_coq_054.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_054.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_054.v | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v new file mode 100644 index 00000000..c6879659 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_054.v @@ -0,0 +1,94 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) +Inductive Empty : Prop := . + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Arguments idpath {A a} , [A] a. + +Definition idmap {A : Type} : A -> A := fun x => x. + +Definition path_sum {A B : Type} (z z' : A + B) + (pq : match z, z' with + | inl z0, inl z'0 => z0 = z'0 + | inr z0, inr z'0 => z0 = z'0 + | _, _ => Empty + end) +: z = z'. + destruct z, z', pq; exact idpath. +Defined. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B) + (* Fortunately, this unifies properly *) + (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) : + let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in + ap f (path_sum x y pq) = path_sum (f x) (f y) + (* Coq appears to require *ALL* of the annotations *) + ((match x as x return match (x, y) with + (inl x', inl y') => x' = y' + | (inr x', inr y') => x' = y' + | _ => Empty + end -> match (f x, f y) with + | (inl x', inl y') => x' = y' + | (inr x', inr y') => x' = y' + | _ => Empty end with + | inl x' => match y as y return match y with + inl y' => x' = y' + | _ => Empty + end -> match f y with + | inl y' => g x' = y' + | _ => Empty end with + | inl y' => ap g + | inr y' => idmap + end + | inr x' => match y as y return match y return Prop with + inr y' => x' = y' + | _ => Empty + end -> match f y return Prop with + | inr y' => h x' = y' + | _ => Empty end with + | inl y' => idmap + | inr y' => ap h + end + end) pq). + destruct x; destruct y; destruct pq; reflexivity. +Qed. +(* Toplevel input, characters 1367-1374: +Error: +In environment +A : Type +B : Type +A' : Type +B' : Type +g : A -> A' +h : B -> B' +x : A + B +y : A + B +pq : +match x with +| inl x' => match y with + | inl y' => x' = y' + | inr _ => Empty + end +| inr x' => match y with + | inl _ => Empty + | inr y' => x' = y' + end +end +f := +fun z : A + B => +match z with +| inl z' => inl (g z') +| inr z' => inr (h z') +end : A + B -> A' + B' +x' : B +y0 : A + B +y' : B +The term "x' = y'" has type "Type" while it is expected to have type +"Prop" (Universe inconsistency). *) |