Library models.Coherence
Require Import ProofIrrelevance.
Require Import FunctionalExtensionality.
Require Import PropExtensionality.
Require Import Relations.
Require Import RelationClasses.
Require Import List.
Require Import FunctionalExtensionality.
Require Import PropExtensionality.
Require Import Relations.
Require Import RelationClasses.
Require Import List.
Record space :=
{
token : Type;
coh: relation token;
coh_refl: Reflexive coh;
coh_symm: Symmetric coh;
}.
Arguments coh {_}.
Existing Instance coh_refl.
Existing Instance coh_symm.
Bind Scope coh_scope with space.
Delimit Scope coh_scope with coh.
Record clique (A : space) :=
{
has : token A → Prop;
has_coh a b : has a → has b → coh a b;
}.
Arguments has {A}.
Bind Scope clique_scope with clique.
Delimit Scope clique_scope with clique.
Open Scope clique_scope.
(* Points are ordered by inclusion and form a DCPPO. *)
Definition ref {A} : relation (clique A) :=
fun x y ⇒ ∀ a, has x a → has y a.
Instance ref_preo A :
PreOrder (@ref A).
Instance ref_po A :
Antisymmetric (clique A) eq (@ref A).
Definition directed {A I} (x : I → clique A) :=
∀ i j, ∃ y, ∀ z, ref (x i) z ∧ ref (x j) z ↔ ref y z.
Program Definition lim {A I} (x : I → clique A) (Hx : directed x) :=
{|
has a := ∃ i, has (x i) a;
|}.
Lemma lim_sup {A I} (x : I → clique A) (Hx : directed x) (y : clique A) :
(∀ i, ref (x i) y) ↔ ref (lim x Hx) y.
Basic categorical structure
Linear maps
Definition
Program Definition lmap (A B : space) : space :=
{|
token := token A × token B;
coh '(a1, b1) '(a2, b2) :=
coh a1 a2 → coh b1 b2 ∧ (b1 = b2 → a1 = a2);
|}.
Infix "--o" := lmap (at level 55, right associativity) : coh_scope.
Notation "A --o B" := (clique (A --o B)) : type_scope.
Lemma lmap_coh {A B} (f : A --o B) (a1 a2 : token A) (b1 b2 : token B) :
coh a1 a2 → has f (a1, b1) → has f (a2, b2) → coh b1 b2.
Lemma lmap_det {A B} (f : A --o B) (a1 a2 : token A) (b1 b2 : token B) :
coh a1 a2 → has f (a1, b1) → has f (a2, b2) → b1 = b2 → a1 = a2.
Lemma lmap_ext {A B} (f g : A --o B):
(∀ x y, has f (x, y) ↔ has g (x, y)) → f = g.
The "pairwise coherent" obligation generated when defining linear
maps can often be discharged using the following tactic.
Ltac process_obligation :=
intros;
repeat match goal with x : _ × _ |- _ ⇒ destruct x end;
firstorder
(subst;
eauto using lmap_coh, lmap_det, has_coh, (reflexivity (R:=coh));
try congruence).
Program Definition lmap_id {A : space} : A --o A :=
{|
has '(x, y) := x = y;
|}.
Program Definition lmap_compose {A B C} (g : B --o C) (f : A --o B) : A --o C :=
{|
has '(x, z) := ∃ y, has f (x, y) ∧ has g (y, z);
|}.
Infix "@" := lmap_compose (at level 30, right associativity) : clique_scope.
Lemma lmap_compose_id_left {A B} (f : A --o B) :
f @ lmap_id = f.
Lemma lmap_compose_id_right {A B} (f : A --o B) :
lmap_id @ f = f.
Lemma lmap_compose_assoc {A B C D} (h : C --o D) (g : B --o C) (f : A --o B) :
(h @ g) @ f = h @ (g @ f).
Action on cliques
Program Definition lmap_apply {A B} (f : A --o B) (x : clique A) : clique B :=
{|
has b := ∃ a, has x a ∧ has f (a, b);
|}.
Lemma lmap_apply_id {A} (x : clique A) :
lmap_apply lmap_id x = x.
Lemma lmap_apply_compose {A B C} (f : A --o B) (g : B --o C) (x : clique A) :
lmap_apply (g @ f) x = lmap_apply g (lmap_apply f x).
(*
Record liso (A B : space) :=
{
liso_of :> A -> B -> Prop;
liso_coh a1 a2 b1 b2 :
liso_of a1 b1 ->
liso_of a2 b2 ->
(coh a1 a2 <-> coh b1 b2) /\
(a1 = a2 <-> b1 = b2)
}.
Arguments liso_of {A B}.
Infix "~=" := liso (at level 70, right associativity) : type_scope.
Program Definition li_fw {A B} (f : A ~= B) :=
{|
lmaps := liso_of f;
|}.
Next Obligation.
destruct f as f Hf; cbn in *.
destruct (Hf a1 a2 b1 b2) as ? ?; auto.
firstorder.
Qed.
Program Definition li_bw {A B} (f : A ~= B) :=
{|
lmaps x y := liso_of f y x;
|}.
Next Obligation.
destruct f as f Hf; cbn in *.
destruct (Hf b1 b2 a1 a2) as ? ?; auto.
firstorder.
Qed.
Lemma li_bw_fw {A B} (f : A ~= B) :
li_fw f @ li_bw f = lmap_id.
Proof.
apply lmap_ext; intros x y.
destruct f as f Hf; cbn in *.
split.
- intros (b & Hxb & Hby). cbn in *.
destruct (Hf b b x y); auto. firstorder.
- intros . exists x.
apply liso_coh.
*)
Simple constructions
Output
Program Definition output (X : Type) :=
{|
token := X;
coh := eq;
|}.
Program Definition omap {X Y} (f : X → Y) : output X --o output Y :=
{|
has '(x, y) := f x = y;
|}.
Lemma omap_id X :
omap (fun x:X ⇒ x) = lmap_id.
Lemma omap_compose {X Y Z} (f : X → Y) (g : Y → Z) :
omap (fun x:X ⇒ g (f x)) = omap g @ omap f.
In fact, output is the left adjoint to clique. Here we give a
characterization in terms of universal morphisms.
Program Definition oret {A} (a : A) : clique (output A) :=
{|
has := eq a;
|}.
Program Definition oext {A B} (f : A → clique B) : output A --o B :=
{|
has '(a, b) := has (f a) b;
|}.
Lemma oext_oret {A B} (f : A → clique B) (a : A) :
lmap_apply (oext f) (oret a) = f a.
Lemma oext_uniq {A B} (f : A → clique B) (g : output A --o B) :
(∀ a, lmap_apply g (oret a) = f a) →
g = oext f.
Here we could prove some consequences, in particular the
isomorphisms between output (A + B) and output A + output B,
and between clique (A && B) and clique A × clique B.
A contravariant functor from Set. Here the domain we obtain is
essentially the powerset of X. For what its worth I believe the
adjoint is the "coclique" contravariant functor clique @ lneg.
Input
Program Definition input (X : Type) :=
{|
token := X;
coh x1 x2 := True;
|}.
Program Definition imap {X Y} (f : X → Y) : input Y --o input X :=
{|
has '(y, x) := f x = y;
|}.
Lemma imap_id X :
imap (fun x:X ⇒ x) = lmap_id.
Lemma imap_compose {X Y Z} (f : X → Y) (g : Y → Z) :
imap (fun x:X ⇒ g (f x)) = imap f @ imap g.
Inductive csprod_coh {A B} (RA : relation A) (RB : relation B) : relation (A + B) :=
| inl_coh x y : RA x y → csprod_coh RA RB (inl x) (inl y)
| inr_coh x y : RB x y → csprod_coh RA RB (inr x) (inr y)
| inl_inr_coh x y : csprod_coh RA RB (inl x) (inr y)
| inr_inl_coh x y : csprod_coh RA RB (inr x) (inl y).
Program Definition csprod (A B : space) : space :=
{|
token := token A + token B;
coh := csprod_coh coh coh;
|}.
Infix "&&" := csprod : coh_scope.
Program Definition csp1 {A B : space} : A && B --o A :=
{|
has '(x, a) := inl a = x;
|}.
Program Definition csp2 {A B : space} : A && B --o B :=
{|
has '(x, b) := inr b = x;
|}.
Program Definition cspair {X A B: space} (f: X --o A) (g: X --o B): X --o A&&B :=
{|
has '(x, y) :=
match y with
| inl a ⇒ has f (x, a)
| inr b ⇒ has g (x, b)
end;
|}.
Notation "{ x , y }" := (cspair x y) (x at level 99) : clique_scope.
Lemma cspair_csp1 {X A B} (f : X --o A) (g : X --o B) :
csp1 @ {f, g} = f.
Lemma cspair_csp2 {X A B} (f : X --o A) (g : X --o B) :
csp2 @ {f, g} = g.
Lemma cspair_uniq {X A B} (h : X --o A && B) :
{csp1 @ h, csp2 @ h} = h.
Inductive cssum_coh {A B} (RA: relation A) (RB: relation B): relation (A + B) :=
| sum_inl_coh x y : RA x y → cssum_coh RA RB (inl x) (inl y)
| sum_inr_coh x y : RB x y → cssum_coh RA RB (inr x) (inr y).
Program Definition cssum (A B : space) : space :=
{|
token := token A + token B;
coh := cssum_coh coh coh;
|}.
Infix "+" := cssum : coh_scope.
Program Definition csi1 {A B : space} : A --o A + B :=
{|
has '(a, x) := inl a = x;
|}.
Program Definition csi2 {A B : space} : B --o A + B :=
{|
has '(b, x) := inr b = x;
|}.
Program Definition copair {A B X: space} (f: A --o X) (g: B --o X) : A+B --o X :=
{|
has '(x, y) :=
match x with
| inl a ⇒ has f (a, y)
| inr b ⇒ has g (b, y)
end;
|}.
Notation "[ x , y ]" := (copair x y) (x at level 99) : clique_scope.
Lemma copair_csi1 {A B X} (f : A --o X) (g : B --o X) :
[f, g] @ csi1 = f.
Lemma copair_csi2 {A B X} (f : A --o X) (g : B --o X) :
[f, g] @ csi2 = g.
Lemma copair_uniq {A B X} (h : A + B --o X) :
[h @ csi1, h @ csi2] = h.
Program Definition discard A : A --o csterm :=
{|
has '(x, y) := False;
|}.
Lemma discard_uniq {A} (f : A --o csterm) :
f = discard A.
Program Definition cstens (A B : space) : space :=
{|
token := token A × token B;
coh '(a1, b1) '(a2, b2) := coh a1 a2 ∧ coh b1 b2;
|}.
Infix "×" := cstens : coh_scope.
Program Definition cstens_lmap {A B C D} (f : A --o B) (g : C --o D) : A×C --o B×D :=
{|
has '((a, c), (b, d)) := has f (a, b) ∧ has g (c, d);
|}.
Infix "×" := cstens_lmap : clique_scope.
Lemma cstens_id {A B} :
(@lmap_id A) × (@lmap_id B) = lmap_id.
Lemma cstens_compose {A1 B1 C1} {A2 B2 C2} :
∀ (f1 : A1 --o B1) (g1 : B1 --o C1) (f2 : A2 --o B2) (g2 : B2 --o C2),
(g1 @ f1) × (g2 @ f2) = (g1 × g2) @ (f1 × f2).
Program Definition csunit : space :=
{|
token := unit;
coh x y := True;
|}.
Notation "1" := csunit : coh_scope.
(*
(** Left unitor *)
Program Definition lam A : 1 * A --o A :=
{|
Next Obligation.
destruct H; auto.
Qed.
(** Right unitor *)
Program Definition rho A : A * 1 --o A :=
{|
lmap_apply a := (a, tt);
|}.
Next Obligation.
destruct H; auto.
Qed.
*)
(* etc.. *)
Negation
Variant lneg_token A :=
| ln (a : token A).
Arguments ln {A}.
Variant lneg_coh (A : space) : relation (lneg_token A) :=
lneg_coh_intro x y :
(coh x y → x = y) → lneg_coh A (ln x) (ln y).
Program Definition lneg (A : space) : space :=
{|
token := lneg_token A;
coh := lneg_coh A;
|}.
Program Definition lmap_flip {A B} (f : A --o B) : lneg B --o lneg A :=
{|
has '((ln x), (ln y)) := has f (y, x);
|}.
Program Definition seq (A B : space) : space :=
{|
token := token A × token B;
coh '(a1, b1) '(a2, b2) := coh a1 a2 ∧ (a1 = a2 → coh b1 b2);
|}.
Infix ";;" := seq (at level 40, left associativity) : coh_scope.
Program Definition seq_lmap {A B C D} (f g : _ --o _) : (A ;; C) --o (B ;; D) :=
{|
has '((a, c), (b, d)) := has f (a, b) ∧ has g (c, d);
|}.
Infix ";;" := seq_lmap : lmap_scope.
Inductive list_coh (A : space) : relation (list (token A)) :=
| nil_coh_l s :
list_coh A nil s
| nil_coh_r s :
list_coh A s nil
| cons_coh a b x y :
coh a b →
(a = b → list_coh A x y) →
list_coh A (a :: x) (b :: y).
Program Definition dag (A : space) : space :=
{|
token := list (token A);
coh := list_coh A;
|}.
Notation "! A" := (dag A)
(at level 8, right associativity, format "'!' A") : coh_scope.
Lemma prefix_coh {A} s1 s2 t1 t2 :
list_coh A (s1 ++ t1) (s2 ++ t2) →
list_coh A s1 s2.
Lemma suffix_coh {A} s t1 t2 :
list_coh A (s ++ t1) (s ++ t2) →
list_coh A t1 t2.
Lemma app_coh {A} s t1 t2 :
list_coh A t1 t2 →
list_coh A (s ++ t1) (s ++ t2).
Action on linear maps
Inductive dag_lmaps {A B} (f : A --o B) : token !A → token !B → Prop :=
| dag_lmaps_nil :
dag_lmaps f nil nil
| dag_lmaps_cons a b aa bb :
has f (a, b) →
dag_lmaps f aa bb →
dag_lmaps f (a :: aa) (b :: bb).
Program Definition dag_lmap {A B} (f : A --o B) : !A --o !B :=
{|
has '(aa, bb) := dag_lmaps f aa bb;
|}.
Notation "! f" := (dag_lmap f)
(at level 8, right associativity, format "'!' f") : clique_scope.
Lemma dag_id {A} :
!(@lmap_id A) = @lmap_id !A.
Lemma dag_compose {A B C} (f : A --o B) (g : B --o C) :
!(g @ f) = !g @ !f.
Counit
Inductive dag_counit_lmaps A : token !A → token A → Prop :=
dag_counit_intro a : dag_counit_lmaps A (a :: nil) a.
Program Definition dag_counit A : !A --o A :=
{|
has '(aa, a) := dag_counit_lmaps A aa a;
|}.
Lemma dag_counit_natural {A B} (f : A --o B) :
f @ dag_counit A = dag_counit B @ !f.
Comultiplication
Inductive dag_comult_lmaps {A} : token !A → token !!A → Prop :=
| dag_comult_nil :
dag_comult_lmaps nil nil
| dag_comult_cons s a aa :
dag_comult_lmaps a aa →
dag_comult_lmaps (s ++ a) (s :: aa).
Program Definition dag_comult A : !A --o !!A :=
{|
has '(a, aa) := dag_comult_lmaps a aa;
|}.
Lemma dag_lmaps_app {A B} (f : A --o B) a1 a2 b1 b2:
has !f (a1, b1) →
has !f (a2, b2) →
has !f (a1 ++ a2, b1 ++ b2).
Lemma dag_lmaps_app_inv {A B} (f : A --o B) a b1 b2:
has !f (a, b1 ++ b2) →
∃ a1 a2,
a = a1 ++ a2 ∧
has !f (a1, b1) ∧
has !f (a2, b2).
Lemma dag_comult_natural {A B} (f : A --o B) :
!!f @ dag_comult A = dag_comult B @ !f.
Properties
Lemma dag_comult_counit {A} :
!(dag_counit A) @ (dag_comult A) = @lmap_id !A.
Lemma dag_counit_comult {A} :
(dag_counit !A) @ (dag_comult A) = @lmap_id !A.
Lemma dag_comult_app {A} x y xs ys:
has (dag_comult A) (x, xs) →
has (dag_comult A) (y, ys) →
has (dag_comult A) (x ++ y, xs ++ ys).
Lemma dag_comult_app_inv {A} a xs ys:
has (dag_comult A) (a, xs ++ ys) →
∃ x y,
a = x ++ y ∧
has (dag_comult A) (x, xs) ∧
has (dag_comult A) (y, ys).
Lemma dag_comult_comult {A} :
!(dag_comult A) @ (dag_comult A) = (dag_comult !A) @ (dag_comult A).
Kleisli extension
Definition dag_ext {A B} (f : !A --o B) : !A --o !B :=
dag_lmap f @ dag_comult A.
Lemma dag_ext_counit A :
dag_ext (dag_counit A) = @lmap_id !A.
Lemma dag_counit_ext {A B} (f : !A --o B) :
dag_counit B @ dag_ext f = f.
Lemma dag_ext_compose {A B C} (f : !A --o B) (g : !B --o C) :
dag_ext (g @ dag_ext f) = dag_ext g @ dag_ext f.