summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1925.v
blob: 4caee1c36d90eba51758d18322e2a16565db5149 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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).