From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/1925.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 test-suite/bugs/closed/1925.v (limited to 'test-suite/bugs/closed/1925.v') diff --git a/test-suite/bugs/closed/1925.v b/test-suite/bugs/closed/1925.v new file mode 100644 index 00000000..4caee1c3 --- /dev/null +++ b/test-suite/bugs/closed/1925.v @@ -0,0 +1,22 @@ +(* Check that the analysis of projectable rel's in an evar instance is up to + aliases *) + +Require Import List. + +Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := + fun x : A => g(f x). + +Definition map_fuse' : + forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), + (map g (map f xs)) = map (compose _ _ _ g f) xs + := + fun A B C g f => + (fix loop (ys : list A) {struct ys} := + match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys + with + | nil => refl_equal nil + | x :: xs => + match loop xs in eq _ a return eq _ ((g (f x)) :: a) with + | refl_equal => refl_equal (map g (map f (x :: xs))) + end + end). -- cgit v1.2.3