(* Copyright (c) 2017, the Dart project authors.  Please see the AUTHORS file
 * for details. All rights reserved. Use of this source code is governed by a
 * BSD-style license that can be found in the LICENSE file. *)

Require Import Common.
Require Export CpdtTactics.

Import OptionMonad.

Ltac extract E x y := set (x := E); assert (y : E = x); [auto|rewrite y in *].

Ltac force_expr E :=
  let v1 := fresh in
  let v2 := fresh in
  extract E v1 v2; destruct v1; [idtac|crush].

Lemma bind_some : forall A B x f, @opt_bind A B (Some x) f = f x.
Proof.
  crush.
Qed.

Ltac force_options :=
  repeat match goal with
         | [ H : (opt_bind ?y (fun x => ?z)) = Some ?w |- _ ] =>
           force_expr y; rewrite bind_some in H
         | [ H : (if ?cond then ?x else None) = Some ?w |- _ ] =>
           force_expr cond
         | [ H : (match ?x with _ => _ end) = Some ?w |- _ ] =>
           force_expr x
         end.

Inductive ltac_no_arg : Set :=
| Ltac_No_Arg : ltac_no_arg.