OOPSLA'19 Paper 161 Coq 8.9.0 formalization of Figure 2, functions of Figure 3, and iteration

lang.v

Require Import Utf8.
Require Import Program.
Require Import Arith.
Require Import Ensembles.
Require Import Setoid.
Require Import Relations.
Require Import Morphisms.
Require Import Coq.Classes.Equivalence.

Polymorphic Definition binop (E:Type) := E -> E -> E.

Polymorphic Definition nilpotent {E:Type} (op:binop E) (X:E) : Prop :=
  forall y,  op y X = X /\ op X y = X.
Polymorphic Definition associative {E:Type} (op:binop E) : Prop :=
  forall x y z, op x (op y z) = op (op x y) z.

Polymorphic Record monoid (E:Type) (op:binop E) (I:E) :=
  { left_unit : forall x,  op I x = x;
    right_unit : forall x, op x I = x;
    massoc: associative op
  }.
Polymorphic Record join_with_top (E:Type) (op:binop E) (top:E) :=
  { comm : forall x y, op x y = op y x;
    jassoc : associative op;
    nilp : nilpotent op top;
    idemp : forall x y, op x (op x y) = op x y;
    selfid : forall x, op x x = x
  }.

Polymorphic Class EffectQuantale (E:Type) :=
  { join : binop E;
    seq : binop E;
    top : E;
    I : E;
    seqmonoid : monoid E seq I;
    isjoin : join_with_top E join top;
    ldist : forall x y z, seq x (join y z) = join (seq x y) (seq x z);
    rdist : forall x y z, seq (join x y) z = join (seq x z) (seq y z)
  }.
Infix "⊔" := join (at level 55).
Infix "▷" := seq (at level 55, right associativity).

Polymorphic Definition quantale_lt `{E:Type,EffectQuantale E} (a b:E) : Prop := a ⊔ b = b.
Infix "⊑" := quantale_lt (at level 60).
Polymorphic Instance qlt_trans `{E:Type,EQ:EffectQuantale E} : Transitive quantale_lt.
Proof.
  unfold Transitive; unfold quantale_lt. intros.
  rewrite <- H0 at 1. rewrite jassoc. rewrite H. assumption.
  apply isjoin.
Qed.
Polymorphic Instance seq_proper `{E:Type,EffectQuantale E}: Proper (quantale_lt ==> quantale_lt ==> quantale_lt) seq.
Proof.
  unfold respectful. unfold Proper.
  intros q r pf1 s t pf2.
  transitivity (q ▷ t).
  { rewrite <- pf2. rewrite ldist. unfold quantale_lt. rewrite jassoc; try apply isjoin. erewrite selfid; try apply isjoin. reflexivity. }
  { rewrite <- pf1. rewrite rdist. unfold quantale_lt. rewrite jassoc; try apply isjoin.
    erewrite selfid; try apply isjoin. reflexivity. }
Qed.

Lemma ListInIncl : ∀ A (x:A) L L', List.In x L -> List.incl L L' -> List.In x L'.
Proof. firstorder. Qed.

Lemma ListInclMap : ∀ A B (L L':list A) (f:A->B), List.incl L L' -> List.incl (List.map f L) (List.map f L').
Proof.
  intros A B L L' f. generalize dependent L'. induction L. firstorder.
  intros. simpl. 
  intros a0 Hin.
  induction Hin. subst. apply List.in_map. apply H. simpl. left. reflexivity.
  unfold List.incl at 2 in IHL. apply IHL; eauto.
  intros x Hx. apply H. right. assumption.
Qed.
Hint Resolve ListInclMap.


Axiom PrimType : Type.
Axiom E : Type.
Axiom EQ : EffectQuantale E.
Existing Instance EQ.



Class Iterable {E:Type}(EQ:EffectQuantale E) :=
  { iter : E -> E;
    iterMono : ∀ x, x ⊑ iter x;
    iterComboL : ∀ x, x ▷ (iter x) ⊑ iter x;
    iterComboR : ∀ x, (iter x) ▷ x ⊑ iter x;
    iterIdem : ∀ x, iter (iter x) = iter x;
    iterDist : ∀ x y, (iter x) ⊔ (iter y) ⊑ iter (x ⊔ y);
    iterId : ∀ x, I ⊑ iter x
  }.
Lemma joinMonoL : ∀ E (Q:EffectQuantale E)(it:Iterable Q) (x y z:E), x ⊑ z -> x ⊔ y ⊑ z ⊔ y.
Proof.
  intros. unfold quantale_lt in H.
  unfold quantale_lt.
  erewrite jassoc.
  erewrite <- jassoc with (x:=x)(y:=y).
  erewrite comm with (x:=y)(y:=z).
  erewrite jassoc with (x:=x)(y:=z).
  rewrite H.
  erewrite comm. erewrite comm with (x:=z).
  erewrite idemp.
  reflexivity.
  eauto using @isjoin.
  eauto using @isjoin.
  eauto using @isjoin.
  eauto using @isjoin.
  eauto using @isjoin.
  eauto using @isjoin.
  eauto using @isjoin.
Qed.

Lemma joinMonoR : ∀ E (Q:EffectQuantale E) (x y z:E), y ⊑ z -> x ⊔ y ⊑ x ⊔ z.
Proof.
  intros.
  unfold quantale_lt in *.
  erewrite <- @jassoc; eauto using @isjoin. 
  rewrite ((@jassoc E0 join _ (@isjoin _ Q)) y x z).
  rewrite ((@comm E0 join _ (@isjoin _ Q)) y x).
  rewrite <- ((@jassoc _ _ _ (@isjoin _ Q)) x y z).
  rewrite H.
  erewrite ((@jassoc _ _ _ (@isjoin _ Q)) x x z).
  rewrite ((@selfid _ _ _ (@isjoin _ Q))). reflexivity.
Qed.

Instance quantale_lt_refl {E:Type}{Q:EffectQuantale E} : Reflexive (@quantale_lt E Q) := {}.
  intros. unfold quantale_lt. erewrite @selfid.
  reflexivity. eapply @isjoin.
Defined.
 
Lemma iterSubDist : ∀ E (Q:EffectQuantale E)(it:Iterable Q) (x y: E),
    (∀ (a b:E), a ⊑ b -> iter a ⊑ iter b) ->
    (iter x) ⊔ (iter y) ⊑ iter (x ⊔ y).
Proof.
  intros.
  assert (x ⊑ x ⊔ y). unfold quantale_lt. erewrite @idemp; eauto using @isjoin.
  assert (y ⊑ x ⊔ y). unfold quantale_lt.
  erewrite @jassoc; eauto using @isjoin.
  erewrite @comm with (x:=y); eauto using @isjoin.
  erewrite <- @jassoc; eauto using @isjoin.
  erewrite @comm; eauto using @isjoin.
  erewrite <- @jassoc; eauto using @isjoin.
  erewrite @idemp; eauto using @isjoin.
  erewrite @comm; eauto using @isjoin.
  transitivity (iter (x ⊔ y) ⊔ (iter (x ⊔ y))).
  assert (iter x ⊑ iter (x ⊔ y)).
  apply H; auto.
  assert (iter y ⊑ iter (x ⊔ y)).
  apply H; auto.
  erewrite joinMonoL; eauto.
  erewrite joinMonoR; eauto.
  apply (@quantale_lt_refl).
  erewrite selfid; eauto using @isjoin.
  apply (@quantale_lt_refl).
Qed.

Axiom IEQ : Iterable EQ.
Existing Instance IEQ.

Section TreeSets.
Set Implicit Arguments.
Variable A : Type.

CoInductive TreeSet : Type :=
  | Empty : TreeSet
  | Union : TreeSet -> TreeSet -> TreeSet
  | Stuff : A -> TreeSet.

(* This won't deal with e.g., a tree with only Empty leaves, but it should make a fair number of small things easier. *)
Definition union (a b : TreeSet) : TreeSet :=
  match a, b with
  | Empty, _ => b
  | _, Empty => a
  | _, _ => Union a b
  end.
Section TreeSet_Properties.

Variable P : A -> Prop.


Inductive Exists : TreeSet -> Prop :=
  | Here : forall x, P x -> Exists (Stuff x)
  | ExistsLeft : forall l r, Exists l -> Exists (Union l r)
  | ExistsRight : forall l r, Exists r -> Exists (Union l r)
.

CoInductive ForAll : TreeSet -> Prop :=
   | ForAllUnion : forall l r, ForAll l -> ForAll r -> ForAll (Union l r)
   | ForAllStuff : forall x, P x -> ForAll (Stuff x)
   | ForAllEmpty : ForAll Empty.

Lemma ExistsUnionL : forall l r, Exists l -> Exists (Union l r).
Proof.
  intros. apply ExistsLeft. assumption.
Qed.
Lemma ExistsUnionR : forall l r, Exists r -> Exists (Union l r).
Proof.
  intros. apply ExistsRight. assumption.
Qed.


End TreeSet_Properties.


End TreeSets.


Section Map.
Polymorphic Variables A B : Type.
Polymorphic Variable f : A -> B.
Polymorphic CoFixpoint tmap (t:TreeSet A) : TreeSet B :=
  match t with
  | Empty _ => Empty _
  | Union a b => Union (tmap a) (tmap b)
  | Stuff x => Stuff (f x)
  end.
Polymorphic Variable fp : A -> bool.

Polymorphic CoFixpoint tfilter (t:TreeSet A) : TreeSet A :=
  match t with
  | Empty _ => Empty _
  | Union a b => Union (tfilter a) (tfilter b)
  | Stuff x => if (fp x) then Stuff x else Empty _
  end.
End Map.


Unset Implicit Arguments.
Definition var := nat.

Definition tag := nat.


Inductive kind : Set := Ty | Eff.

(* Defining types and effects coinductively gives recursive types and effects "for free" and also makes it easiser
   to integrate infinite (tree-based) sets into prophecies. *)
CoInductive type : Type :=
| prim : PrimType -> type
| unit : type
| N : type
| B : type
| pi : type -> TreeSet proph -> list ceff -> E -> type -> type
| cont : tag -> type -> TreeSet proph -> list ceff -> E -> type -> type
with ceff : Type :=
  abort : tag -> type -> E -> ceff
| replace : tag -> E -> type -> ceff
with proph : Type :=
| prophecy : tag -> TreeSet proph -> list ceff -> E -> TreeSet proph -> list ceff -> E -> type -> proph
| fprophecy : tag -> TreeSet proph -> list ceff -> E -> TreeSet proph -> list ceff -> E -> type -> tag -> proph
.

Definition ceffPrefix (q:E) (c:ceff) : ceff :=
  match c with
  | abort t ty q' => abort t ty (q ▷ q')
  | replace t q' g => replace t (q ▷ q') g
  end.
Definition ceffPrefixes (q:E) (c:list ceff) : list ceff :=
  List.map (ceffPrefix q) c.

CoFixpoint prophSeq (p' : TreeSet proph) (c:list ceff) (q:E) (p:proph) : proph :=
  match p with
  | prophecy t Pp Cp Qp P' C' Q' σ => 
        prophecy t Pp Cp Qp  (Union (tmap (prophSeq p' c q) P') p') (C' ++ (ceffPrefixes Q' c)) (Q' ▷ q) σ
  | fprophecy t Pp Cp Qp P' C' Q' σ t' => fprophecy t Pp Cp Qp P' C' Q' σ t'
  end.

Definition prophSeqs (p:TreeSet proph) (ps : TreeSet proph) (c:list ceff) (q:E) : TreeSet proph :=
  tmap (prophSeq ps c q) p.

Definition ceffjoin (C1 C2:list ceff) : list ceff := (C1++C2)%list.
Definition prophset_union (P Q : TreeSet proph) := union P Q.

(* Continuation Effects *)
Definition CEff : Type := (TreeSet proph * list ceff * E).
(* Unit *)
Definition CI : CEff := (Empty _, nil, I).

Definition ceffSeq (A B : CEff) : CEff :=
  match A, B with
    (P1, C1, Q1), (P2, C2, Q2) => ( prophset_union (prophSeqs P1 P2 C2 Q2) P2 ,
                                    C1 ++ (ceffPrefixes Q1 C2),
                                    Q1 ▷ Q2 )%list
  end.


CoFixpoint infUnion (start:nat) (f: nat -> TreeSet proph) : TreeSet proph :=
  Union (f start) (infUnion (S start) f).
Fixpoint ceffSeqIterN (n:nat) (X:CEff) : CEff :=
match n with
| O => CI
| S n' => ceffSeq X (ceffSeqIterN n' X)
end.
Definition ceffSeqIter (X:CEff) : CEff :=
match X with
| (P,C,Q) => (infUnion 0 (fun n => match (ceffSeqIterN n (P,C,Q)) with
                                   | (P',C',Q') => prophSeqs P P' C' Q'
                                   end),
              ceffPrefixes (iter Q) C,
              iter Q)
end.


Definition freezeUntil (l:tag) (p:proph) :=
  match p with
  | prophecy t Pp Cp Qp P' C' Q' σ => fprophecy t Pp Cp Qp P' C' Q' σ l
  | fprophecy t Pp Cp Qp P' C' Q' σ t' => fprophecy t Pp Cp Qp P' C' Q' σ t'
  end.
Definition pfreeze (P:TreeSet proph) (l:tag) : TreeSet proph := tmap (freezeUntil l) P.

Definition cmask (C:list ceff) (l:tag) : list ceff :=
  List.filter (λ c, match c with
                    | abort t τ q => negb (beq_nat t l)
                    | replace t q σ => negb (beq_nat t l)
                    end) C.

Definition cproj (C:list ceff) (l:tag) : list E :=
  List.map (λ c, match c with | abort t _ q => q | replace t q _ => q end)
           (List.filter (λ c, match c with | abort t _ _ => beq_nat t l | replace t _ _ => beq_nat t l end) C).
Definition cprojh (C:list ceff) (l:tag) (Qh:E) : list E :=
  List.map (λ c, match c with | abort t _ q => q ▷ Qh | replace t q _ => q end)
           (List.filter (λ c, match c with | abort t _ _ => beq_nat t l | replace t _ _ => beq_nat t l end) C).
CoFixpoint pmask'' l Qh p : proph :=
  match p with
  | prophecy t Pp Cp Qp P' C' Q' σ =>
      prophecy t Pp Cp Qp (tmap (pmask'' l Qh) P') (cmask C' l) (List.fold_right join Q' (cprojh C' l Qh)) σ
  | fprophecy t Pp Cp Qp P' C' Q' σ t' => if (beq_nat t' l)
                                then prophecy t Pp Cp Qp (tmap (pmask'' l Qh) P') (cmask C' l) (List.fold_left join (cprojh C' l Qh) Q') σ
                                else fprophecy t Pp Cp Qp P' C' Q' σ t'
  end.


Definition pmask (P:TreeSet proph) l Qh : TreeSet proph :=
  tmap (pmask'' l Qh) (tfilter (λ p, match p with
                                            | prophecy t _ _ _ _ _ _ _ => negb (beq_nat t l)
                                            | fprophecy t _ _ _ _ _ _ _ _ => negb (beq_nat t l)
                                            end) P).


Definition minQ t C Q Qh := (List.fold_right join Q (cprojh C t Qh)).

Definition prophSetContains (p:proph) (P:nat -> list proph) := exists i, List.In p (P i).

Reserved Notation "x ≡ y" (at level 55).
(* Not currently including effect equivalence in type equivalence! *)
CoInductive tyequiv : type -> type -> Prop :=
| teqprim : ∀ pr pr', pr = pr' -> (prim pr) ≡ (prim pr')
| tequnit : unit ≡ unit
| teqN : N ≡ N
| teqB : B ≡ B
| teqpi : ∀ τ τ' σ σ' P C Q, τ ≡ τ' -> σ ≡ σ' -> (pi τ P C Q σ) ≡ (pi τ' P C Q σ')
| teqcont : ∀ ℓ τ τ' σ σ' P C Q, τ ≡ τ' -> σ ≡ σ' -> (cont ℓ τ P C Q σ) ≡ (cont ℓ τ' P C Q σ')
where "x ≡ y" := (tyequiv x y).

Inductive subeff : CEff -> CEff -> Prop :=
| subsem : ∀ P1 C1 Q1 P2 C2 Q2, prophSub P1 P2 ->
                                ceffSub C1 C2 ->
                                Q1 ⊑ Q2 ->
                                subeff (P1,C1,Q1) (P2,C2,Q2)
with subtype : type -> type -> Prop :=
     | subtrefl : ∀ t, subtype t t
     | subteq : ∀ t t', t ≡ t' -> subtype t t'
     | subfun : ∀ τ σ τ' σ' P C Q P' C' Q',
         subtype τ' τ ->
         subtype σ σ' ->
         subeff (P,C,Q) (P',C',Q') ->
         subtype (pi τ P C Q σ) (pi τ' P' C' Q' σ')
with ceffLT : ceff -> ceff -> Prop :=
| abrtLT : ∀ ℓ τ τ' X X', subtype τ τ' -> X ⊑ X' -> ceffLT (abort ℓ τ X) (abort ℓ τ' X')
| replLT : ∀ ℓ τ τ' X X', subtype τ τ' -> X ⊑ X' -> ceffLT (replace ℓ X τ) (replace ℓ X' τ')
with ceffSub : list ceff -> list ceff -> Prop :=
| cS : forall C1 C2, (∀ x, List.In x C1 -> exists x', ceffLT x x' /\ List.In x' C2) ->
                     ceffSub C1 C2
with prophLT : proph -> proph -> Prop :=
| prophecyLT : ∀ l Pp Cp Qp P P' C C' Q Q' t, prophSub P P' -> ceffSub C C' -> Q ⊑ Q' -> prophLT (prophecy l Pp Cp Qp P C Q t) (prophecy l Pp Cp Qp P' C' Q' t)
| fprophecyLT : ∀ l Pp Cp Qp P P' C C' Q Q' t l', prophSub P P' -> ceffSub C C' -> Q ⊑ Q' -> prophLT (fprophecy l Pp Cp Qp P C Q t l') (fprophecy l Pp Cp Qp P' C' Q' t l')
with prophSub : TreeSet proph -> TreeSet proph -> Prop :=
| pS : forall P1 P2, ForAll (fun x => Exists (fun y => prophLT x y) P2) P1 -> prophSub P1 P2
with ceffEquiv : list ceff -> list ceff -> Prop :=
| cE : ∀ C1 C2, ceffSub C1 C2 -> ceffSub C2 C1 -> ceffEquiv C1 C2
with prophEquiv : TreeSet proph -> TreeSet proph -> Prop :=
| pE : ∀ P1 P2, prophSub P1 P2 -> prophSub P2 P1 -> prophEquiv P1 P2
.

Inductive term : Type :=
| v : var -> term
| val : value -> term
| app : term -> term -> term
| raise : E -> term
| callcc : tag -> term -> term
| abrt : tag -> term -> term
| prompt : tag -> term -> term -> term
| If : term -> term -> term -> term
with value : Type :=
| tt : value
| n : nat -> value
| lam : var -> term -> value
(*| Lam : var -> term -> value*)
| valcont : tag -> continuation -> value
| vtrue : value
| vfalse : value
with continuation : Type :=
| CHole
| CFunc : continuation -> term -> continuation
| CArg : value -> continuation -> continuation
| Ccallcc : tag -> continuation -> continuation
| Cabrt : tag -> continuation -> continuation
| Cprompt : tag -> continuation -> term -> continuation
| CIf : continuation -> term -> term -> continuation
.
Coercion val : value >-> term.


Definition toEnsemble {A:Set} (l:list A) : Ensemble A := flip (@List.In A) l.

Definition isval (t:term) : option value :=
  match t with
  | val v0 => Some v0
  | _ => None
  end.
Fixpoint ctxtDecomp (e:term) : continuation * term :=
  match e with
  | (app f a) => (match isval f, isval a with
                 | None, _ => let (E', e') := ctxtDecomp f in (CFunc E' a, e')
                 | Some vf, None => let (E', e') := ctxtDecomp a in (CArg vf E', e')
                 | Some _, Some _ => (CHole, e)
                 end)
  | (callcc t k) => if (isval k)
                    then (CHole, e)
                    else (let (E', e') := ctxtDecomp k in (Ccallcc t E', e'))
  | (abrt t x) => if (isval x)
                  then  (CHole, e)
                  else (let (E', e') := ctxtDecomp x in (Cabrt t E', e'))
  | (prompt t b h) => if (isval b)
                      then (CHole, e)
                      else (let (E', e') := ctxtDecomp b in (Cprompt t E' h, e'))
  | If c et ef => if (isval c) then (CHole, e)
                  else (let (E', e') := ctxtDecomp c in (CIf E' et ef, e'))
  | _ => (CHole, e)
  end.

Lemma isvalTrue : ∀ e x, isval e = Some x -> e = val x.
Proof.
  intros. destruct e; inversion H; subst. reflexivity.
Qed.

Fixpoint ctxtPlug (E:continuation) (e:term) : term :=
  match E with
  | CHole => e
  | CFunc E' e2 => (app (ctxtPlug E' e) e2)
  | CArg f E' => (app (val f) (ctxtPlug E' e))
  | Ccallcc t E' => (callcc t (ctxtPlug E' e))
  | Cabrt t E' => (abrt t (ctxtPlug E' e))
  | Cprompt t E' h => (prompt t (ctxtPlug E' e) h)
  | CIf E' et ef => If (ctxtPlug E' e) et ef
  end.
Lemma ctxtDecompPlug : ∀ e e' E, ctxtDecomp e = (E, e') -> ctxtPlug E e' = e.
Proof.
  intro e.
  induction e; simpl; try (intros; inversion H; subst; reflexivity).
  + intros. induction (isval e1) eqn:Heq.
    induction (isval e2) eqn:Heq2.
    inversion H; subst.  reflexivity.
    destruct (ctxtDecomp e2) eqn:Heq'. inversion H. subst.
    simpl. rewrite (isvalTrue _ _ Heq); auto. rewrite IHe2; reflexivity.
    destruct (ctxtDecomp e1) eqn:Heq'. inversion H; subst.
    simpl. rewrite IHe1; reflexivity.
  + intros. induction (isval e) eqn:Heq. inversion H; subst. reflexivity.
    destruct (ctxtDecomp e) eqn:Heq'. inversion H; subst.
    simpl. rewrite IHe; reflexivity.
  + intros. induction (isval e) eqn:Heq. inversion H; subst. reflexivity.
    destruct (ctxtDecomp e) eqn:Heq'. inversion H; subst.
    simpl. rewrite IHe; reflexivity.
  + intros. induction (isval e1) eqn:Heq. inversion H; subst. reflexivity.
    destruct (ctxtDecomp e1) eqn:Heq'. inversion H; subst.
    simpl. rewrite IHe1; reflexivity.
  + intros. induction (isval e1) eqn:Heq. inversion H; subst. reflexivity.
    destruct (ctxtDecomp e1) eqn:Heq'. inversion H; subst.
    simpl. rewrite IHe1; reflexivity.
Qed.

Fixpoint subst (t:term) (x:var) (e:term) : term :=
  match t with
  | tt => tt
  | vtrue => vtrue
  | vfalse => vfalse
  | n x => n x
  | v y => if (beq_nat x y) then e else v y
  | lam y e' => if (beq_nat x y) then (lam y e') else lam y (subst e' x e)
  | app e1 e2 => app (subst e1 x e) (subst e2 x e)
  | raise q => raise q
  | callcc l k => callcc l (subst k x e)
  | abrt l e' => abrt l (subst e' x e)
  | valcont l E => valcont l E (* contexts captured by continuations have no free variables *)
  | prompt l e' h => prompt l (subst e' x e) (subst h x e)
  | If c et ef => If (subst c x e) (subst et x e) (subst ef x e)
  end
.


Inductive noPrompts : tag -> continuation -> Prop :=
| nopHole : ∀ t, noPrompts t CHole
| nopFunc : ∀ t E' e, noPrompts t E' -> noPrompts t (CFunc E' e)
| nopArg : ∀ t E' e, noPrompts t E' -> noPrompts t (CArg e E')
| nopCallcc : ∀ t t' E', noPrompts t E' -> noPrompts t (Ccallcc t' E')
| nopAbrt : ∀ t t' E', noPrompts t E' -> noPrompts t (Cabrt t' E')
| nopPrompt : ∀ t t' E' h, noPrompts t E' -> t <> t' -> noPrompts t (Cprompt t' E' h)
| nopIf : ∀ t E' et ef, noPrompts t E' -> noPrompts t (CIf E' et ef)
.