Qcert.Basic.Util.RUtil

Section RUtil.

  Section bools.

    Lemma andb_true_inversion:
      ∀ b1 b2 : bool,
        andb b1 b2 = true ↔ b1 = true ∧ b2 = true.

    Lemma four_cases {A:Type} :
      ∀ (p1 p2: A → bool) (a:A),
        ((((p1 a) = true) ∧ ((p2 a) = true)) ∨
         (((p1 a) = true) ∧ ((p2 a) = false))) ∨
        ((((p1 a) = false) ∧ ((p2 a) = true)) ∨
         (((p1 a) = false) ∧ ((p2 a) = false))).

    Lemma two_cases {A:Type} :
      ∀ (p: A → bool) (a:A),
        ((p a) = true) ∨ ((p a) = false).

    Lemma notand p q:
      ~(p ∨ q) → ¬p ∧ ¬q.

    Lemma eq_implies_pred {A:Type} :
      ∀ (p:A → bool), ∀ (x1 x2:A),
          x1 = x2 → (p x1) = (p x2).

    Lemma not_pred_implies_neq {A:Type}:
      ∀ (p:A → bool), ∀ (x1 x2:A),
          (p x1) ≠ (p x2) → x1 ≠ x2.

  End bools.

  Section In.
    Context {A:Type}.

    Lemma In_app (x:A) (l1 l2:list A):
      In x (l1 ++ l2) → In x l1 ∨ In x l2.

    Lemma In_app_comm (v:A) (l1 l2:list A) :
      In v (l1++l2) → In v (l2++l1).

    Lemma In_app_iff (v:A) (l1 l2:list A) :
      In v (l1++l2) ↔ In v (l2++l1).

    Lemma find_In {f l} {b:A} : find f l = Some b → In b l.

    Lemma find_correct {f l} {b:A} : find f l = Some b → f b = true.

    Lemma app_or_in (x:A) (l1 l2: list A) :
      In x (l1 ++ l2) → In x l1 ∨ In x l2.

    Lemma app_or_in_iff (x:A) (l1 l2: list A) :
      In x (l1 ++ l2) ↔ In x l1 ∨ In x l2.

    Lemma in_or_not (eqd:∀ a a':A, {a=a'} + {a≠a'}) (l:list A) a:
      (In a l) ∨ ~(In a l).

    Lemma nin_app_or (x:A) a b :
      (¬ In x (a ++ b)) ↔ (¬ In x a ∧ ¬ In x b).

    Lemma in_in_app_false {l l1 l2} :
      (∀ x:A,
          In x l →
          In x (l1 ++ l2) → False) →
      ((∀ x,
           In x l →
           In x l1 → False) ∧
       (∀ x,
           In x l →
           In x l2 → False)).

    Lemma in_in_cons_app_false {v l l1 l2} :
      (∀ x:A,
          In x l →
          v = x ∨ In x (l1 ++ l2) → False) →
      ((∀ x,
           In x l →
           In x (l1) → False) ∧
       (∀ x,
           In x l →
           In x (l2) → False) ∧
       ¬ (In v l)).

    Lemma in_in_cons_cons_app_app_false {v v0 l l1 l2 l3} :
      (∀ x:A,
          In x l →
          v = x ∨ v0 = x ∨ In x (l1 ++ l2 ++ l3) → False) →
      ((∀ x,
           In x l →
           In x l1 → False) ∧
       (∀ x,
           In x l →
           In x l2 → False) ∧
       (∀ x,
           In x l →
           In x l3 → False) ∧
       ¬ (In v l) ∧
       ¬ (In v0 l)).

  End In.

  Section forallt.
    Inductive Forallt {A : Type} (P : A → Type) : list A → Type :=
      Forallt_nil : Forallt P nil
    | Forallt_cons : ∀ (x : A) (l : list A),
        P x → Forallt P l → Forallt P (x :: l).

    Lemma list_Forallt_eq_dec {A:Type}:
      ∀ (c l: list A),
        Forallt (fun x : A ⇒ ∀ y : A, {x = y} + {x ≠ y}) c → {c = l} + {c ≠ l}.

    Lemma forallt_impl {A} {P1 P2:A→Type} {l:list A} :
      Forallt P1 l → Forallt (fun x ⇒ P1 x → P2 x) l → Forallt P2 l.

    Lemma forallt_weaken {A} P : (∀ x:A, P x) → ∀ l, Forallt P l.

    Lemma Forallt_inv: ∀ A P (a:A) l, Forallt P (a :: l) → P a.

    Lemma Forallt_inv2: ∀ A P (a:A) l, Forallt P (a :: l) → Forallt P l.


    Lemma Forallt_In {A:Type} {P:A→Type} {r} {eq:EqDec A eq}:
      Forallt P r → ∀ a, In a r → P a.

    Lemma Forall_app {A} (P:A→Prop) (l1 l2:list A):
      Forall P l1 → Forall P l2 →
      Forall P (l1 ++ l2).

    Lemma Forall_app_inv {A : Type} {P : A → Prop} (l1 l2 : list A) :
      Forall P (l1 ++ l2) → Forall P l1 ∧ Forall P l2.

    Lemma Forall_map {A B} P (f:A→B) l:
      Forall P (map f l) ↔
      Forall (fun x ⇒ P (f x)) l.

    Lemma Forall_impl_in {A} {P Q : A → Prop} {l} :
      (∀ a, In a l → P a → Q a) →
      Forall P l → Forall Q l.

    Lemma Forallt_Forall {A:Prop} (P:A→Prop) (l:list A) :
      Forallt P l → Forall P l.

  End forallt.

  Section forallb.

    Lemma forallb_ext {A} f1 f2 (l:list A) :
      (∀ x, In x l → f1 x = f2 x) →
      forallb f1 l = forallb f2 l.

    Lemma forallb_incl {A} f (l1 l2 : list A) :
      incl l1 l2 →
      forallb f l2 = true →
      forallb f l1 = true.

    Lemma forallb_app {A} (f:A→bool) l1 l2 :
      forallb f (l1 ++ l2) = true ↔
      (forallb f l1 = true ∧ forallb f l2 = true).

    Lemma forallb_map {A B} f (mf:A→B) m : forallb f (map mf m) = forallb ((fun x ⇒ f (mf x))) m.

    Lemma existsb_not_forallb {A} f (l:list A)
      : existsb f l = negb (forallb (fun x ⇒ negb (f x)) l).

    Lemma forallb_not_existb {A} f (l:list A)
      : forallb f l = negb (existsb (fun x ⇒ negb (f x)) l).

    Lemma map_eq {A B} {f g:A→B} {l} :
      Forall (fun x ⇒ f x = g x) l →
      map f l = map g l.

    Lemma map_cons {A B:Type} (f:A→B) (l:list A) (a:A) :
      map f (a::l) = (f a)::map f l.

    Lemma map_eq_cons {A B} (f : A → B) (l:list A) b l' :
      map f l = b::l' →
      {a : A & {ls:list A | l = a::ls ∧f a = b ∧ map f ls = l'}}.

  End forallb.

  Section pairs.

    Lemma pair_eq_dec {A B:Type} (a1:A) (b1:B) (a2:A) (b2:B) :
      {a1 = a2} + {a1 ≠ a2} →
      {b1 = b2} + {b1 ≠ b2} →
      {(a1, b1) = (a2, b2)} + {(a1, b1) ≠ (a2, b2)}.


    Global Instance string_eqdec : EqDec String.string eq := String.string_dec.
    Global Instance pair_eqdec {A B} `{EqDec A eq} `{EqDec B eq} : EqDec (prod A B) eq.

    Global Instance option_eqdec {A:Type} `{EqDec A eq}: EqDec (option A) eq.

  End pairs.


  Section arith.

    Lemma min_zero:
      ∀ (n1 n2:nat), min n1 (S n2) = 0 → n1 = 0.

    Lemma min_against_one:
      ∀ (n:nat), min n 1 = 0 ∨ min n 1 = 1.

    Lemma compare_either (n1 n2:nat):
      (n1 ≤ n2) ∨ (n2 ≤ n1).

    Lemma min_one_yields_one:
      ∀ n:nat, min n 1 = 1 → 1 ≤ n.

    Lemma fold_left_arith_dist1 {A} (x0:nat) (l:list A) (f:A → nat):
      fold_left (fun (x:nat) (y:A) ⇒ (f y) + x) l x0 =
      (fold_left (fun (x:nat) (y:A) ⇒ (f y) + x) l 0) + x0.

    Lemma fold_left_arith_dist2 {A} (x0 n0:nat) (l:list A) (f:A → nat):
      fold_left (fun (x:nat) (y:A) ⇒ n0 × (f y) + x) l x0 =
      n0 × (fold_left (fun (x:nat) (y:A) ⇒ (f y) + x) l 0) + x0.

    Lemma fold_left_arith_dist3 {A} (x0 n0:nat) (l:list A) (f:A → nat):
      n0 × (fold_left (fun (x:nat) (y:A) ⇒ (f y) + x) l 0) + x0 =
      n0 × (fold_left (fun (x:nat) (y:A) ⇒ x + (f y)) l 0) + x0.

    Lemma fold_left_arith_dist4 {A} (x0 n0:nat) (l:list A) (f:A → nat):
      fold_left (fun (x:nat) (y:A) ⇒ n0 × (f y) + x) l x0 =
      n0 × (fold_left (fun (x:nat) (y:A) ⇒ x + (f y)) l 0) + x0.

  End arith.

  Section Zutil.

    Definition ZToSignedNat (z:Z) : (bool×nat) :=
      match (Z.sgn z) with
      | -1 ⇒ (false,(Z.to_nat z))
      | _ ⇒ (true, (Z.to_nat z))
      end.

    Lemma pos_succ_inv (n1 n2:positive):
      (Pos.succ n1 = Pos.succ n2 → n1 = n2).

    Lemma Pos_of_nat_inv (n1 n2:nat) :
      Pos.of_nat (S n1) = Pos.of_nat (S n2) → n1 = n2.

    Lemma of_nat_inv (n1 n2:nat) :
      Z.of_nat n1 = Z.of_nat n2 → n1 = n2.

    Lemma pos_succ_nat_inv (n1 n2:nat) :
      Pos.of_succ_nat n1 = Pos.of_succ_nat n2 → n1 = n2.

    Global Instance Z_eqdec : EqDec Z eq.

  End Zutil.

  Section iter.
    Lemma repeat_plus {A} (x:A) (n1 n2:nat) :
      repeat x (n1+n2) = repeat x n1 ++ repeat x n2.

    Fixpoint iter {A} (f:A→A) (iterations:nat) (a:A)
      := match iterations with
         | 0 ⇒ a
         | S n ⇒ iter f n (f a)
         end.

    Lemma iter_fold_left_list {A B} (f:A→A) (l:list B) (a:A)
      : iter f (length l) a = fold_left (fun x y ⇒ f x) l a.

    Lemma iter_fold_left_repeat {A} (f:A→A) (iterations:nat) (a:A)
      : iter f iterations a = fold_left (fun x y ⇒ f x) (repeat 0 iterations) a.

    Lemma iter_fold_right_list {A B} (f:A→A) (l:list B) (a:A)
      : iter f (length l) a = fold_right (fun x y ⇒ f y) a l.

    Lemma iter_plus {A} (f:A→A) (iterations1 iterations2:nat) (a:A) :
      iter f (iterations1+iterations2) a = iter f iterations2 (iter f iterations1 a).

    Lemma iter_trans {A} (R:relation A) {pre:PreOrder R} f
          (pf:∀ x, R x (f x)) (iterations:nat) a :
      R a (iter f iterations a).

  End iter.

  Section cost.

    Context {A:Type}.
    Function iter_cost (optim: A → A) (cost: A → nat) (p: A) { measure cost p } :=
      let p' := optim p in
      if lt_dec (cost p') (cost p)
      then iter_cost optim cost p'
      else p.

    Lemma iter_cost_trans (R:relation A) {pre:PreOrder R} f
          (pf:∀ x, R x (f x)) (cost:A→nat) a :
      R a (iter_cost f cost a).

  End cost.

  Section vm.
    Definition is_true {A B} (x:{A}+{B}) : bool :=
      Eval vm_compute in (if x then true else false).

    Definition holds {A B} (x:{A}+{B}) : Prop :=
      is_true x = true.
  End vm.

End RUtil.



Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.










Definition brand := string.

Class ToString (A:Type)
  := {
      toString (a:A) : string
      }.