Add invert_expr_subst

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index c403ed5e6..6a44a87aa 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -137,3 +137,15 @@ Global Arguments invert_LetIn {_ _ _ _} _.
 Global Arguments invert_Pair {_ _ _ _ _} _.
 Global Arguments invert_Abs {_ _ _ _ _} _ _.
 Global Arguments invert_Return {_ _ _ _} _.
+
+Ltac invert_expr_subst_step :=
+  match goal with
+  | _ => progress subst
+  | [ H : invert_Var ?e = Some _ |- _ ] => apply invert_Var_Some in H
+  | [ H : invert_Op ?e = Some _ |- _ ] => apply invert_Op_Some in H
+  | [ H : invert_LetIn ?e = Some _ |- _ ] => apply invert_LetIn in H
+  | [ H : invert_Pair ?e = Some _ |- _ ] => apply invert_Pair_Some in H
+  | [ H : invert_Abs ?e = _ |- _ ] => apply invert_Abs_Some in H
+  | [ H : invert_Return ?e = _ |- _ ] => apply invert_Return_Some in H
+  end.
+Ltac invert_expr_subst := repeat invert_expr_subst_step.