1 files changed, 16 insertions, 0 deletions
diff --git a/src/Util/Tactics/SimplifyRepeatedIfs.v b/src/Util/Tactics/SimplifyRepeatedIfs.v
new file mode 100644
index 000000000..54d79ee48
--- /dev/null
+++ b/src/Util/Tactics/SimplifyRepeatedIfs.v
@@ -0,0 +1,16 @@
+Ltac simplify_repeated_ifs_step :=
+  match goal with
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let x' := match x with
+                 | context x'[b] => let x'' := context x'[true] in x''
+                 end in
+       let G' := context G[if b then x' else y] in
+       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let y' := match y with
+                 | context y'[b] => let y'' := context y'[false] in y''
+                 end in
+       let G' := context G[if b then x else y'] in
+       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
+  end.
+Ltac simplify_repeated_ifs := repeat simplify_repeated_ifs_step.