Module Utils

Require Import Coqlib.
Require Integers Pointers Errors.
Require Import BinPos List Utf8.
Require Import Values Maps.

Set Implicit Arguments.

Tactic Notation "inv" ident(X) := inversion X; try (subst; clear X).

Ltac discr :=
  match goal with
    | H : forall _, _ <> _ |- _ => eelim H; reflexivity
  end || idtac.

Lemma true_neq_false : true <> false.

Ltac tnf := match goal with
              | H : true = false |- _ => elim (true_neq_false H)
              | H : false = true |- _ => elim (true_neq_false (eq_sym H))
            end.

Notation "'do' X <- A ; B" := (optbind (fun X => B) A)
 (at level 200, X ident, A at level 100, B at level 200).

Definition bind2 (A B C: Type) (f: option (A*B)) (g: A -> B -> option C) : option C :=
  match f with Some (a,b) => g a b | None => None end.

Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
 (at level 200, X ident, Y ident, A at level 100, B at level 200).

Lemma opt_bind_inversion {A B g f} {b:B} :
  optbind g f = Some b ->
  exists a : A, f = Some a.

Lemma opt_bind_inversion' {A B g f} :
  optbind g f <> @None B ->
  exists a : A, f = Some a.

Ltac opt_bind_inv t :=
  match goal with
    | H : @None _ <> optbind _ _ |- _ => symmetry in H; opt_bind_inv t
    | H : Some _ = optbind _ _ |- _ => symmetry in H; opt_bind_inv t
    | H : optbind _ _ = Some _ |- _ =>
      let H' := fresh "Hbind" in
      destruct (opt_bind_inversion H) as [t H']; rewrite H' in H; simpl in H
    | H : optbind _ _ <> @None _ |- _ =>
      let H' := fresh "Hbind" in
      destruct (opt_bind_inversion' H) as [t H']; rewrite H' in H; simpl in H
  end.

  Ltac bi :=
    match goal with
      | [H: Errors.bind _ _ = Errors.OK _ |- _] =>
          let u := fresh "Hbi" in
          destruct (Errors.bind_inversion _ _ H) as (? & u & ?); clear H;
          (match goal with
             | [K: unit |- _] => destruct K
           end || idtac)
    end.

  Ltac bif2 :=
    match goal with
      | [H: context [if ?c then _ else _] |- _] =>
          let Q := fresh "Htrue" in
          case_eq c; intros Q; rewrite Q in H; clarify
    end.

  Ltac autorw :=
    match goal with
      | [H: _ = _ |- _] => rewrite H in *
    end.

  Ltac autorw' := repeat (progress (autorw; clarify)).

Tactic Notation "app_inv" :=
  match goal with
    | H : _ ++ _ :: nil = _ ++ _ :: nil |- _ =>
      destruct (app_inj_tail _ _ _ _ H) as [?Hsnoc0 ?Hsnoc]; subst; clear H
    | H : nil = _ ++ _ :: _ |- _ => elim (app_cons_not_nil _ _ _ H)
    | H : _ ++ _ :: _ = nil |- _ => eelim app_cons_not_nil; symmetry; eassumption
    | H : _ ++ _ :: _ = _ :: nil |- _ => rewrite <- app_nil_l in H;
      destruct (app_inj_tail _ _ _ _ H) as [?Hsnoc0 ?Hsnoc]; subst; clear H
  end.

Lemma canap : forall {A l} {e:A} {x f}, l ++ e :: nil = x::f ->
                                        (l = nil /\ f = nil /\ x = e)
                                \/ (exists m, l = x::m /\ f = m++e::nil).

Inductive lift_exists_list {X Y : Type} (R: X -> Y -> Prop) : list X -> Y -> Prop :=
| lel_hd x tl y (HR: R x y) : lift_exists_list R (x::tl) y
| lel_tl hd tl y (HR: lift_exists_list R tl y) : lift_exists_list R (hd::tl) y
.

Lemma in_lift_exists_list {X Y} (R: X -> Y -> Prop) :
  forall y l x,
    R x y -> In x l -> lift_exists_list R l y.

Lemma lift_exists_list_in {X Y} (R: X -> Y -> Prop) :
  forall y l,
    lift_exists_list R l y ->
    exists x, R x y /\ In x l.

Inductive list_forall {X : Type} (P: X -> Prop) : list X -> Prop :=
| lf_nil : list_forall P nil
| lf_cons x l : P x -> list_forall P l -> list_forall P (x::l)
.

Inductive lift_forall_list {X Y : Type} (R: X -> Y -> Prop) : list X -> list Y -> Prop :=
| lfl_nil : lift_forall_list R nil nil
| lfl_cons x y xl yl (HEAD: R x y) (TAIL: lift_forall_list R xl yl)
  : lift_forall_list R (x::xl) (y::yl).

Lemma in_lift_list {X Y} R : ∀ l l',
  lift_forall_list R l l' ->
  ∀ x : X, In x l -> ∃ y : Y, (In y l' ∧ R x y).

Lemma lfl_snoc {X Y} (R:X→Y→Prop) : ∀ xl yl x y,
  lift_forall_list R (xl ++ x :: nil) (yl ++ y :: nil) <->
                   (lift_forall_list R xl yl ∧ R x y).

Lemma lfl2 A B R :
  forall x y, @list_forall2 A B R x y <-> @lift_forall_list A B R x y.

Lemma lessdef_list_length {l l'} :
  Val.lessdef_list l l' →
  length l = length l'.

Inductive lift_opt {X Y} (R: X -> Y -> Prop) : option X -> option Y -> Prop :=
| lo_none : lift_opt R None None
| lo_some x y (HR: R x y) : lift_opt R (Some x) (Some y)
.
Hint Constructors lift_opt.

Definition list_max := fold_left Pmax.

Notation "M '{{' key '}}'" :=
  (match PTree.get key M with Some l => l | None => @nil _ end)(at level 0, no associativity).

Definition of_pair_list {A} (elt: list (positive * A)) : PTree.t A :=
  fold_left
    (fun m kv =>
       m ! (fst kv) <- (snd kv)
    )
    elt
    (PTree.empty A).

Fixpoint of_list' {A} (elt: list A) id : PTree.t A :=
  match elt with
    | nil => PTree.empty _
    | e::elt' =>
        let m := of_list' elt' (Psucc id) in
          m ! id <- e
  end.

Definition of_list {A} (elt: list A) : PTree.t A := of_list' elt xH.

Section FIND_P.
Context {A : Type}.
Variable P : A -> Prop.
Hypothesis P_dec : forall a : A, { P a } + { ~ P a }.

Variable t : PTree.t A.

Definition find_p' : option positive :=
  PTree.fold (fun res i a =>
                match P_dec a with
                  | left _ => Some i
                  | right _ => res
                end
             ) t None.

Lemma find_p_correct :
  match find_p' with
    | Some i => match t ! i with Some a => P a | None => False end
    | None => forall i a, t ! i = Some a -> ~ P a
  end.

Definition find_p : { i : positive | match t ! i with Some a => P a | None => False end }
                      + { forall i a, t ! i = Some a -> ~ P a }.

End FIND_P.

Section REV_FIND.

Context {A : Type}.
Hypothesis A_eq : forall a a' : A, { a = a' } + { a <> a' }.
Variable t : PTree.t A.

Definition rev_find a : option positive :=
  find_p' _ (A_eq a) t.

Lemma rev_find_correct a :
  match rev_find a with
    | Some i => t ! i = Some a
    | None => forall i, t ! i <> Some a
  end.

End REV_FIND.

Section FORALL.

Context {A : Type}.
Variable P : positive -> A -> Prop.
Hypothesis P_dec : forall k (a : A), { P k a } + { ~ P k a }.

Variable t : PTree.t A.

Definition forall_spec (F : bool) : Prop :=
  if F
  then forall k v, t ! k = Some v -> P k v
  else exists k, exists v, t ! k = Some v /\ ~ P k v.

Definition tree_forall : bool :=
  PTree.fold
       (fun (b:bool) k v => if b then if P_dec k v then true else false else false)
       t
       true.

Lemma tree_forall_correct : forall_spec tree_forall.

End FORALL.

Section FORALLB.

Context {A: Type}.
Variable P : positive -> A -> bool.

Variable t : PTree.t A.

Let P' : positive -> A -> Prop := fun k a => P k a.
Lemma P'_dec : forall k a, { P' k a } + { ~ P' k a }.

Definition tree_forallb : bool :=
  tree_forall P' P'_dec t.

Corollary tree_forallb_correct :
  if tree_forallb
  then forall k v, t ! k = Some v -> P k v
  else exists k, exists v, t ! k = Some v /\ ~ P k v.

End FORALLB.

Section SUBTREE.

Context {A : Type}.
Variable t : PTree.t A.

Program Fixpoint subtree' acc id (lst: list positive) :
  option (PTree.t { i : positive | t ! i <> None }) :=
  match lst with
    | i :: lst' =>
        do m <- acc ;
        match t ! i as H return t ! i = H -> _ with
          | Some _ => fun K => subtree' (Some (m ! id <- (exist _ i _))) (Psucc id) lst'
          | None => fun _ => None
        end (eq_refl _)
    | nil => acc
  end.

Definition subtree lst := subtree' (Some (PTree.empty _)) xH lst.

Context {B:Type}.
Variable f : A -> B.
Lemma map_subtree_prop i : t ! i <> None -> (PTree.map (fun _ => f) t) ! i <> None.

Definition map_subtree (s : PTree.t { i : positive | t ! i <> None }) :
  PTree.t { i : positive | (PTree.map (fun _ => f) t) ! i <> None } :=
  PTree.map (fun _ (iH : { i : positive | t ! i <> None } ) =>
               match iH with exist i H =>
                               exist (fun j => (PTree.map (fun _ => f) t) ! j <> None)
                                     i (map_subtree_prop i H)
               end) s.

End SUBTREE.


Ltac tid_case tid :=
  intros ?t;
  case (peq t tid); intros ?Ht;
  [subst; repeat rewrite PTree.gss| repeat (rewrite PTree.gso;[|exact Ht])].

Tactic Notation "solve_by_inversion_step" tactic(t) :=
  match goal with
  | H : _ |- _ => solve [ inversion H; subst; t ]
  end
  || fail "because the goal is not solvable by inversion.".

Tactic Notation "solve" "by" "inversion" "1" :=
  solve_by_inversion_step idtac.
Tactic Notation "solve" "by" "inversion" "2" :=
  solve_by_inversion_step (solve by inversion 1).
Tactic Notation "solve" "by" "inversion" "3" :=
  solve_by_inversion_step (solve by inversion 2).
Tactic Notation "solve" "by" "inversion" :=
  solve by inversion 1.

Lemma last_eq {X:Type} : ∀l x d,
  last (l++x::@nil X) d = x.

Lemma last_cons {X:Type} : forall b (a c:X), last (a::b) c = last b a.


Tactic Notation ">" tactic(t) := t.
Tactic Notation "by" tactic(t) := t; fail "this goal should be proved at this point".

Ltac invh f :=
    match goal with
      [ id: f |- _ ] => inv id
    | [ id: f _ |- _ ] => inv id
    | [ id: f _ _ |- _ ] => inv id
    | [ id: f _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    end.


Require Import Coqlib.

Section MAPS.
Local Open Scope positive_scope.
Context {A:Type}.
Variable q : PTree.t A.

Lemma list_max_correct : ∀l x z, (In x l ∨ Ple x z) → Ple x (list_max l z).

Lemma list_max_bound : ∀l x z, Plt (list_max l z) x → (~ In x l) ∧ Plt z x.

Definition max_key : positive :=
  PTree.fold (fun acc k _ => Pmax acc k) q xH.

Lemma max_key_correct : ∀k,
  Plt max_key k → PTree.get k q = None.

End MAPS.

Section TREE_MAP_PARTIAL.

Context {A B: Type}.
Variable f : positive -> A -> Errors.res B.

Definition ptree_map_partial (t: PTree.t A) : Errors.res (PTree.t B) :=
  PTree.fold
       (fun q k a =>
          Errors.bind q
                (fun x =>
                   Errors.bind (f k a)
                         (fun y => Errors.OK (x ! k <- y))))
       t
       (Errors.OK (PTree.empty B)).

Lemma ptree_map_partial_spec t :
  match ptree_map_partial t with
    | Errors.OK t' =>
        (forall k a,
          t ! k = Some a -> exists b, f k a = Errors.OK b /\ t' ! k = Some b) /\
        (forall k, t ! k = None -> t' ! k = None)
    | Errors.Error msg =>
        exists k, exists a,
          t ! k = Some a /\ f k a = Errors.Error msg
  end.

Corollary ptree_map_partial_ok {t t'} :
  ptree_map_partial t = Errors.OK t' ->
        (forall k a,
          t ! k = Some a -> exists b, f k a = Errors.OK b /\ t' ! k = Some b) /\
        (forall k, t ! k = None -> t' ! k = None).

Corollary ptree_map_partial_ko {t msg} :
  ptree_map_partial t = Errors.Error msg ->
        exists k, exists a,
          t ! k = Some a /\ f k a = Errors.Error msg.

Corollary ptree_map_partial_inv {t t'} :
  ptree_map_partial t = Errors.OK t' ->
  forall k b,
    t' ! k = Some b ->
    exists a,
      t ! k = Some a /\ f k a = Errors.OK b.

End TREE_MAP_PARTIAL.

Section TREE_OPT_MAP.

Context {A B : Type}.
Variable f : A -> option B.
Variable t : PTree.t A.

Definition ptree_opt_map : PTree.t B :=
  PTree.fold (fun res k a => match f a with Some b => res ! k <- b | None => res end) t (PTree.empty B).

Lemma ptree_opt_map_spec :
  forall k,
    match t ! k, ptree_opt_map ! k with
      | None, None => True
      | None, _ => False
      | Some a, b => f a = b
    end.

End TREE_OPT_MAP.

Module Rset.
  Definition t := PTree.t unit.
  Local Notation elt := positive.
  Definition empty : t := PTree.empty _.
  Definition add (x:elt) (s:t) : t := PTree.set x tt s.
  Definition singleton (x:elt) : t := add x empty.
  Definition remove (x:elt) (s:t) : t := PTree.remove x s.
  Definition add_list (l:list elt) (s:t) : t := List.fold_right add s l.
  Definition remove_list (l:list elt) (s:t) : t := List.fold_right remove s l.
  Definition mem (x:elt) (s:t) : bool :=
    match PTree.get x s with
      | None => false
      | Some _ => true
    end.
  Definition union (s1 s2:t) : t :=
    PTree.combine (fun o1 o2 =>
      match o1, o2 with
        | None, None => None
        | _, _ => Some tt
      end) s1 s2.
  Definition inter (s1 s2:t) : t :=
    PTree.combine (fun o1 o2 =>
      match o1, o2 with
        | Some _, Some _ => Some tt
        | _, _ => None
      end) s1 s2.
  Definition forallb (f:elt->bool) (s:t) : bool :=
    PTree.fold (fun b x _ => b && f x) s true.

  Definition subset (r s:t) : bool :=
    forallb (fun x => mem x s) r.

  Section PROP.
      Lemma add_mem {s v} : mem v (add v s).
      Lemma add_mem_o {s v v'} : v <> v' -> mem v (add v' s) = mem v s.
      Lemma mem_add {s v v'} : mem v s -> mem v (add v' s).
      Lemma add_comm {s v v'} : add v (add v' s) = add v' (add v s).
      Lemma add_not_empty {s v} : add v s <> empty.
      Lemma mem_add_nop {s v} : mem v s -> add v s = s.

      Lemma remove_comm {s v v'} : remove v (remove v' s) = remove v' (remove v s).
      Lemma remove_add {s v} : ~ mem v s -> remove v (add v s) = s.
      Lemma remove_add_remove {s v} : remove v (add v s) = remove v s.
      Lemma add_remove {s v} : add v (remove v s) = add v s.
      Lemma not_mem_remove_nop {s v} : ~ mem v s -> remove v s = s.
      Lemma remove_not_mem {v s} : ¬ mem v (remove v s).
      Lemma mem_rmo {s v v'} : v <> v' -> mem v (remove v' s) = mem v s.
      Lemma empty_not_mem {v} : ~ mem v empty.

    Context { f : elt -> bool }.
    Lemma forallb_spec r :
      match forallb f r with
        | true => forall x, mem x r -> f x
        | false => exists x, mem x r /\ ~ f x
      end.
    Corollary forallb_forall {x r} :
      forallb f r -> mem x r -> f x.
    Corollary forall_forallb {r} :
      (∀ x, mem x r → f x) → forallb f r.

  End PROP.

    Lemma subset_spec {r s} : subset r s <-> ∀ x, mem x r → mem x s.

    Remark empty_subset {r} : subset empty r.

    Lemma subset_refl {r} : subset r r.

    Lemma subset_trans : transitive _ subset.

    Lemma subset_antisym : antisymmetric _ subset.

    Remark subset_empty {r} : subset r empty → r = empty.

    Lemma mem_singleton {x y} : mem x (singleton y) → x = y.

    Lemma subset_singleton : ∀ r x, subset r (singleton x) → r = empty ∨ r = singleton x.

    Lemma remove_subset {x r} : subset (remove x r) r.

    Lemma subset_add {v s} : subset s (add v s).

    Lemma add_singleton {v v' s} : add v s = singleton v' →
                                   v = v' ∧ subset s (singleton v).

    Lemma remove_last {v s} : remove v s = empty → subset s (singleton v).

    Lemma add_remove_comm {v v' s} :
      v ≠ v' →
      remove v' (add v s) = add v (remove v' s).
End Rset.

Section list.

Context {A:Type}.

Lemma In_eq_app: forall (x:A) l, In x l -> exists l1, exists l2, l = l1++x::l2.



Lemma eq_app_app: forall (a b:A) l1 l2 l3 l4, l1 ++ a :: l2 = l3 ++ b :: l4 -> a<>b ->
  (exists l, l1 = l3 ++ b :: l /\ l4 = l ++ a :: l2)
  \/
  (exists l, l3 = l1 ++ a :: l /\ l2 = l ++ b :: l4).


End list.

Reserved Notation "m ¡ l" (no associativity, at level 60).
Fixpoint get_list {X:Type} (m: PTree.t X) (l: list positive)
: option (list X) :=
  match l with
    | nil => Some nil
    | p::l' =>
      do x <- m ! p ;
      do r <- m ¡ l';
      Some (x :: r)
  end
where "m ¡ l" := (get_list m l).

Fixpoint fold_left2 {A B C: Type} (f: A → B → C → A) (z: A) (u: list B) (v: list C) : A :=
  match u, v with
    | b::u', c::v' => fold_left2 f (f z b c) u' v'
    | _, _ => z
  end.

Fixpoint fold_right2 {A B C: Type} (f: A → B → C → A) (z: A) (u: list B) (v: list C) : A :=
  match u, v with
    | b::u', c::v' => f (fold_right2 f z u' v') b c
    | _, _ => z
  end.

Class EqDec {X: Type} :=
{ eq_dec: ∀ x y: X, { x = y } + { x ≠ y }
}.

Definition upd `{X: Type} `{EqDec X} {Y} (f: X → Y) p (v:Y) := fun q => if eq_dec p q then v else f q.

Lemma upd_s `{X: Type} `{EqDec X} {Y} (f: X → Y) p v:
  (upd f p v) p = v.

Lemma upd_o `{X: Type} `{EqDec X} {Y} (f: X → Y) p v p' :
  p ≠ p' → (upd f p v) p' = f p'.

Ltac eq_case :=
  match goal with |- appcontext[ @eq_dec _ _ ?x ?y ] => case (eq_dec x y) end.

Instance ZEqDec : @EqDec Z := Build_EqDec Z_eq_dec.
Instance PosEqDec : @EqDec positive := Build_EqDec peq.
Instance IntEqDec : @EqDec Integers.int := Build_EqDec _.
Instance PtrEqDec : @EqDec Pointers.pointer := Build_EqDec _.

Section OPT_MAP.

  Context {A B: Type}.
  Variable (f: A → option B).

  Definition opt_map' (l: list A) : option (list B) → option (list B) :=
    fold_left (fun l a => do b <- f a; do l' <- l; Some (b::l')) l.

  Definition opt_map (l: list A) : option (list B) := opt_map' l (Some nil).

  Lemma opt_map'_none l: opt_map' l None = None.

  Lemma opt_map_none (l: list A) :
    opt_map l = None → ∃a, In a l ∧ f a = None.

  Lemma opt_map_some (l: list A) :
    opt_map l ≠ None → ∀a, In a l → f a ≠ None.

End OPT_MAP.

Ltac andb' a b :=
  match goal with
    | [H: is_true (_ && _) |- _ ] => unfold is_true in H; andb' a b
    | [H: _ && _ = true |- _ ] => apply andb_true_iff in H; destruct H as [a b]
  end.

Tactic Notation "andb" "as" ident(a) ident(b) := andb' a b.
Tactic Notation "andb" := let a := fresh "L" in let b := fresh "R" in andb' a b.