Add CheckOwnInContext

theories/lithium/infrastructure.v

 (** General infrastructure *)
+From iris.base_logic.lib Require Import iprop.
 From refinedc.lithium Require Import base.
 
 (** * [protected] *)
@@ -27,6 +28,10 @@ Ltac check_hyp_not_exists P :=
 Class CheckHypNotExists (P : Prop) : Prop := check_hyp_not_exists : True.
 Hint Extern 1 (CheckHypNotExists ?P) => (check_hyp_not_exists P; change True; fast_done) : typeclass_instances.
 
+(** * Checking if a hyp in the context
+  The implementation can be found in interpreter.v *)
+Class CheckOwnInContext {Σ} (P : iProp Σ) : Prop := { check_own_in_context : True }.
+
 (** * Different ways of checking if a property holds  *)
 (** ** [FastDone]
  Should be used if it is expected that the property shows up directly as a hypothesis. *)

theories/lithium/interpreter.v

@@ -405,6 +405,24 @@ Ltac solve_protected_eq :=
 Ltac liEnforceInvariantAndUnfoldInstantiatedEvars :=
   unfold_instantiated_evars; try liEnforceInvariant.
 
+(** * Checking if the context contains ownership of a certain assertion
+
+  Note that this implementation requires that liEnforceInvariant has been called
+  previously when there was a envs_entails goal.
+ *)
+Ltac liCheckOwnInContext P :=
+  let rec go Hs :=
+      lazymatch Hs with
+      | Esnoc ?Hs2 ?id ?Q =>
+        first [ unify Q P with typeclass_instances | go Hs2 ]
+      end in
+  match goal with
+  | H := Envs ?Δi ?Δs _ |- _ =>
+      lazymatch (type of H) with | IPM_STATE _ => idtac end;
+      first [ go Δs | go Δi ]
+  end.
+Hint Extern 1 (CheckOwnInContext ?P) => (liCheckOwnInContext P; constructor; exact: I) : typeclass_instances.
+
 (** * Main lithium tactics *)
 Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
 Ltac convert_to_i2p P cont :=

theories/typing/programs.v

@@ -554,8 +554,8 @@ Section typing.
     type_alive ty β ∗ T -∗
     subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) T.
   Proof. iIntros "[Ha $] Hl". rewrite /type_alive. by iApply "Ha". Qed.
-  Global Instance subsume_alloc_alive_type_alive_inst ty β l :
-    Subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) | 50 :=
+  Global Instance subsume_alloc_alive_type_alive_inst ty β l `{!CheckOwnInContext (type_alive ty β)} :
+    Subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) | 10 :=
     λ T, i2p (subsume_alloc_alive_type_alive ty β l T).
 
   Lemma simplify_goal_type_alive ty β P `{!AllocAlive ty β P} T :