allow vm_compute_hint to return option

theories/lithium/classes.v

@@ -53,9 +53,8 @@ Typeclasses Opaque destruct_hint.
 Arguments destruct_hint : simpl never.
 
 (** * [vm_compute_hint] *)
-Definition vm_compute_hint {A B C} (f : A → B) (x : A) (T : B → C) : C :=
-  T (f x).
-Typeclasses Opaque vm_compute_hint.
+Definition vm_compute_hint {Σ A B} (f : A → option B) (x : A) (T : B → iProp Σ) : iProp Σ :=
+  ∃ y, ⌜f x = Some y⌝ ∗ T y.
 Arguments vm_compute_hint : simpl never.
 
 (** * [RelatedTo] *)

theories/lithium/infrastructure.v

@@ -38,6 +38,10 @@ Class CheckOwnInContext {Σ} (P : iProp Σ) : Prop := { check_own_in_context : T
 Class FastDone (P : Prop) : Prop := fast_done_proof : P.
 Global Hint Extern 1 (FastDone ?P) => (change P; fast_done) : typeclass_instances.
 
+(** ** [TCDone] *)
+Class TCDone (P : Prop) : Prop := done_proof : P.
+Global Hint Extern 1 (TCDone ?P) => (change P; done) : typeclass_instances.
+
 (** ** [CanSolve]
  Requires the user to provide a general purpose [can_solve_tac] (see tactics.v)
  which should try hard to solve this goal. *)

theories/lithium/interpreter.v

@@ -28,11 +28,15 @@ Section coq_tactics.
     (P1 -∗ P2) → envs_entails Δ (P1 ∗ T) → envs_entails Δ (P2 ∗ T).
   Proof. by rewrite envs_entails_eq => -> HP. Qed.
 
-  Lemma tac_vm_compute_hint {A B} Δ (f : A → B) a (Q : B → iProp Σ) x:
-    (∀ y, x = y → f a = y) →
+  Lemma tac_vm_compute_hint {A B} Δ (f : A → option B) a (Q : B → iProp Σ) x:
+    (∀ y, Some x = y → f a = y) →
     envs_entails Δ (Q x) →
     envs_entails Δ (vm_compute_hint f a Q).
-  Proof. naive_solver. Qed.
+  Proof.
+    rewrite envs_entails_eq. intros ? HQ.
+    etrans; [done|]. etrans; [ |apply: bi.exist_intro].
+    iIntros "$ !%". naive_solver.
+  Qed.
 
   Lemma tac_protected_eq_app {A} (f : A → Prop) a :
     f a → f (protected a).

theories/lithium/simpl_instances.v

@@ -82,6 +82,11 @@ Proof. destruct b; done. Qed.
 Global Instance simpl_negb_false b: SimplBothRel (=) (negb b) false (b = true).
 Proof. destruct b; done. Qed.
 
+Global Instance simpl_eqb_true b1 b2: SimplBothRel (=) (eqb b1 b2) true (b1 = b2).
+Proof. destruct b1, b2; done. Qed.
+Global Instance simpl_eqb_false b1 b2: SimplBothRel (=) (eqb b1 b2) false (b1 = negb b2).
+Proof. destruct b1, b2; done. Qed.
+
 Global Instance simpl_min_glb_nat n1 n2 m : SimplBoth (m ≤ n1 `min` n2)%nat (m ≤ n1 ∧ m ≤ n2)%nat.
 Proof. rewrite /SimplBoth. lia. Qed.
 Global Instance simpl_min_glb n1 n2 m : SimplBoth (m ≤ n1 `min` n2) (m ≤ n1 ∧ m ≤ n2).