Module RUtil

Require Import List.
Require Import Sumbool.

Require Import Permutation.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Peano_dec.


Ltac dest_eqdec :=
  match goal with
  | [|- context [eq_nat_dec ?x ?y]] => destruct (eq_nat_dec x y)
  | [H: context [eq_nat_dec ?x ?y] |- _] => destruct (eq_nat_dec x y)
                                                     
  | [|- context [@equiv_dec ?a ?b ?c ?d ?x ?y]] => destruct (@equiv_dec a b c d x y)
  | [H: context [@equiv_dec ?a ?b ?c ?d ?x ?y] |- _] => destruct (@equiv_dec a b c d x y)
  end; unfold Equivalence.equiv, RelationClasses.complement in *; try subst.

Section RUtil.

  Section bools.
  
    Require Import Bool.
    Lemma andb_true_inversion:
      forall b1 b2 : bool,
        andb b1 b2 = true <-> b1 = true /\ b2 = true.

    Lemma four_cases {A:Type} :
      forall (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} :
      forall (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} :
      forall (p:A -> bool), forall (x1 x2:A),
          x1 = x2 -> (p x1) = (p x2).
  
    Lemma not_pred_implies_neq {A:Type}:
      forall (p:A -> bool), forall (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:forall 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} :
      (forall x:A,
          In x l ->
          In x (l1 ++ l2) -> False) ->
      ((forall x,
           In x l ->
           In x l1 -> False) /\
       (forall x,
           In x l ->
           In x l2 -> False)).

    Lemma in_in_cons_app_false {v l l1 l2} :
      (forall x:A,
          In x l ->
          v = x \/ In x (l1 ++ l2) -> False) ->
      ((forall x,
           In x l ->
           In x (l1) -> False) /\
       (forall 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} :
      (forall x:A,
          In x l ->
          v = x \/ v0 = x \/ In x (l1 ++ l2 ++ l3) -> False) ->
      ((forall x,
           In x l ->
           In x l1 -> False) /\
       (forall x,
           In x l ->
           In x l2 -> False) /\
       (forall 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 : forall (x : A) (l : list A),
        P x -> Forallt P l -> Forallt P (x :: l).
  
    Lemma list_Forallt_eq_dec {A:Type}:
      forall (c l: list A),
        Forallt (fun x : A => forall 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 : (forall x:A, P x) -> forall l, Forallt P l.

    Lemma Forallt_inv: forall A P (a:A) l, Forallt P (a :: l) -> P a.
    
    Lemma Forallt_inv2: forall A P (a:A) l, Forallt P (a :: l) -> Forallt P l.

    Require Import RelationClasses.
    Require Import EquivDec.
    Require Import Equivalence.

    Lemma Forallt_In {A:Type} {P:A->Type} {r} {eq:EqDec A eq}:
      Forallt P r -> forall 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} :
      (forall 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) :
      (forall 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)}.

    Require String.

    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.

  Require Import Omega.
  
  Section arith.

    Lemma min_zero:
      forall (n1 n2:nat), min n1 (S n2) = 0 -> n1 = 0.

    Lemma min_against_one:
      forall (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:
      forall 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.
    Require Import ZArith Zdigits Znat.
    Open Scope Z_scope.
  
    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:forall x, R x (f x)) (iterations:nat) a :
      R a (iter f iterations a).

  End iter.

  Section cost.
    Require Import Recdef.
    Require Import Compare_dec.

    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:forall 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.

Require String.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

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.


Ltac notHyp P :=
  match goal with
    | [ _ : P |- _ ] => fail 1
    | _ => idtac
  end.

Ltac extend P :=
  let t := type of P in
  notHyp t; generalize P; intro.

Ltac match_destr
  := match goal with [|- context [match ?x with _ => _ end]] => destruct x end; trivial; try discriminate.

Ltac match_destr_in H
  := match type of H with context [match ?x with _ => _ end] => destruct x end; trivial; try discriminate.

Ltac match_case
  := match goal with [|- context [match ?x with _ => _ end]] => case_eq x end; trivial; try discriminate.

Ltac match_case_in H
  := match type of H with context [match ?x with _ => _ end] => case_eq x end; trivial; try discriminate.


Ltac cut_to H :=
  match type of H with
    | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
    | _ -> ?b => cut (b); [clear H; intros H|apply H]
  end.

Ltac invcs H := inversion H; clear H; try subst.

Require Import String.
Definition brand := string.

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