fixed some rules + a tiny example that takes way too long to prove

Needs more automation
logsem · Feb 26, 2024 · b2c9453 · b2c9453
1 parent 4a128e7
commit b2c9453
Show file tree

Hide file tree

Showing 2 changed files with 40 additions and 6 deletions.
diff --git a/theories/input_lang_delim/interp.v b/theories/input_lang_delim/interp.v
@@ -277,34 +277,53 @@ Section weakestpre.
   Qed.
 
 
-  Lemma wp_pop_end (v : ITV) (k : IT -n> IT) {Hk : IT_hom k}
+  Lemma wp_pop_end (v : ITV)
     Φ s :
     has_substate [] -∗
     ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} IT_of_V v @ s {{ Φ }}) -∗
-    WP@{rs} k $ 𝒫 (IT_of_V v) @ s {{ Φ }}.
+    WP@{rs} 𝒫 (IT_of_V v) @ s {{ Φ }}.
   Proof.
     iIntros "Hs Ha".
-    rewrite get_val_ITV. simpl. rewrite hom_vis.
+    rewrite get_val_ITV. simpl.
     iApply (wp_subreify _ _ _ _ _ _ _ ((Next $ IT_of_V v)) with "Hs").
     - simpl. reflexivity.
     - reflexivity.
     - done.
   Qed.
 
-  Lemma wp_pop_cons (σ : state) (v : ITV) (k : IT -n> IT) {Hk : IT_hom k}
+  Lemma wp_pop_cons (σ : state) (v : ITV) (k : IT -n> IT)
     Φ s :
     has_substate ((laterO_map k) :: σ) -∗
     ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k $ IT_of_V v @ s {{ Φ }}) -∗
-    WP@{rs} k $ 𝒫 (IT_of_V v) @ s {{ Φ }}.
+    WP@{rs} 𝒫 (IT_of_V v) @ s {{ Φ }}.
   Proof.
     iIntros "Hs Ha".
-    rewrite get_val_ITV. simpl. rewrite hom_vis.
+    rewrite get_val_ITV. simpl.
     iApply (wp_subreify _ _ _ _ _ _ _ ((laterO_map k (Next $ IT_of_V v))) with "Hs").
     - simpl. reflexivity.
     - reflexivity.
     - done.
   Qed.
 
+  Lemma wp_app_cont (σ : state) (e : laterO IT) (k' : laterO (IT -n> IT))
+    (k : IT -n> IT) {Hk : IT_hom k}
+    Φ s :
+    has_substate σ -∗
+    ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗
+       WP@{rs} later_car (laterO_ap k' e) @ s {{ Φ }}) -∗
+    WP@{rs} k (APP_CONT e k') @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    unfold APP_CONT. simpl. rewrite hom_vis.
+    iApply (wp_subreify _ _ _ _ _ _ _ (laterO_ap k' e) with "Hs").
+    - simpl. do 2 f_equiv.
+      trans (laterO_map k :: σ); last reflexivity.
+      rewrite ccompose_id_l. f_equiv. intro. simpl. by rewrite ofe_iso_21.
+    - reflexivity.
+    - iApply "Ha".
+  Qed.
+
+
 End weakestpre.
 
 Section interp.

diff --git a/theories/input_lang_delim/lang.v b/theories/input_lang_delim/lang.v
@@ -655,9 +655,24 @@ Global Instance AppNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNo
   __app e K := cont_compose K (AppRK (__asSynExpr e) END)
   }.
 
+Class AppContNotation (A B C : Type) := { __app_cont : A -> B -> C }.
+
+Global Instance AppContNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : AppContNotation (F S) (G S) (expr S) := {
+  __app_cont e₁ e₂ := AppCont (__asSynExpr e₁) (__asSynExpr e₂)
+  }.
+
+Global Instance AppContNotationLK {S : Set} : AppContNotation (cont S) (val S) (cont S) := {
+  __app_cont K v := cont_compose K (AppContLK v END)
+  }.
+
+Global Instance AppContNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppContNotation (F S) (cont S) (cont S) := {
+  __app_cont e K := cont_compose K (AppContRK (__asSynExpr e) END)
+  }.
+
 Notation of_val := Val (only parsing).
 
 Notation "x '⋆' y" := (__app x%syn y%syn) (at level 40, y at next level, left associativity) : syn_scope.
+Notation "x '@k' y" := (__app_cont x%syn y%syn) (at level 40, y at next level, left associativity) : syn_scope.
 Notation "x '+' y" := (__op x%syn Add y%syn) : syn_scope.
 Notation "x '-' y" := (__op x%syn Sub y%syn) : syn_scope.
 Notation "x '*' y" := (__op x%syn Mult y%syn) : syn_scope.