Library nominal


Require Import Setoid.

Require Import basics.
Require Import categories.
Require Import preord.
Require Import sets.
Require Import finsets.
Require Import atoms.
Require Import permutations.

The category of nominal types


Obligation Tactic := intuition.

Require Import List.

Module Nominal.

Record mixin_of (A:Type) (eq_mixin:Eq.mixin_of A) :=
  Mixin
  { Aeq := Eq.Pack A eq_mixin
  ; papp : perm -> Aeq -> Aeq
  ; support : Aeq -> finset atom
  ; nom_ident : forall a, papp id a a
  ; nom_comp : forall a p1 p2,
       papp p1 (papp p2 a) papp (p1 p2) a
  ; papp_respects : forall p p' a a',
       p p' -> a a' -> papp p a papp p' a'
  ; support_axiom : forall (p:perm) a,
       (forall v, v support a -> v Perm.support p -> False) ->
       papp p a a
  ; support_papp : forall (p:perm) x v,
       v support x <-> p v support (papp p x)
  }.

Record ob :=
  Ob
  { carrier :> Type
  ; eq_mixin : Eq.mixin_of carrier
  ; nominal_mixin : mixin_of carrier eq_mixin
  }.

Definition papp_op (A:ob) : perm -> A -> A :=
  papp (carrier A) (eq_mixin A) (nominal_mixin A).

Definition support_op (A:ob) : A -> finset atom :=
  support (carrier A) (eq_mixin A) (nominal_mixin A).

Canonical Structure nom_support (A:ob) : supported :=
  Supported A (support_op A).

Canonical Structure ob_eq (A:ob) : Eq.type :=
  Eq.Pack (carrier A) (eq_mixin A).

Record hom (A B:ob) :=
  Hom
  { map :> carrier A -> carrier B
  ; eq_axiom : forall x y, x y -> map x map y
  ; equivariant : forall x (p:perm),
       map (papp_op A p x) papp_op B p (map x)
  }.

Program Definition ident (A:ob) :=
  Hom A A (fun x => x) _ _.

Program Definition compose (A B C:ob) (f:hom B C) (g:hom A B) :=
  Hom A C (fun x => f (g x)) _ _.

Definition comp_mixin : Comp.mixin_of ob hom :=
  Comp.Mixin ob hom ident compose.

Canonical Structure comp := Comp.Pack ob hom comp_mixin.

Program Definition hom_eq_mixin (A B:ob) : Eq.mixin_of (hom A B) :=
  Eq.Mixin (hom A B) (fun f g => forall x, f x g x) _ _ _.

Lemma category_axioms : Category.axioms ob hom hom_eq_mixin comp_mixin.

Canonical Structure NOMINAL : category :=
  Category ob hom hom_eq_mixin comp_mixin category_axioms.

Canonical Structure eq (A:ob) : Eq.type := Eq.Pack (carrier A) (eq_mixin A).
Canonical Structure hom_eq (A B:ob) : Eq.type := Eq.Pack (hom A B) (hom_eq_mixin A B).

End Nominal.

Notation NOMINAL := Nominal.NOMINAL.
Notation nominal := Nominal.ob.
Canonical Structure NOMINAL.
Canonical Structure Nominal.nom_support.
Canonical Structure Nominal.eq.
Canonical Structure Nominal.hom_eq.
Canonical Structure Nominal.comp.
Coercion Nominal.carrier : Nominal.ob >-> Sortclass.
Coercion Nominal.map : Nominal.hom >-> Funclass.

Notation "p · x" := (Nominal.papp_op _ p x) (at level 35, right associativity).

Add Parametric Morphism (A B:nominal) :
  (Nominal.map A B)
    with signature (eq_op (Nominal.hom_eq A B)) ==>
                   (eq_op (Nominal.eq A)) ==>
                   (eq_op (Nominal.eq B))
   as nom_map_morphism.

Add Parametric Morphism (A:nominal) :
  (Nominal.papp_op A)
  with signature (@eq_op (Perm.eq tt tt)) ==>
                 (@eq_op (Nominal.eq A)) ==>
                 (@eq_op (Nominal.eq A))
    as papp_morphism.

Lemma nom_compose (A:nominal) (p1 p2:perm) (x:A) :
  p1 · p2 · x (p1 p2) · x.

Lemma nom_compose' (A:nominal) (p p1 p2:perm) (x:A) :
  p1 p2 p ->
  p1 · p2 · x p · x.

Lemma nom_ident (A:nominal) (x:A) :
  id·x x.

Lemma nom_ident' (A:nominal) (p:perm) (x:A) :
  p id(tt) ->
  p·x x.

Lemma support_axiom (A:nominal) (p:perm) (x:A) :
  xp -> p·x x.

Lemma support_axiom' (A:nominal) (p:perm) (x:A) :
  xp -> x p·x.

Lemma support_papp (A:nominal) (p:perm) (x:A) (v:atom) :
  v x <-> p v p·x.

Lemma papp_inj (A:nominal) (p:perm) (x y:A) :
  p·x p·y -> x y.

NOMINAL is an initialized category.

Program Definition initius_eq_mixin :=
  Eq.Mixin False (fun _ _ => False) _ _ _.

Program Definition initius_mixin :=
  Nominal.Mixin
      False initius_eq_mixin
      (fun p x => False_rect _ x)
      (fun x => False_rect _ x)
      _ _ _ _ _.

Canonical Structure initius :=
  Nominal.Ob False initius_eq_mixin initius_mixin.

Program Definition initiate (A:nominal) : initius A :=
  Nominal.Hom initius A (fun x => False_rect _ x) _ _.

Program Definition initialized_mixin :=
  Initialized.Mixin
    Nominal.ob Nominal.hom
    Nominal.hom_eq_mixin
    initius initiate
    _.

Canonical Structure initialized_nominal : initialized :=
  Initialized
    Nominal.ob Nominal.hom
    Nominal.hom_eq_mixin
    Nominal.comp_mixin
    Nominal.category_axioms
    initialized_mixin.

NOMINAL has binary coproducts.

Section nom_sum.
  Variables A B:nominal.

  Definition nom_sum_equiv (x y:A+B) :=
    match x, y with
    | inl a, inl a' => a a'
    | inr b, inr b' => b b'
    | _, _ => False
    end.

  Definition nom_sum_papp (p:perm) (x:A+B) :=
    match x with
    | inl a => inl (p · a)
    | inr b => inr (p · b)
    end.

  Definition nom_sum_support (x:A+B) : finset atom :=
    match x with
    | inl a => a
    | inr b => b
    end.

  Program Definition nom_sum_eq_mixin :=
    Eq.Mixin (A+B) nom_sum_equiv _ _ _.

  Program Definition nom_sum_mixin :=
    Nominal.Mixin (A+B) nom_sum_eq_mixin nom_sum_papp nom_sum_support
       _ _ _ _ _.

  Canonical Structure nom_sum : nominal :=
    Nominal.Ob (A+B) nom_sum_eq_mixin nom_sum_mixin.
End nom_sum.

NOMINAL has colimits for directed systems.
Require Import directed.
Require Import cont_functors.

Section nominal_directed_colimits.
  Variable I:directed_preord.
  Variable DS:directed_system I NOMINAL.

  Record nom_colimit_type :=
    NomColim
    { nom_colim_idx : I
    ; nom_colim_elem : ds_F DS nom_colim_idx
    }.

  Definition nom_colimit_equiv (x y:nom_colimit_type) :=
    exists k
      (Hxk:nom_colim_idx x k)
      (Hyk:nom_colim_idx y k),
      ds_hom DS _ _ Hxk (nom_colim_elem x)
      ds_hom DS _ _ Hyk (nom_colim_elem y).

  Program Definition nom_colimit_eq_mixin :=
    Eq.Mixin nom_colimit_type nom_colimit_equiv _ _ _ .

  Definition nom_colimit_papp (p:perm) (x:nom_colimit_type) :=
    match x with
    | NomColim i x' => NomColim i (p · x')
    end.

  Program Definition nom_colimit_mixin :=
    Nominal.Mixin
      nom_colimit_type
      nom_colimit_eq_mixin
      nom_colimit_papp
      (fun x => nom_colim_elem x )
      _ _ _ _ _.

  Canonical Structure nom_colimit : nominal :=
    Nominal.Ob nom_colimit_type nom_colimit_eq_mixin nom_colimit_mixin.

  Program Definition nom_colimit_spoke (i:I) : ds_F DS i nom_colimit :=
    Nominal.Hom (ds_F DS i) nom_colimit (NomColim i) _ _.

  Program Definition nom_colimit_cocone : cocone DS :=
    Cocone DS nom_colimit nom_colimit_spoke _.

  Section nom_colimit_univ.
    Variable YC:cocone DS.

    Definition nom_colimit_univ_defn (x:nom_colimit) : cocone_point YC :=
      match x with
      | NomColim i x' => cocone_spoke YC i x'
      end.

    Program Definition nom_colimit_univ : nom_colimit cocone_point YC :=
      Nominal.Hom nom_colimit (cocone_point YC) nom_colimit_univ_defn _ _.

    Lemma nom_colimit_commute : forall i,
      cocone_spoke YC i nom_colimit_univ nom_colimit_spoke i.

    Lemma nom_colimit_uniq : forall (f:nom_colimit YC),
      (forall i, cocone_spoke YC i f nom_colimit_spoke i) ->
      f nom_colimit_univ.
  End nom_colimit_univ.

  Definition nom_has_colimits : directed_colimit DS nom_colimit_cocone
    := DirectedColimit DS nom_colimit_cocone
         nom_colimit_univ nom_colimit_commute nom_colimit_uniq.
End nominal_directed_colimits.

NOMINAL has least fixpoints of continuous functors.
NOMINAL is a terminated category.

Program Definition nom_terminus_eq_mixin :=
  Eq.Mixin unit (fun _ _ => True) _ _ _.

Program Definition nom_terminus_mixin :=
  Nominal.Mixin unit nom_terminus_eq_mixin (fun p u => u) (fun _ => nil) _ _ _ _ _.

Canonical Structure nom_terminus : nominal :=
  Nominal.Ob unit nom_terminus_eq_mixin nom_terminus_mixin.

Program Definition nom_terminate (A:nominal) : A nom_terminus :=
  Nominal.Hom A nom_terminus (fun _ => tt) _ _.

Program Definition nom_terminated_mixin :=
  Terminated.Mixin
    Nominal.ob Nominal.hom
    Nominal.hom_eq_mixin
    nom_terminus nom_terminate _.

Canonical Structure nom_terminated :=
  Terminated
    Nominal.ob Nominal.hom
    Nominal.hom_eq_mixin
    Nominal.comp_mixin
    Nominal.category_axioms
    nom_terminated_mixin.

NOMINAL is a cartesian category.
Program Definition nom_prod_eq_mixin (A B :nominal) :=
   Eq.Mixin (A*B) (fun x y => fst x fst y /\ snd x snd y) _ _ _.
Solve Obligations using intuition eauto.

Program Definition nom_prod_mixin (A B:nominal) :=
  Nominal.Mixin (A*B) (nom_prod_eq_mixin A B)
     (fun p xy => (p · fst xy, p · snd xy))
     (fun xy => fst xy ++ snd xy)
     _ _ _ _ _.

Canonical Structure nom_prod (A B:nominal) : nominal :=
  Nominal.Ob (A*B) (nom_prod_eq_mixin A B) (nom_prod_mixin A B).

Program Definition nom_pi1 (A B:nominal) : nom_prod A B A :=
  Nominal.Hom (nom_prod A B) A (fun x => fst x) _ _.

Program Definition nom_pi2 (A B:nominal) : nom_prod A B B :=
  Nominal.Hom (nom_prod A B) B (fun x => snd x) _ _.

Program Definition nom_pairing (C A B:nominal) (f:C A) (g:C B) : C nom_prod A B
  := Nominal.Hom C (nom_prod A B) (fun c => (f c, g c)) _ _.

Program Definition nom_cartesian_mixin :=
  Cartesian.Mixin
    Nominal.ob Nominal.hom
    Nominal.hom_eq_mixin
    Nominal.comp_mixin
    nom_prod nom_pi1 nom_pi2 nom_pairing
    _.

Canonical Structure nom_cartesian : cartesian :=
  Cartesian
     Nominal.ob Nominal.hom
     Nominal.hom_eq_mixin
     Nominal.comp_mixin
     Nominal.category_axioms
     nom_terminated_mixin
     nom_cartesian_mixin.

NOMINAL is a cartesian closed category.

Record nom_exp_type (A B:nominal) :=
  NomExp
  { exp_map :> A -> B
  ; exp_support : finset atom
  ; exp_eq_axiom : forall x y, x y -> exp_map x exp_map y
  ; exp_support_axiom : forall (p:perm),
       (forall v, v exp_support -> v p -> False) ->
       (forall x, p · exp_map (p⁻¹ · x) exp_map x)
  }.

Program Definition exp_papp (A B:nominal) (p:perm) (f:nom_exp_type A B) :
  nom_exp_type A B :=
  NomExp A B
    (fun x => p · f (p⁻¹ · x))
    (List.map p (exp_support A B f))
    _ _.

Program Definition nom_exp_eq_mixin (A B:nominal) :=
  Eq.Mixin (nom_exp_type A B) (fun f g => forall x, f x g x) _ _ _.

Canonical Structure nom_exp_eq (A B:nominal) :=
  Eq.Pack (nom_exp_type A B) (nom_exp_eq_mixin A B).

Add Parametric Morphism (A B:nominal) :
  (exp_map A B)
  with signature (eq_op (nom_exp_eq A B)) ==>
                 (eq_op (Nominal.ob_eq A)) ==>
                 (eq_op (Nominal.ob_eq B))
   as exp_map_morphism.

Program Definition nom_exp_mixin (A B:nominal) :=
  Nominal.Mixin
  (nom_exp_type A B)
  (nom_exp_eq_mixin A B)
  (exp_papp A B)
  (exp_support A B)
  _ _ _ _ _.

Canonical Structure nom_exp (A B:nominal) : nominal :=
  Nominal.Ob
    (nom_exp_type A B)
    (nom_exp_eq_mixin A B)
    (nom_exp_mixin A B).

Program Definition nom_curry (C A B:nominal) (f:C×A B) : C nom_exp A B :=
  Nominal.Hom C (nom_exp A B)
     (fun c => NomExp A B (fun a => f (c,a)) (c) _ _) _ _.

Program Definition nom_apply (A B:nominal) : nom_exp A B × A B :=
  Nominal.Hom (nom_exp A B × A) B (fun fx => fst fx (snd fx)) _ _.

Program Definition nom_ccc_mixin :=
  CartesianClosed.Mixin
    Nominal.ob Nominal.hom
    Nominal.hom_eq_mixin
    Nominal.comp_mixin
    Nominal.category_axioms
    nom_terminated_mixin
    nom_cartesian_mixin
    nom_exp nom_curry nom_apply
    _.

Canonical Structure nom_ccc : cartesian_closed :=
  CartesianClosed
     Nominal.ob Nominal.hom
     Nominal.hom_eq_mixin
     Nominal.comp_mixin
     Nominal.category_axioms
     nom_cartesian_mixin
     nom_terminated_mixin
     nom_ccc_mixin.

Atom binding construct.

Inductive binding_ty (A:nominal) :=
  | bind : atom -> A -> binding_ty A.

Notation "'ν' x , t" := (bind _ x t) (at level 50, format "'ν' x , t").

Definition binding_equiv (A:nominal) (x y:binding_ty A) :=
  let (v, x') := x in
  let (w, y') := y in
    exists u:atom, u (v :: w :: x' ++ y' : finset atom) /\
      u v · x' u w · y'.

Lemma binding_equiv_forall (A:nominal) (x y:binding_ty A) (avoid : finset atom):
  binding_equiv A x y <->
  let (v,x') := x in
  let (w,y') := y in
  forall u,
      u (v :: w :: x' ++ y' : finset atom) ->
      u avoid ->
      u v · x' u w · y'.

Program Definition binding_eq_mixin (A:nominal) : Eq.mixin_of (binding_ty A) :=
  Eq.Mixin (binding_ty A) (binding_equiv A) _ _ _.

Canonical Structure binding_eq (A:nominal) :=
  Eq.Pack (binding_ty A) (binding_eq_mixin A).

Definition binding_papp (A:nominal) (p:perm) (x:binding_ty A) :=
  match x with
  | ν a, x' => ν (p a), (p·x')
  end.

Definition binding_support (A:nominal) (x:binding_ty A) :=
  match x with
  | ν a, x' => finset_remove atom_dec (x') a
  end.

Program Definition binding_nominal_mixin (A:nominal) :=
  Nominal.Mixin
    (binding_ty A)
    (binding_eq_mixin A)
    (binding_papp A)
    (binding_support A)
    _ _ _ _ _.

Canonical Structure binding (A:nominal) : nominal :=
  Nominal.Ob (binding_ty A) (binding_eq_mixin A) (binding_nominal_mixin A).

binding induces an endofunctor on NOMINAL.

Definition binding_fmap_defn (A B:nominal) (f:A B)
  (x:binding A) : binding B :=
  match x with
  | ν a, x' => ν a, (f x')
  end.

Program Definition binding_fmap (A B:nominal) (f:A B) : binding A binding B :=
  Nominal.Hom (binding A) (binding B) (binding_fmap_defn A B f) _ _.


Lemma binding_fmap_ident (A:nominal) :
  binding_fmap A A id(A) id(binding A).

Lemma binding_fmap_compose (A B C:nominal) f g :
  binding_fmap B C f binding_fmap A B g binding_fmap A C (f g).

Lemma binding_fmap_respects (A B:nominal) (f f':A B) :
  f f' -> binding_fmap A B f binding_fmap A B f'.

Program Definition bindingF : functor NOMINAL NOMINAL :=
  Functor NOMINAL NOMINAL
     binding binding_fmap _ _ _.