Library models.Coherence
Require Import ProofIrrelevance.
Require Import FunctionalExtensionality.
Require Import PropExtensionality.
Require Import Relations.
Require Import RelationClasses.
Require Import List.
Local Obligation Tactic := cbn.
Require Import FunctionalExtensionality.
Require Import PropExtensionality.
Require Import Relations.
Require Import RelationClasses.
Require Import List.
Local Obligation Tactic := cbn.
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).
Local Obligation Tactic :=
cbn; try solve [process_obligation].
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.