Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Theorem Prover Advent Calendar day 15.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment