Add SideConditionFramework

1 files changed, 13 insertions, 0 deletions

diff --git a/src/Specific/Framework/SideConditionFramework.v b/src/Specific/Framework/SideConditionFramework.v
new file mode 100644
index 000000000..51322b129
--- /dev/null
+++ b/src/Specific/Framework/SideConditionFramework.v
@@ -0,0 +1,13 @@
+Require Import Crypto.Util.Decidable.
+
+Definition vm_decide_package (P : Prop) := P.
+Definition cbv_minus_then_vm_decide_package {T} (ident : T) (P : Prop) := P.
+Definition vm_compute_reflexivity_package (P : Prop) := P.
+
+Ltac autosolve else_tac :=
+  lazymatch goal with
+  | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide
+  | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide
+  | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity
+  | _ => else_tac ()
+  end.