filled in lemmas about liftStackS

theories/Core/SubEvent.v

@@ -3,9 +3,16 @@ Require Import ExtLib.Structures.Applicative.
 Require Import ExtLib.Structures.Monad.
 Require Import Program.Tactics.
 
+From Coq Require Import
+     Program
+     Setoid
+     Morphisms
+     Relations.
+
 Require Import ITree.Basics.Basics.
 Require Import HeterogeneousRelations EnTreeDefinition.
-
+Require Import Eq.Eqit.
+From Paco Require Import paco.
 
 Class ReSum (E1 E2 : Type) : Type := resum : E1 -> E2.
 
@@ -23,11 +30,75 @@ Definition trigger {E1 E2 : Type} `{ReSumRet E1 E2}
            (e : E1) : entree E2 (encodes e) :=
   Vis (resum e) (fun x : encodes (resum e) => Ret (resum_ret e x)).
 
-(* Use resum and resum_ret to map the events in an entree to another type *)
-CoFixpoint resumEntree {E1 E2 : Type} `{ReSumRet E1 E2}
-           A (t : entree E1 A) : entree E2 A :=
-  match observe t with
+CoFixpoint resumEntree' {E1 E2 : Type} `{ReSumRet E1 E2}
+           {A} (ot : entree' E1 A) : entree E2 A :=
+  match ot with
   | RetF r => Ret r
-  | TauF t => Tau (resumEntree A t)
-  | VisF e k => Vis (resum e) (fun x => resumEntree A (k (resum_ret e x)))
+  | TauF t => Tau (resumEntree' (observe t))
+  | VisF e k => Vis (resum e) (fun x => resumEntree' (observe (k (resum_ret e x))))
   end.
+
+(* Use resum and resum_ret to map the events in an entree to another type *)
+Definition resumEntree {E1 E2 : Type} `{ReSumRet E1 E2}
+           {A} (t : entree E1 A) : entree E2 A :=
+  resumEntree' (observe t).
+
+Lemma resumEntree_Ret {E1 E2 : Type} `{ReSumRet E1 E2}
+           {R} (r : R) : 
+  resumEntree (Ret r) ≅ Ret r.
+Proof. pstep. constructor. auto. Qed.
+
+Lemma resumEntree_Tau  {E1 E2 : Type} `{ReSumRet E1 E2}
+           {R} (t : entree E1 R) : 
+  resumEntree (Tau t) ≅ Tau (resumEntree t).
+Proof.
+  pstep. red. cbn. constructor. left. apply Reflexive_eqit. auto.
+Qed.
+
+Lemma resumEntree_Vis {E1 E2 : Type} `{ReSumRet E1 E2}
+           {R} (e : E1) (k : encodes e -> entree E1 R) : 
+  resumEntree (Vis e k) ≅ Vis (resum e) (fun x => resumEntree (k (resum_ret e x))).
+Proof. 
+  pstep. red. cbn. constructor. left. apply Reflexive_eqit. auto.
+Qed.
+
+Lemma resumEntree_proper E1 E2 R1 R2 b1 b2 (RR : R1 -> R2 -> Prop) `{ReSumRet E1 E2} : 
+  forall (t1 : entree E1 R1) (t2 : entree E1 R2),
+    eqit RR b1 b2 t1 t2 -> eqit RR b1 b2 (resumEntree t1) (resumEntree t2).
+Proof.
+  ginit. gcofix CIH.
+  intros. punfold H4. red in H4.
+  unfold resumEntree. hinduction H4 before r; intros.
+  - setoid_rewrite resumEntree_Ret. gstep. constructor. auto.
+  - pclearbot. setoid_rewrite resumEntree_Tau. gstep. constructor.
+    gfinal. eauto.
+  - pclearbot. setoid_rewrite resumEntree_Vis. gstep. constructor.
+    gfinal. intros. left. eapply CIH. apply REL.
+  - setoid_rewrite resumEntree_Tau. inversion CHECK. subst.
+    rewrite tau_euttge. eauto.
+  - setoid_rewrite resumEntree_Tau. inversion CHECK. subst.
+    rewrite tau_euttge. eauto.
+Qed.
+
+#[global] Instance resumEntree_proper_inst  E1 E2 R `{ReSumRet E1 E2} :
+  Proper (@eq_itree E1 _ R R eq ==> @eq_itree E2 _ R R eq) resumEntree.
+Proof.
+  repeat intro. apply resumEntree_proper. auto.
+Qed.
+
+Lemma resumEntree_bind (E1 E2 : Type) `{ReSumRet E1 E2}
+           (R S : Type) (t : entree E1 R) (k : R -> entree E1 S) :
+  resumEntree (EnTree.bind t k) ≅
+              EnTree.bind (resumEntree t) (fun x => resumEntree (k x)).
+Proof.
+  revert t. ginit. gcofix CIH.
+  intros t. unfold EnTree.bind at 1, EnTree.subst at 1.
+  unfold resumEntree at 2. destruct (observe t).
+  - setoid_rewrite resumEntree_Ret. setoid_rewrite bind_ret_l.
+    apply Reflexive_eqit_gen. auto.
+  - setoid_rewrite resumEntree_Tau. setoid_rewrite bind_tau.
+    gstep. constructor. gfinal. eauto.
+  - setoid_rewrite resumEntree_Vis. setoid_rewrite bind_vis.
+    gstep. constructor. gfinal. eauto.
+Qed.
+

theories/Eq/Eqit.v

@@ -99,6 +99,13 @@ Proof.
   intros. pstep. constructor. auto.
 Qed.
 
+Lemma eqit_Vis {E R1 R2} `{EncodingType E} b1 b2 (RR : R1 -> R2 -> Prop) (e : E) k1 k2 :
+  (forall a, eqit RR b1 b2 (k1 a) (k2 a)) -> 
+  eqit RR b1 b2 (Vis e k1) (Vis e k2).
+Proof.
+  intros. pstep. constructor. left. apply H0.
+Qed.
+
 Lemma eqit_Vis_inv {E R1 R2} `{EncodingType E} b1 b2 (RR : R1 -> R2 -> Prop) (e : E) k1 k2 :
   eqit RR b1 b2 (Vis e k1) (Vis e k2) -> forall a, eqit RR b1 b2 (k1 a) (k2 a).
 Proof.

theories/Ref/Automation.v

@@ -24,6 +24,9 @@ From EnTree Require Import
      Ref.SpecMFacts
 .
 
+From Paco Require Import paco.
+
+
 (* From Coq 8.15 *)
 Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ;  '/  ' y )").
 Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1").
@@ -1546,42 +1549,79 @@ Lemma spec_refines_liftStackS_ret_bind_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
   (RR : Rel R1 R2) A1 a k1 t2 :
   spec_refines RPre RPost RR (k1 a) t2 ->
   spec_refines RPre RPost RR (liftStackS A1 (RetS a) >>= k1) t2.
-Admitted.
+Proof.
+  intros. setoid_rewrite resumEntree_Ret. setoid_rewrite bind_ret_l.
+  auto.
+Qed.
 
 Lemma spec_refines_liftStackS_bind_bind_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
   (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
   (RR : Rel R1 R2) A1 B1 t1 k1 k2 t2 :
   spec_refines RPre RPost RR (x <- liftStackS A1 t1 ;; liftStackS B1 (k1 x) >>= k2) t2 ->
   spec_refines RPre RPost RR (liftStackS B1 (t1 >>= k1) >>= k2) t2.
-Admitted.
+Proof.
+  intros. setoid_rewrite resumEntree_bind. setoid_rewrite bind_bind. eauto.
+Qed.
 
 Lemma spec_refines_liftStackS_assume_bind_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
   (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
   (RR : Rel R1 R2) P k1 t2 :
   spec_refines RPre RPost RR (AssumeS P >>= k1) t2 ->
   spec_refines RPre RPost RR (liftStackS _ (AssumeS P) >>= k1) t2.
-Admitted.
+Proof.
+  intros.
+  enough (@liftStackS E1 Γ1 unit (AssumeS P) ≅ AssumeS P).
+  rewrite H0. auto.
+  setoid_rewrite resumEntree_Vis.
+  setoid_rewrite bind_vis. cbn. apply eqit_Vis.
+  cbn. intros. rewrite bind_ret_l. setoid_rewrite resumEntree_Ret. 
+  apply eqit_Ret. auto.
+Qed.
 
 Lemma spec_refines_liftStackS_assert_bind_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
   (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
   (RR : Rel R1 R2) P k1 t2 :
   spec_refines RPre RPost RR (AssertS P >>= k1) t2 ->
   spec_refines RPre RPost RR (liftStackS _ (AssertS P) >>= k1) t2.
-Admitted.
+Proof.
+  intros.
+  enough (@liftStackS E1 Γ1 unit (AssertS P) ≅ AssertS P).
+  rewrite H0. auto.
+  setoid_rewrite resumEntree_Vis.
+  setoid_rewrite bind_vis. cbn. apply eqit_Vis.
+  cbn. intros. rewrite bind_ret_l. setoid_rewrite resumEntree_Ret. 
+  apply eqit_Ret. auto.
+Qed.
 
 Lemma spec_refines_liftStackS_forall_bind_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
   (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
   (RR : Rel R1 R2) A1 `{QuantType A1} k1 t2 :
   spec_refines RPre RPost RR (ForallS A1 >>= k1) t2 ->
   spec_refines RPre RPost RR (liftStackS _ (ForallS A1) >>= k1) t2.
-Admitted.
+Proof.
+  intros.
+  enough (@liftStackS E1 Γ1 A1 (ForallS A1) ≅ ForallS A1).
+  rewrite H1. auto.
+  setoid_rewrite resumEntree_Vis.
+  apply eqit_Vis.
+  cbn. intros. setoid_rewrite resumEntree_Ret. apply eqit_Ret. 
+  auto.
+Qed.
 
 Lemma spec_refines_liftStackS_exists_bind_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
   (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
   (RR : Rel R1 R2) A1 `{QuantType A1} k1 t2 :
   spec_refines RPre RPost RR (ExistsS A1 >>= k1) t2 ->
   spec_refines RPre RPost RR (liftStackS _ (ExistsS A1) >>= k1) t2.
-Admitted.
+Proof.
+  intros.
+  enough (@liftStackS E1 Γ1 A1 (ExistsS A1) ≅ ExistsS A1).
+  rewrite H1. auto.
+  setoid_rewrite resumEntree_Vis.
+  apply eqit_Vis.
+  cbn. intros. setoid_rewrite resumEntree_Ret. apply eqit_Ret. 
+  auto.
+Qed.
 
 #[global] Hint Extern 101 (spec_refines _ _ _ (liftStackS _ (RetS _) >>= _) _) =>
   simple apply spec_refines_liftStackS_ret_bind_l : refines.
@@ -1610,14 +1650,43 @@ Proof. intro; rewrite <- (bind_ret_r (liftStackS _ _)); eauto. Qed.
 #[global] Hint Extern 101 (spec_refines _ _ _ (liftStackS _ ?t1) _) =>
   simple apply (spec_refines_liftStackS_bind_ret_l _ _ _ _ _ _ _ _ _ _ t1) : refines.
 
+
+Lemma spec_refines_liftStackS_proper:
+  forall (E1 : EvType) (Γ1 : list RecFrame) (frame1 : RecFrame) (R1 : Type) (t1 t2 : SpecM E1 nil R1),
+    spec_refines eqPreRel eqPostRel eq t1 t2 ->
+    spec_refines eqPreRel eqPostRel eq (@liftStackS E1 (frame1 :: Γ1) R1 t1) (liftStackS R1 t2).
+Proof.
+  intros E1 Γ1 frame1 R1 t1 t2 H. 
+  enough (strict_refines  (@liftStackS E1 (frame1 :: Γ1) R1 t1) (liftStackS R1 t2)).
+  {
+    eapply padded_refines_monot; try apply H0; auto.
+    intros. red in PR. dependent destruction PR. subst. cbn. constructor.
+  }
+  apply padded_refines_liftStackS_proper.
+  eapply padded_refines_monot; try apply H; auto.
+  intros. dependent destruction PR. red. econstructor.
+  Unshelve. all : auto. simpl. auto.
+Qed.
+
+(* I think this is backwards *)
 Lemma spec_refines_liftStackS_trans_bind_l {E1 E2 Γ1 Γ2 frame1 frame2 R1 R2}
       {RPre : SpecPreRel E1 E2 (frame1 :: Γ1) (frame2 :: Γ2)}
       {RPost : SpecPostRel E1 E2 (frame1 :: Γ1) (frame2 :: Γ2)}
       {RR : Rel R1 R2} {t1 t2 k1 t3} :
   spec_refines eqPreRel eqPostRel eq t1 t2 ->
   spec_refines RPre RPost RR (liftStackS R1 t2 >>= k1) t3 ->
   spec_refines RPre RPost RR (liftStackS R1 t1 >>= k1) t3.
-Admitted.
+Proof.
+  intros.
+  assert (spec_refines eqPreRel eqPostRel eq (@liftStackS E1 (frame1 :: Γ1) R1 t1) (liftStackS R1 t2)).
+  apply spec_refines_liftStackS_proper. auto.
+  eapply padded_refines_weaken_r; try eapply H0.
+  eapply padded_refines_bind with (RR := eq).
+  - red in H1. eapply padded_refines_monot; try apply H1; auto.
+    intros. dependent destruction PR. red. econstructor. auto. Unshelve. 2 : auto.
+    cbn. auto.
+  - intros. subst. reflexivity.
+Qed.
 
 Create HintDb refines_proofs.
 #[global] Hint Extern 901 (spec_refines _ _ _ (liftStackS _ _ >>= _) _) =>

theories/Ref/SortEx.v

@@ -27,6 +27,8 @@ From EnTree Require Import
      Ref.RecFixSpecTotal
 .
 
+From Coq Require Export Wellfounded Arith.Wf_nat Arith.Compare_dec Arith.Lt.
+
 Import Monad.
 Import MonadNotation.
 Local Open Scope monad_scope.
@@ -80,7 +82,27 @@ Definition dec_length {A : Type} (l1 l2 : list A) :=
   length l1 < length l2.
 
 Lemma dec_length_wf A : well_founded (@dec_length A).
-Admitted.
+Proof.
+  eapply well_founded_lt_compat.
+  unfold dec_length. eauto.
+Qed.
+
+Definition dec_either_length {A} (pr1 pr2 : list A * list A) :=
+  length (fst pr1) < length (fst pr2) /\ length (snd pr1) = length (snd pr2) \/
+  length (fst pr1) = length (fst pr2) /\ length (snd pr1) < length (snd pr2).
+
+Lemma wf_dec_either_length A : well_founded (@dec_either_length A).
+Proof.
+  apply wf_union.
+  - intros [z1 z2] [y1 y2] [] [x1 x2] []; simpl in *.
+    exists (z1, x2); simpl; split; try easy.
+    + rewrite <- H0. exact H2.
+    + rewrite H1. exact H.
+  - eapply wf_incl; [| apply well_founded_ltof ].
+    intros ? ? []. exact H.
+  - eapply wf_incl; [| apply well_founded_ltof ].
+    intros ? ? []. exact H0.
+Qed.
 
 Definition rdec_merge {A} (p1 p2 : list A * list A)  :=
   let '(l1,l2) := p1 in
@@ -91,7 +113,10 @@ Definition rdec_merge {A} (p1 p2 : list A * list A)  :=
     length l2 < length l4.
 
 Lemma rdec_merge_wf A : well_founded (@rdec_merge A).
-Admitted.
+Proof.
+  eapply wf_incl; try apply wf_dec_either_length.
+  red. intros [? ?] [? ?] H. auto.
+Qed.
 
 Definition sorted : list nat -> Prop :=
   Sorted (Nat.le).
@@ -117,6 +142,11 @@ Definition halve : list nat -> entree_spec E (list nat * list nat) :=
                         '(l4,l5) <- rec l3;;
                         Ret (x::l4, y::l5)).
 
+
+(* splits a list in half using th monadic, recursion operator rec_fix_spec. 
+   The calling the rec function argument corresponds to recursive calls to the halve function *)
+
+
 Definition halve_pre (l : list nat) := True.
 Definition halve_post (l : list nat) p :=
   let '(l1,l2) := p in

theories/Ref/SpecM.v

@@ -333,7 +333,7 @@ Definition ErrorS {E} {Γ} A (str : string) : SpecM E Γ A :=
 
 (* Lift a SpecM in the empty FunStack to an arbitrary FunStack *)
 Definition liftStackS {E} {Γ} A (t:SpecM E nil A) : SpecM E Γ A :=
-  resumEntree A t.
+  resumEntree t.
 
 (* Compute the type forall a b c ... . SpecM ... (R a b c ...) from an lrt *)
 (*

theories/Ref/SpecMFacts.v

@@ -180,3 +180,63 @@ Proof.
 Qed.
 
 End interp_mrec_spec_quantr.
+
+Lemma refines_liftStackS_proper:
+  forall (E1 : EvType) (Γ1 : list RecFrame) (frame1 : RecFrame) (R1 : Type) (t1 t2 : SpecM E1 nil R1),
+    refines eq PostRelEq eq t1 t2 ->
+    refines eq PostRelEq eq (@liftStackS E1 (frame1 :: Γ1) R1 t1) (liftStackS R1 t2).
+Proof.
+  intros E1 Γ1 frame1 R1. unfold liftStackS. pcofix CIH. intros t1 t2 Ht12.
+  unfold resumEntree. punfold Ht12. red in Ht12.
+  pstep. red. hinduction Ht12 before r; intros.
+  - constructor. auto.
+  - constructor. pclearbot. right. eauto.
+  - simpl. subst. unfold resum. unfold ReSum_nil_FunStack. destruct e2; constructor;
+      auto; intros; pclearbot; right; eauto. 
+    dependent destruction H. eapply CIH. 
+    cbn in H0. cbn in b.
+    match goal with |- refines _ _ _ (k1 ?a) _ => remember a as b' end.
+    cbn in b'. specialize (H0 b' b' (PostRelEq_intro _ _)). pclearbot. auto.
+    dependent destruction H.  eapply CIH. 
+    cbn in H0. cbn in b.
+    match goal with |- refines _ _ _ (k1 ?a) _ => remember a as b' end.
+    cbn in b'. specialize (H0 b' b' (PostRelEq_intro _ _)). pclearbot. auto.
+  - constructor. eauto.
+  - constructor. eauto.
+  - cbn. constructor. intros. eauto.
+  - econstructor. eauto.
+  - econstructor. eauto.
+  - constructor. eauto.
+Qed.
+
+Lemma pad_resumEntree_comm E1 E2 `{resret : ReSumRet E1 E2} R (t : entree E1 R) :
+      resumEntree (Padded.pad t) ≅ Padded.pad (resumEntree t).
+Proof.
+  revert t. ginit. gcofix CIH.
+  intros. unfold resumEntree at 2. unfold Padded.pad at 1.
+  destruct (observe t).
+  - setoid_rewrite Padded.pad_ret. rewrite resumEntree_Ret.
+    gstep. constructor. auto.
+  - setoid_rewrite Padded.pad_tau. rewrite resumEntree_Tau.
+    gstep. constructor. gfinal. eauto.
+  - setoid_rewrite Padded.pad_vis. rewrite resumEntree_Vis.
+    gstep. constructor. intros. red. rewrite resumEntree_Tau.
+    gstep. constructor. gfinal. eauto.
+Qed.
+
+Lemma padded_refines_liftStackS_proper:
+  forall (E1 : EvType) (Γ1 : list RecFrame) (frame1 : RecFrame) (R1 : Type) (t1 t2 : SpecM E1 nil R1),
+    padded_refines eq PostRelEq eq t1 t2 ->
+    padded_refines eq PostRelEq eq (@liftStackS E1 (frame1 :: Γ1) R1 t1) (liftStackS R1 t2).
+Proof.
+  unfold padded_refines.
+  intros.
+  eapply refines_eutt_padded_l with (t1 := liftStackS R1 (Padded.pad t1)); try apply Padded.pad_is_padded.
+  setoid_rewrite pad_resumEntree_comm. reflexivity.
+  eapply refines_eutt_padded_r with (t2 := liftStackS R1 (Padded.pad t2));
+    try apply Padded.pad_is_padded.
+  setoid_rewrite pad_resumEntree_comm. apply Padded.pad_is_padded.
+  setoid_rewrite pad_resumEntree_comm. reflexivity.
+  apply refines_liftStackS_proper. auto.
+Qed.
+