Adapt for the stdpp/iris bump.

rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v

@@ -39,7 +39,8 @@ Definition CR
   structR "C" q **
   _field "C::mut" |-> recursive_mutex.derivedR γ q **
   as_Rep (fun this : ptr =>
-    recursive_mutex.inv_rmutex γ (∃ a_b : tele_arg _, tele_app (P this) a_b)).
+    recursive_mutex.inv_rmutex γ (∃ a_b : tele_arg TT,
+      @tele_app TT (fun _ => mpred) (P this) a_b)).
 
 #[only(cfractional,ascfractional,type_ptr)] derive CR.
 #[only(lazy_unfold)] derive CR.
@@ -90,28 +91,29 @@ Section with_cpp.
   Proof. solve_learnable. Qed.
 
   Lemma tele_app_mk_beta (P : Z -> Z -> mpred) (x y : Z) :
-    tele_app (TT := TT) (λ a b : Z, P a b) (mk x y) = P x y.
+    @tele_app TT (fun _ => mpred) (λ a b : Z, P a b) (mk x y) = P x y.
   Proof. reflexivity. Qed.
 
   (** "Eta-expand" [∃ xy : TT, ... tele_app P xy ... ] to [∃ (x y : Z), ... tele_app P (mk x y) ...].
   This is useful because [tele_app (λ a b : Z, Q a b) (mk x y)] simplifies to [Q x y] ([tele_app_mk_beta]). *)
   #[program] Definition learn_args_C (P : TT -t> mpred) :=
     \cancelx
     \bound_existential args
-    \proving tele_app P args
+    \proving @tele_app TT (fun _ => mpred) P args
     \exist a b
     \instantiate args := mk a b
-    \through tele_app P (mk a b)
+    \through @tele_app TT (fun _ => mpred) P (mk a b)
     \end.
   Next Obligation. work. Qed.
   #[local] Hint Resolve learn_args_C : br_hints.
 
   #[program] Definition P_unfold_split_args_F this args :=
     \cancelx
-    \consuming tele_app (P this) args
+    \consuming @tele_app TT (fun _ => mpred) (P this) args
     \intro a
     \intro b
-    \deduce tele_app (TT := TT) (fun a b => this |-> CR' a b) (mk a b)
+    \deduce @tele_app TT (fun _ => mpred)
+      (fun a b => this |-> CR' a b) (mk a b)
     \deduce [| args = mk a b |]
     \end.
   Next Obligation. iIntros (this [a [b []]]) "/= ?". iExists a, b. rewrite P.unlock. work. Qed.

rocq-brick-libstdcpp/proof/mutex/spec/recursive_mutex.v

@@ -349,7 +349,8 @@ cinv (
     current_thread th **
     match t with
     | NotHeld => locked g.(lock_gname) th 0
-    | Held n args => own g.(level_gname) (◯E (S n, th)) ** tele_app P args
+    | Held n args => own g.(level_gname) (◯E (S n, th)) **
+        @tele_app TT (fun _ => mpred) P args
     end.
 
   Section with_cpp.
@@ -413,7 +414,7 @@ cinv (
         (_ : acquire (TT := TT) t t') :=
       \cancelx
       \consuming acquireable g th t' P
-      \deduce{args} tele_app P args
+      \deduce{args} @tele_app TT (fun _ => mpred) P args
       \deduce{n} [| t' = Held n args /\ t = release t' |]
       \deduce own g.(level_gname) (◯E (S n, th))
       \end.
@@ -432,8 +433,8 @@ cinv (
       \proving acquireable γ th' args' P'
       \instantiate th' := th
       \instantiate args' := Held n args
-      \deduce tele_app P args
-      \through tele_app P' args
+      \deduce @tele_app TT (fun _ => mpred) P args
+      \through @tele_app TT (fun _ => mpred) P' args
       \end.
     Next Obligation. rewrite acquireable.unlock; work. Qed.
 
@@ -444,7 +445,7 @@ cinv (
       \consuming own g.(level_gname) (◯E (S n, th))
       \bound n' args
       \proving acquireable (TT := TT) g th (Held n' args) P
-      \through tele_app P args
+      \through @tele_app TT (fun _ => mpred) P args
       \through [| n' = n |]
       \end.
     Next Obligation. rewrite acquireable.unlock; work. Qed.
@@ -462,21 +463,26 @@ cinv (
     Proof. solve_learnable. Qed.
 
     #[global] Instance learn_inv_rmutex_TT : `{Learnable
-      (inv_rmutex γ (∃ xs : tele_arg TT1, tele_app P1 xs))
-      (inv_rmutex γ (∃ xs : tele_arg TT2, tele_app P2 xs))
+      (inv_rmutex γ (∃ xs : tele_arg TT1,
+        @tele_app TT1 (fun _ => mpred) P1 xs))
+      (inv_rmutex γ (∃ xs : tele_arg TT2,
+        @tele_app TT2 (fun _ => mpred) P2 xs))
       [TT2 = TT1] }.
     Proof. solve_learnable. Qed.
 
     #[global] Instance learn_inv_rmutex_P TT : `{Learnable
-      (inv_rmutex γ1 (∃ xs : tele_arg TT, tele_app P1 xs))
-      (inv_rmutex γ2 (∃ xs : tele_arg TT, tele_app P2 xs))
+      (inv_rmutex γ1 (∃ xs : tele_arg TT,
+        @tele_app TT (fun _ => mpred) P1 xs))
+      (inv_rmutex γ2 (∃ xs : tele_arg TT,
+        @tele_app TT (fun _ => mpred) P2 xs))
       [P2 = P1] }.
     Proof. solve_learnable. Qed.
 
     #[global] Instance learn_args
       {TT: tele} (t : acquire_state TT) (P : TT -t> mpred) :
       `{Learnable
-      (tele_app P args ** own (level_gname γ) (◯E (S n, th)))
+      (@tele_app TT (fun _ => mpred) P args **
+        own (level_gname γ) (◯E (S n, th)))
       (acquireable γ th t P)
       [t = Held n args] }.
     Proof. solve_learnable. Qed.
@@ -485,7 +491,7 @@ cinv (
       (x : acquire_state TT) : acquire_state TT :=
       match x with
       | NotHeld => NotHeld
-      | Held n xs => Held n (tele_app f xs)
+      | Held n xs => Held n (@tele_app TT (fun _ => TT) f xs)
       end.
 
     Lemma update_eq {TT : tele} f t1 t2 : acquire t1 t2 ->
@@ -498,38 +504,41 @@ cinv (
     cpp.spec "std::recursive_mutex::recursive_mutex()" as ctor_spec' with
       (\this this
       \persist{th} current_thread th
-      \pre{TT P xs} |> tele_app (TT := TT) P xs
-      \require ∀ xs, WeaklyObjective (tele_app P xs)
+      \pre{TT P xs} |> @tele_app TT (fun _ => mpred) P xs
+      \require ∀ xs, WeaklyObjective (@tele_app TT (fun _ => mpred) P xs)
       \post
         Exists g,
           this |-> derivedR g 1$m **
           used_threads g.(lock_gname) empty **
-          inv_rmutex g (∃ xs, tele_app P xs)).
+          inv_rmutex g (∃ xs, @tele_app TT (fun _ => mpred) P xs)).
 
     cpp.spec "std::recursive_mutex::~recursive_mutex()" as dtor_spec' with
       (\this this
       \pre{g} this |-> derivedR g 1
       \pre used_threads g.(lock_gname) empty
-      \pre{TT P} inv_rmutex g (∃ xs, tele_app (TT := TT) P xs)
-      \post |> (Exists xs, tele_app (TT := TT) P xs)).
+      \pre{TT P} inv_rmutex g (∃ xs,
+        @tele_app TT (fun _ => mpred) P xs)
+      \post |> (Exists xs, @tele_app TT (fun _ => mpred) P xs)).
 
     cpp.spec "std::recursive_mutex::lock()" as lock_spec' with
       (\this this
-      \persist{g TT P} inv_rmutex g (∃ xs, tele_app (TT := TT) P xs)
+      \persist{g TT P} inv_rmutex g (∃ xs,
+        @tele_app TT (fun _ => mpred) P xs)
       \prepost{q} this |-> derivedR g q
       \pre{th n} acquireable g th n P
       \post (Exists n', [| acquire n n' |] ** ▷ acquireable g th n' P)).
     (* to prove: this is derivable from lock_spec *)
 
     cpp.spec "std::recursive_mutex::unlock()" as unlock_spec' with
       (\this this
-      \persist{g TT P} inv_rmutex g (∃ xs, tele_app (TT := TT) P xs)
+      \persist{g TT P} inv_rmutex g (∃ xs,
+        @tele_app TT (fun _ => mpred) P xs)
       \prepost{q} this |-> derivedR g q
       \pre{th n args} acquireable g th (Held n args) P
       \post acquireable g th (release $ Held n args) P).
 
     Definition do_lock g K : mpred := ∃ TT P th n,
-      inv_rmutex g (∃ xs, tele_app (TT := TT) P xs)
+      inv_rmutex g (∃ xs, @tele_app TT (fun _ => mpred) P xs)
       ** acquireable g th n P
       ** (
         (* TODO readd *)
@@ -539,7 +548,7 @@ cinv (
     #[global] Arguments do_lock /.
 
     Definition do_unlock g K : mpred := ∃ TT P th n args,
-      inv_rmutex g (∃ xs, tele_app (TT := TT) P xs)
+      inv_rmutex g (∃ xs, @tele_app TT (fun _ => mpred) P xs)
       ** acquireable g th (Held n args) P
       ** (
         (* TODO readd *)

rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v

@@ -17,7 +17,8 @@ Section to_upstream.
   Proof. unshelve solve_inhabited. solve_inhabited. Qed.
 
   #[global] Instance timeless_tele_app {PROP : bi} {TT : tele} (args : TT) (P : TT -t> PROP):
-    `{(∀.. args, Timeless (tele_app P args)) -> Timeless (tele_app P args)}.
+    `{(∀.. args, Timeless (@tele_app TT (fun _ => PROP) P args)) ->
+      Timeless (@tele_app TT (fun _ => PROP) P args)}.
   Proof.
     elim: TT args P => [[] //|T TT IH] args P HT.
     destruct_tele; simpl.
@@ -88,7 +89,8 @@ Definition CR
   structR "C" q **
   _field "C::m" |-> recursive_mutex.derivedR γ q **
   as_Rep (fun this : ptr =>
-    recursive_mutex.inv_rmutex γ (∃ a : tele_arg TT, tele_app (P this) a)).
+    recursive_mutex.inv_rmutex γ (∃ a : tele_arg TT,
+      @tele_app TT (fun _ => mpred) (P this) a)).
 
 #[only(cfractional,ascfractional,cfracvalid,type_ptr)] derive CR.
 #[only(lazy_unfold(export))] derive CR.
@@ -99,14 +101,17 @@ Section with_cpp.
   Context `{!recursive_mutex.lockedG Σ}.
   Context `{!HasOwn (iPropI _) recursive_mutex.cmraR}.
 
-  #[local] Instance: `{WeaklyObjective1 (tele_app (P p))}.
+  #[local] Instance:
+    `{WeaklyObjective1 (@tele_app TT (fun _ => mpred) (P p))}.
   Proof. Admitted.
 
   #[global] Instance P_timeless p a : Timeless (P p a).
   Proof. rewrite P.unlock; apply _. Qed.
 
-  Succeed #[global] Instance CR'_timeless' p args : Timeless (tele_app (TT := TT) (λ a : Z, p |-> CR' a) args) := _.
-  Succeed #[global] Instance P_timeless' p args : Timeless (tele_app (P p) args) := _.
+  Succeed #[global] Instance CR'_timeless' p args :
+    Timeless (@tele_app TT (fun _ => mpred) (λ a : Z, p |-> CR' a) args) := _.
+  Succeed #[global] Instance P_timeless' p args :
+    Timeless (@tele_app TT (fun _ => mpred) (P p) args) := _.
 
   cpp.spec "test_one_answer()" from source with (
     \post[Vint 42] emp
@@ -150,7 +155,8 @@ Section with_cpp.
     \pre{γ} this |-> CR γ 1$m
     (* \pre recursive_mutex.used_threads (lock_gname γ) empty *)
     \pre recursive_mutex.used_threads γ.(lock_gname) {[thr]}
-    \pre recursive_mutex.inv_rmutex γ (∃ xs, tele_app (TT := TT) (P this) xs)
+    \pre recursive_mutex.inv_rmutex γ (∃ xs,
+      @tele_app TT (fun _ => mpred) (P this) xs)
     \pre recursive_mutex.acquireable (TT := TT) γ thr recursive_mutex.NotHeld (P this)
     \post emp).