Library Scat.MiscUtils


Require Export Bool.
Require Import ZArith.
Require Export Sumbool.

Lemma ex_monotonic (A:Type) (P Q: AProp):
  ex P → ( x, P xQ x) → ex Q.
Proof.
  firstorder.
Qed.

Definition try {A} (res: option A) (R: AProp) (E: Prop): Prop
  := match res with
     | NoneE
     | Some vR v
     end.

Lemma try_def {A} {res: option A} {R: AProp} {E: Prop} :
   try res R E{ v | res=Some v & R v } + { res=None E }.
Proof.
  case res; simpl; firstorder.
Qed.

Lemma try_monotonic {A} {res} {R1 R2: AProp} {E1 E2: Prop}:
  try res R1 E1 → ( a, R1 aR2 a) → (E1E2) → try res R2 E2.
Proof.
  case res; simpl; auto.
Qed.

Definition ok {A} (res: option A) (R: AProp) := try res R False.

Lemma ok_def {A} {res: option A} {R: AProp} :
   ok res R v, res=Some v R v.
Proof.
  case res; simpl; firstorder.
Qed.

Lemma ok_monotonic A res (R1 R2: AProp):
  ok res R1 → ( a, R1 aR2 a) → ok res R2.
Proof.
  case res; simpl; auto.
Qed.

Tactics on booleans (typically about decidable equalities)

Open Scope lazy_bool_scope.

Hint Resolve eqb_prop Peqb_true_eq Zeq_bool_eq: eqtrue.

Ltac casebool t :=
 match t with
  | ?t1 &&& ?t2casebool t1
  | _case (sumbool_of_bool t); [ let nH := fresh "H" in intro nH; rewrite nH; simpl; auto with eqtrue |
                                      let nH := fresh "H" in intro nH; rewrite nH; simpl; try (discriminate) ]
 end.

Ltac caseeqtrue :=
  match goal with
  | |- ?pmatch p with
            | appcontext [?t = true] ⇒ casebool t
            end
  end.

Ltac eqtrue := repeat caseeqtrue.

Ltac decide_eqb_eq x y := generalize y; clear y; induction x; let y:=fresh "y" in intro y; destruct y; simpl; try (intuition discriminate).

Ltac eqtriv :=
  match goal with
  | |- ?x = ?yapply f_equal; auto with eqtrue; eqtriv
  | |- (?f ?x = ?g ?y) ⇒ cutrewrite (f=g); auto with eqtrue; eqtriv
  | _idtac
  end.