change implementation of via_vm_compute and add negb simpl instances

theories/lithium/interpreter.v

@@ -665,14 +665,18 @@ Ltac liAccu :=
 
 Ltac liSideCond :=
   lazymatch goal with
-  | |- ?P ∧ _ =>
+  | |- ?P ∧ ?Q =>
     lazymatch P with
     | shelve_hint _ => split; [ unfold shelve_hint; li_shelve_sidecond |]
     | _ => first [
       match P with
-      | context [via_vm_compute ?f ?a] =>
+      | context C [via_vm_compute ?f ?a] =>
         rewrite (via_vm_compute_eq f a);
-        vm_compute (f a)
+        (* TODO: using [vm_compute (f a)] leads to very slow QED. Why is this the case? *)
+        (* vm_compute (f a) *)
+        let x := eval vm_compute in (f a) in
+        let P' := context C [ x ] in
+        change_no_check (P' ∧ Q)
       end |
       progress normalize_goal_and |
     lazymatch P with

theories/lithium/simpl_instances.v

@@ -77,6 +77,11 @@ Proof. split; destruct b; naive_solver. Qed.
 Global Instance simpl_Is_true_false b : SimplBoth (¬ Is_true b) (b = false).
 Proof. split; destruct b; naive_solver. Qed.
 
+Global Instance simpl_negb_true b: SimplBothRel (=) (negb b) true (b = false).
+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_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).