Theorem Prover Advent Calendar day 15.

map_advent_2014.v

Set Implicit Arguments.
Unset Strict Implicit.

Require Import setoid_advent_2014.

Structure Map (X Y: Setoid) :=
  {
    map_body:> X -> Y;

    prf_Map:> Proper ((==) ==> (==)) map_body
  }.
Existing Instance prf_Map.
Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" := 
  (makeMap (fun x => .. (makeMap (fun y => p)) ..))
    (at level 200, x binder, y binder, right associativity,
     format "'[' [ x .. y :-> '/ ' p ] ']'").

Program Definition eq_Map
        (A B: Type)(f: A -> B): Map (eq_Setoid A) (eq_Setoid B) :=
  [ x :-> f x ].

Definition fun_Map
        {X Y Z W: Type}(F: (X -> Y) -> (Z -> W))
: Map (fun_Setoid X Y) (fun_Setoid Z W).
  refine ([ f :-> F f ]).

unfold Proper, respectful; simpl.

intros f g Heq z.

Abort.

Definition const {A B: Type}(a: A): forall _: B, A := fun _ => a.