Library Scat.MiscUtils

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

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

Definition try {A} (res: option A) (R: A → Prop) (E: Prop): Prop
  := match res with
     | None ⇒ E
     | Some v ⇒ R v
     end.

Lemma try_def {A} {res: option A} {R: A → Prop} {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: A → Prop} {E1 E2: Prop}:
  try res R1 E1 → (∀ a, R1 a → R2 a) → (E1 → E2) → try res R2 E2.
Proof.
  case res; simpl; auto.
Qed.

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

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

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

Open Scope lazy_bool_scope.

Hint Resolve eqb_prop Peqb_true_eq Zeq_bool_eq: eqtrue.

Ltac casebool t :=
 match t with
  | ?t1 &&& ?t2 ⇒ casebool 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
  | |- ?p ⇒ match 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 = ?y ⇒ apply f_equal; auto with eqtrue; eqtriv
  | |- (?f ?x = ?g ?y) ⇒ cutrewrite (f=g); auto with eqtrue; eqtriv
  | _ ⇒ idtac
  end.