PCM.v 4.28 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
(** Partial commutative monoids. *)

Require Export Predom.
Require Import MetricCore.
Require Import PreoMet.

Class Associative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
  assoc : forall t1 t2 t3, op t1 (op t2 t3) == op (op t1 t2) t3.
Class Commutative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
  comm  : forall t1 t2, op t1 t2 == op t2 t1.

Section Definitions.
  Context (T : Type).
  Local Instance eqT : Setoid T | 20000 := discreteType.

  Class PCM_unit := pcm_unit : T.
  Class PCM_op   := pcm_op : option T -> option T -> option T.
  Class PCM {TU : PCM_unit} {TOP : PCM_op} :=
    mkPCM {
        pcm_op_assoc :> Associative (eqT := discreteType) pcm_op;
        pcm_op_comm  :> Commutative (eqT := discreteType) pcm_op;
        pcm_op_unit  :  forall t, pcm_op (Some pcm_unit) t = t;
        pcm_op_zero  :  forall t, pcm_op None t = None
      }.

End Definitions.

Notation "1" := (Some (pcm_unit _)) : pcm_scope.
Notation "0" := None : pcm_scope.
Notation "p · q" := (pcm_op _ p q) (at level 40, left associativity) : pcm_scope.

Delimit Scope pcm_scope with pcm.

(* PCMs with cartesian products of carriers. *)
Section Products.
  Context S T `{pcmS : PCM S, pcmT : PCM T}.
  Local Open Scope pcm_scope.
  Local Existing Instance eqT.

  Global Instance pcm_unit_prod : PCM_unit (S * T) := (pcm_unit S, pcm_unit T).
  Global Instance pcm_op_prod : PCM_op (S * T) :=
    fun ost1 ost2 =>
      match ost1, ost2 with
        | Some (s1, t1), Some (s2, t2) =>
          match Some s1 · Some s2, Some t1 · Some t2 with
            | Some sr, Some tr => Some (sr, tr)
            | _, _ => None
          end
        | _, _ => None
      end.
  Global Instance pcm_prod : PCM (S * T).
  Proof.
    split.
    - intros [[s1 t1] |]; [| reflexivity].
      intros [[s2 t2] |]; [| reflexivity].
      intros [[s3 t3] |];
        [unfold pcm_op, pcm_op_prod |
         unfold pcm_op at 1 2, pcm_op_prod;
           destruct (Some (s1, t1) · Some (s2, t2)) as [[s t] |]; simpl; tauto].
      assert (HS := assoc (Some s1) (Some s2) (Some s3));
        assert (HT := assoc (Some t1) (Some t2) (Some t3)).
      destruct (Some s1 · Some s2) as [s12 |];
        destruct (Some s2 · Some s3) as [s23 |]; [.. | reflexivity].
      + destruct (Some t1 · Some t2) as [t12 |];
        destruct (Some t2 · Some t3) as [t23 |]; [.. | reflexivity].
        * simpl in HS, HT; rewrite HS, HT; reflexivity.
        * erewrite comm, pcm_op_zero in HT by eassumption; simpl in HT.
          rewrite <- HT; destruct (Some s12 · Some s3); reflexivity.
        * erewrite pcm_op_zero in HT by eassumption; simpl in HT.
          rewrite HT; destruct (Some s1 · Some s23); reflexivity.
      + erewrite comm, pcm_op_zero in HS by eassumption; simpl in HS.
        destruct (Some t1 · Some t2) as [t12 |]; [| reflexivity].
        rewrite <- HS; reflexivity.
      + erewrite pcm_op_zero in HS by eassumption; simpl in HS.
        destruct (Some t2 · Some t3) as [t23 |]; [| reflexivity].
        rewrite HS; reflexivity.
    - intros [[s1 t1] |] [[s2 t2] |]; try reflexivity; []; simpl; unfold pcm_op, pcm_op_prod.
      rewrite (comm (Some s1)); assert (HT := comm (Some t1) (Some t2)).
      simpl in HT; rewrite HT; reflexivity.
    - intros [[s t] |]; [| reflexivity]; unfold pcm_op, pcm_op_prod; simpl.
      erewrite !pcm_op_unit by eassumption; reflexivity.
    - intros st; reflexivity.
  Qed.

End Products.

Section Order.
  Context T `{pcmT : PCM T}.
  Local Open Scope pcm_scope.
  Local Existing Instance eqT.

92 93
  Definition pcm_ord (t1 t2 : option T) :=
    exists td, td · t1 = t2.
94

95
  Global Program Instance PCM_preo {pcmT : PCM T} : preoType (option T) | 0 := mkPOType pcm_ord.
96 97 98 99 100 101 102 103 104
  Next Obligation.
    split.
    - intros x; exists 1; eapply pcm_op_unit; assumption.
    - intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
      rewrite <- assoc; congruence.
  Qed.

  Global Instance prod_ord : Proper (pord ==> pord ==> pord) (pcm_op _).
  Proof.
105 106 107
    intros x1 x2 [xd EQx] y1 y2 [yd EQy].
    exists (xd · yd).
    rewrite <- assoc, (comm yd), <- assoc, assoc, (comm y1); congruence.
108 109 110 111 112 113 114 115 116 117 118 119 120
  Qed.

End Order.

(* Package of a monoid as a module type (for use with other modules). *)
Module Type PCM_T.

  Parameter res : Type.
  Declare Instance res_op : PCM_op res.
  Declare Instance res_unit : PCM_unit res.
  Declare Instance res_pcm : PCM res.

End PCM_T.