diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_055.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_055.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v new file mode 100644 index 00000000..92d70ad1 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_055.v @@ -0,0 +1,53 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +Set Universe Polymorphism. + +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'. + + admit. +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) + + (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) + ((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 with + | inl y' => ap g + | inr y' => idmap + end + | inr x' => match y with + | inl y' => idmap + | inr y' => ap h + end + end) pq). + +Admitted. +(* Toplevel input, characters 20-29: +Error: Matching on term "f y" of type "A' + B'" expects 2 branches. *) |