Reduce closed terms of type Z

theories/lithium/base.v

@@ -47,6 +47,21 @@ Ltac get_head e :=
   | _    => constr:(e)
   end.
 
+(* Checks that a term is closed using a trick by Jason Gross. *)
+Ltac check_closed t :=
+  assert_succeeds (
+    let x := fresh "x" in
+    exfalso; pose t as x; revert x;
+    repeat match goal with H : _ |- _ => clear H end;
+    lazymatch goal with H : _ |- _ => fail | _ => idtac end
+  ).
+
+Tactic Notation "reduce_closed" constr(x) :=
+  check_closed x;
+  let r := eval vm_compute in x in
+  change_no_check x with r in *
+.
+
 Definition Z_of_bool (b : bool) : Z :=
   if b then 1 else 0.
 Typeclasses Opaque Z_of_bool.

theories/lithium/solvers.v

@@ -162,10 +162,23 @@ Ltac enrich_context :=
 Ltac solve_goal_prepare_tac := idtac.
 Ltac solve_goal_normalized_prepare_tac := idtac.
 
+Local Open Scope Z_scope.
+Ltac reduce_closed_Z_tac := idtac.
+Ltac reduce_closed_Z :=
+  idtac;
+  reduce_closed_Z_tac;
+  repeat match goal with
+  | |- context [?a ≪ ?b] => progress reduce_closed (a ≪ b)
+  | H : context [?a ≪ ?b] |- _ => progress reduce_closed (a ≪ b)
+  | |- context [?a ≫ ?b] => progress reduce_closed (a ≫ b)
+  | H : context [?a ≫ ?b] |- _ => progress reduce_closed (a ≫ b)
+  end.
+
+
 Ltac solve_goal :=
   try fast_done;
   solve_goal_prepare_tac;
   normalize_and_simpl_goal;
-  solve_goal_normalized_prepare_tac; enrich_context;
+  solve_goal_normalized_prepare_tac; reduce_closed_Z; enrich_context;
   repeat case_bool_decide => //; repeat case_decide => //; repeat case_match => //;
   refined_solver lia.