add via_vm_compute

theories/lithium/infrastructure.v

@@ -47,3 +47,19 @@ Class CanSolve (P : Prop) : Prop := can_solve: P.
 Definition shelve_hint (P : Prop) : Prop := P.
 Typeclasses Opaque shelve_hint.
 Arguments shelve_hint : simpl never.
+
+(** * [via_vm_compute]
+  [via_vm_compute f a] is equivalent to [f a] but tells the automation that it should
+  be reduced using [vm_compute]
+ *)
+Definition via_vm_compute_def {A B} (f : A → B) (x : A) : B :=
+  f x.
+Definition via_vm_compute_aux : seal (@via_vm_compute_def). by eexists. Qed.
+Definition via_vm_compute := unseal via_vm_compute_aux.
+Definition via_vm_compute_eq' : @via_vm_compute = @via_vm_compute_def :=
+  seal_eq via_vm_compute_aux.
+Arguments via_vm_compute {_ _} _ _.
+
+Lemma via_vm_compute_eq {A B} (f : A → B) x:
+  via_vm_compute f x = f x.
+Proof. rewrite via_vm_compute_eq'. done. Qed.

theories/lithium/interpreter.v

@@ -658,7 +658,13 @@ Ltac liSideCond :=
   | |- ?P ∧ _ =>
     lazymatch P with
     | shelve_hint _ => split; [ unfold shelve_hint; shelve |]
-    | _ => first [ progress normalize_goal_and |
+    | _ => first [
+      match P with
+      | context [via_vm_compute ?f ?a] =>
+        rewrite (via_vm_compute_eq f a);
+        vm_compute (f a)
+      end |
+      progress normalize_goal_and |
     lazymatch P with
     | context [protected _] => first [
         split; [ solve_protected_eq |]; unfold_instantiated_evars