Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import Floats.
Require Import Integers.
Require Ascii.
Require String.
Require Import Relation_Operators.
Require Psatz.
Require Import Permutation.
Require Import List.

Tactics

Ltac exploit_dstr x :=
  let Hnew := fresh "Htmp"
    in exploit x ; eauto ; intros Hnew ; destruct Hnew as [] ; intuition.

Ltac boolInv :=
  match goal with
  | [ H: _ && _ = true |- _ ] =>
      destruct (andb_prop _ _ H); clear H; boolInv
  | [ H: proj_sumbool _ = true |- _ ] =>
      generalize (proj_sumbool_true _ H); clear H;
      let EQ := fresh in (intro EQ; try subst; boolInv)
  | _ =>
      idtac
  end.

Ltac revert_arith :=
  repeat
    (match goal with
       | H : Z |- _ => generalize dependent H
       | H : positive |- _ => generalize dependent H
       | H : N |- _ => generalize dependent H
       | H : nat |- _ => generalize dependent H
       | H : context[?X] |- _ => match type of X with
                | nat => generalize dependent H
                                   | Z => generalize dependent H
              | N => generalize dependent H
                              | positive => generalize dependent H
     end
     end
    ) ; clear ; intros.

Ltac lia :=
  (try revert_arith) ; zify ; unfold Z.succ in * ; Psatz.lia.

Fixpoint get_digits (z:Z) (p:positive) : list nat :=
  match p with
    | xH => nil
    | xO p | xI p =>
      let digit := (z - ((z/10)*10))%Z in
        match digit with
          | Zpos d => (nat_of_P d)::(get_digits (z/10) p)
          | Z0 => O::(get_digits (z/10) p)
          | _ => nil
        end
  end.

Fixpoint rm_zeros l :=
  match l with
    | nil => nil
    | O::m => rm_zeros m
    | x::m => l
  end.

Definition encode_ascii (n: nat) := (n + 48)%nat.

Fixpoint digits l :=
   match l with
     | nil => String.EmptyString
     | d::m => String.String (Ascii.ascii_of_nat (encode_ascii d)) (digits m)
   end.
 
Definition pos_to_string (p:positive) : String.string :=
  let ldigits := rm_zeros (rev (get_digits (Zpos p) p)) in
    digits ldigits.

Utilities on the option type

Definition get_opt {A B:Type} (f:A->B) (x:option A) : option B :=
  match x with
    | None => None
    | Some a => Some (f a)
  end.

Lemma option_map_some: forall A B (f:A->B) x i,
 option_map f x = Some i -> exists i', x = Some i'.

Global Hint Resolve option_map_some : core.

Properties about PTree

Require Import DLib.

Lemma PTree_xfold_none : forall (A B:Type) (f:A->positive->B->A) (m:PTree.t B) (x:A) p',
  (forall p, m!p = None) ->
  PTree.xfold f p' m x = x.
  
Lemma ptree_set_permut: forall r r0 r1 (v0 v1:val) t ,
  r0 <> r1 ->
  Maps.PTree.get r (Maps.PTree.set r0 v0 (Maps.PTree.set r1 v1 t)) =
  Maps.PTree.get r (Maps.PTree.set r1 v1 (Maps.PTree.set r0 v0 t)).

Lemma ptree_setset: forall r dst (v1 v2:val) t,
Maps.PTree.get dst (Maps.PTree.set r v2 (Maps.PTree.set r v1 t)) =
Maps.PTree.get dst (Maps.PTree.set r v2 t).
  

Definition forall_ptree {A:Type} (f:positive->A->bool) (m:Maps.PTree.t A) : bool :=
  Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true.

Remark ptree_forall:
  forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
  Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true = true ->
  forall i x, Maps.PTree.get i m = Some x -> f i x = true.

Lemma forall_ptree_true:
  forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
    forall_ptree f m = true ->
    forall i x, Maps.PTree.get i m = Some x -> f i x = true.

PTrees over pairs of positive

Require Maps2.

Module P2Map : MAP with Definition elt := (positive * positive)%type :=
  Maps2.MakeProdMap PMap PMap.

Notation "a #2 b" := (P2Map.get b a) (at level 1).
Notation "a ##2 b" := (List.map (fun r => P2Map.get r a) b) (at level 1).
Notation "a #2 b <- c" := (P2Map.set b c a) (at level 1, b at next level).
Notation "a !!2 b" := (P2Map.get b a) (at level 1).
Notation p2eq := P2Map.elt_eq.

Getting the index of an element in a list

Fixpoint get_index_acc (l:list positive) (a:positive) (acc: nat) : option nat :=
  match l with
    | nil => None
    | x::m =>
      if (peq x a)
      then Some acc
      else get_index_acc m a (acc+1)
  end.

Definition get_index (l:list positive) (a:positive) :=
  get_index_acc l a O.


Inductive nth_okp {A:Type}: nat -> list A -> Prop :=
  | nth_okp_headO : forall l e, nth_okp 0 (e::l)
  | nth_okp_headS : forall l e n, nth_okp n l -> nth_okp (S n) (e::l).

Lemma nth_okp_exists {A:Type}: forall (l: list A) k,
  nth_okp k l -> exists v, nth_error l k = Some v.

Lemma nth_okp_length : forall (A B:Type) k (l1:list A),
  nth_okp k l1 -> forall (l2:list B), length l1 = length l2 -> nth_okp k l2.


Lemma get_index_acc_progress: forall (l: list positive) (a b:positive) acc k,
  b <> a ->
  get_index_acc (b::l) a acc = Some k ->
  get_index_acc l a (acc+1) = Some k.

Lemma get_index_acc_ge_acc: forall l e acc k,
  get_index_acc l e acc = Some k ->
  ge k acc.

Lemma get_index_acc_inv2 : forall l a (acc acc' :nat) x,
  get_index_acc l a (acc+acc') = Some (x+acc')%nat ->
  get_index_acc l a acc = Some x.

Lemma get_index_some_sn: forall l a e k acc,
  a <> e ->
  get_index_acc (a :: l) e acc = Some ((k+1)%nat) ->
  get_index_acc l e acc = Some k.
  
Lemma get_index_some_in: forall l e k,
  get_index l e = Some k ->
  In e l.

Lemma get_index_acc_inv : forall l a (acc acc' :nat) x,
  get_index_acc l a acc = Some x ->
  get_index_acc l a (acc+acc') = Some (x+acc')%nat.
  
Lemma in_get_index_some: forall l a,
  In a l -> exists k, get_index l a = Some k.

Lemma get_index_some : forall l pc k,
  get_index l pc = Some k ->
  (k < length l)%nat.

Lemma get_index_nth_error: forall pc l k,
  get_index l pc = Some k ->
  nth_error l k = Some pc.

Lemma get_index_acc_nth_okp_aux : forall pc l k k',
  get_index_acc l pc k' = Some (k'+k)%nat -> nth_okp k l.

Lemma get_index_acc_nth_okp : forall pc l k,
  get_index l pc = Some k -> nth_okp k l.

Lemma in_tl_in_cons: forall (A:Type) (l: list A) (a e:A),
  In e l -> In e (a::l).

Lemma in_hd_in_cons: forall (A:Type) (l: list A) (a:A),
  In a (a::l).

Global Hint Resolve in_tl_in_cons: core.
Global Hint Resolve in_hd_in_cons: core.

Lemma app_cons_nil : forall (A:Type) (l l': list A) (n1 n2 : A),
  n1 :: nil = l ++ n2 :: l' ->
  (l = nil) /\ (l' = nil).

Lemma in_nth_error_some : forall (A: Type) (l: list A) (a: A),
  In a l ->
  (exists k, nth_error l k = Some a).

Lemma nth_error_nil_some {A: Type} : forall k (e: A),
  nth_error nil k = Some e -> False.

Lemma nth_error_some_in: forall (A:Type), forall k (l:list A) r,
  nth_error l k = Some r -> In r l.

Lemma nth_error_some_same_length {A B: Type}: forall (l1: list A) (l2: list B) k e,
  nth_error l1 k = Some e ->
  List.length l1 = List.length l2 ->
  exists e, nth_error l2 k = Some e.
  
Lemma map_in_some {A B :Type} : forall (f:A -> B) l b,
  In b (map f l) ->
  exists a, In a l /\ f a = b.

Lemma list_map_nth_some {A B : Type} : forall (f: A -> B) l a k,
  nth_error l k = Some a ->
  nth_error (map f l) k = Some (f a).

Lemma fold_left_inv {A : Type} : forall (f: A -> bool) (l: list A) (a : A) (res0:bool),
    fold_left (fun (res : bool) (i : A) => res && f i) (a::l) res0 =
    (f a) && fold_left (fun (res : bool) (i : A) => res && f i) l res0.

Lemma list_forall {A: Type}: forall (f: A -> bool) (l: list A),
  fold_left (fun (res : bool) (i : A) => res && f i) l true = true ->
  forall (i : A), In i l -> f i = true.

Fixpoint forall_list2 {A:Type} (f:A->A->bool) (l1 l2: list A) : bool :=
  match l1, l2 with
    | nil, nil => true
    | a1::q1, a2::q2 => f a1 a2 && (forall_list2 f q1 q2)
    | _, _ => false
  end.

Lemmas about positive

Lemma Ple_Plt_trans:
  forall (p q r: positive), Ple p q -> Plt q r -> Plt p r.

Lemma Ple_Plt_succ: forall p1 p2,
  Ple p1 p2 -> Plt p1 (Pos.succ p2).

The inclist predicate

Inductive inclist {A:Type} : list A -> list A -> Prop:=
| inclist_nil : forall l, inclist nil l
| inclist_cons1: forall l1 l2 b, inclist l1 l2 -> inclist l1 (b::l2)
| inclist_cons2: forall l1 l2 a, inclist l1 (a::l2) -> inclist (a::l1) (a::l2).

Lemma inclist_refl {A:Type} : forall (l: list A), inclist l l.

Lemma inclist_cons_in {A:Type} : forall l1 l2 (a:A),
  inclist (a :: l2) l1 -> In a l1.


Lemma inclist_indu : forall A l2 l1 (a:A),
  inclist (a::l1) l2 -> inclist l1 l2.

The alln predicate

Inductive alln {A:Type} (n:A) : list A -> Prop:=
| alln_nil : alln n nil
| alln_cons: forall m, alln n m -> alln n (n::m).

Additional definitions and properties of lists

Lemma list_nth_z_tonat {A: Type} : forall (l : list A) (n: Z) (a: A),
list_nth_z l n = Some a ->
n = Z0 \/ (exists p, n = Zpos p).
  
Lemma arith_utils: forall (n:Z) (n1: nat) ,
   Z.to_nat n = Datatypes.S n1 ->
   n1 = (Z.to_nat (Z.pred n)) .

Local Open Scope Z_scope.

Lemma arith_utils2: forall (n:Z) (n1: nat) ,
  n > 0 ->
  n1 = (Z.to_nat (Z.pred n)) ->
  Z.to_nat n = Datatypes.S n1.
  
Lemma list_nth_z_nth_error {A: Type} : forall (l : list A) (n: Z) (a: A),
list_nth_z l n = Some a ->
nth_error l (Z.to_nat n) = Some a.

Lemma nth_error_list_nth_z {A: Type} : forall (l : list A) (n: Z) (a: A),
n >= 0 ->
nth_error l (Z.to_nat n) = Some a ->
list_nth_z l n = Some a.

Lemma list_nth_z_ge0 {A: Type} : forall (l: list A) (n:Z) (a: A),
  list_nth_z l n = Some a ->
  n >= 0.

Local Close Scope Z_scope.

Lemma list_norepet_app: forall A (l1:list A), list_norepet l1 ->
  forall l2, list_norepet l2 ->
    (forall x, In x l1 -> In x l2 -> False) ->
    list_norepet (l1++l2).

Lemma list_norepet_rev: forall A (l:list A), list_norepet l -> list_norepet (rev l).

Section FORALL1.

Variable A: Type.
Variable P: A -> Prop.

Inductive list_forall1: list A -> Prop :=
  | list_forall1_nil: list_forall1 nil
  | list_forall1_cons: forall a al, P a -> list_forall1 al -> list_forall1 (a :: al).


End FORALL1.

Set Implicit Arguments.


Section forall3_ptree.

  Variable A B: Type.
  Variable f: positive -> option A -> option A -> option B -> bool.
  Hypothesis f_none_none: forall p x, f p None None x = true.

  Fixpoint xforall3_l (m : PTree.t A) (m3 : PTree.t B) (i : positive) : bool :=
      match m with
      | PTree.Leaf => true
      | PTree.Node l o r =>
        match m3 with
          | PTree.Leaf =>
            f (PTree.prev i) o None None &&
            (xforall3_l l PTree.Leaf (xO i)) &&
            (xforall3_l r PTree.Leaf (xI i))
          | PTree.Node l3 o3 r3 =>
            f (PTree.prev i) o None o3 &&
            (xforall3_l l l3 (xO i)) &&
            (xforall3_l r r3 (xI i))
        end
      end.

  Lemma xgforall3_l :
    forall i m m3 j,
      xforall3_l m m3 j = true ->
      f (PTree.prev (PTree.prev_append i j)) (PTree.get i m) None (PTree.get i m3) = true.

  Fixpoint xforall3_r (m : PTree.t A) (m3 : PTree.t B) (i : positive) : bool :=
      match m with
      | PTree.Leaf => true
      | PTree.Node l o r =>
        match m3 with
          | PTree.Leaf =>
            (f (PTree.prev i) None o None) &&
            (xforall3_r l PTree.Leaf (xO i)) &&
            (xforall3_r r PTree.Leaf (xI i))
          | PTree.Node l3 o3 r3 =>
            (f (PTree.prev i) None o o3) &&
            (xforall3_r l l3 (xO i)) &&
            (xforall3_r r r3 (xI i))
        end
      end.

  Lemma xgforall3_r :
    forall i m m3 j,
      xforall3_r m m3 j = true ->
      f (PTree.prev (PTree.prev_append i j)) None (PTree.get i m) (PTree.get i m3) = true.

  Fixpoint xforall3_ptree (m1 m2 : PTree.t A) (m3: PTree.t B) (i : positive) {struct m1} : bool :=
    match m1 with
    | PTree.Leaf => xforall3_r m2 m3 i
    | PTree.Node l1 o1 r1 =>
        match m2 with
        | PTree.Leaf => xforall3_l m1 m3 i
        | PTree.Node l2 o2 r2 =>
          match m3 with
            | PTree.Leaf =>
              (xforall3_ptree l1 l2 PTree.Leaf (xO i)) &&
              (f (PTree.prev i) o1 o2 None) &&
              (xforall3_ptree r1 r2 PTree.Leaf (xI i))
            | PTree.Node l3 o3 r3 =>
              (xforall3_ptree l1 l2 l3 (xO i)) &&
              (f (PTree.prev i) o1 o2 o3) &&
              (xforall3_ptree r1 r2 r3 (xI i))
          end
        end
    end.

  Lemma xgforall3_ptree :
    forall i m1 m2 m3 j,
      xforall3_ptree m1 m2 m3 j = true ->
      f (PTree.prev (PTree.prev_append i j)) (PTree.get i m1) (PTree.get i m2) (PTree.get i m3) = true.

  Definition forall3_ptree (m1 m2 : PTree.t A) (m3: PTree.t B) : bool :=
    xforall3_ptree m1 m2 m3 xH.

  Lemma gforall3_ptree :
    forall m1 m2 m3, forall3_ptree m1 m2 m3 = true ->
      forall i, f i (PTree.get i m1) (PTree.get i m2) (PTree.get i m3) = true.

End forall3_ptree.
Arguments forall3_ptree [A B].

  Section COMBINE.
    Import PTree.
    Variable A B C: Type.
    Variable f: option A -> option B -> option C.
    Hypothesis f_none_none: f None None = None.

  Fixpoint xcombine_l (m : t A) {struct m} : t C :=
      match m with
      | Leaf => Leaf
      | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r)
      end.

  Lemma xgcombine_l :
          forall (m: t A) (i : positive),
          get i (xcombine_l m) = f (get i m) None.

  Fixpoint xcombine_r (m : t B) {struct m} : t C :=
      match m with
      | Leaf => Leaf
      | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r)
      end.

  Lemma xgcombine_r :
          forall (m: t B) (i : positive),
          get i (xcombine_r m) = f None (get i m).

  Fixpoint combine (m1:t A) (m2 : t B) {struct m1} : t C :=
    match m1 with
    | Leaf => xcombine_r m2
    | Node l1 o1 r1 =>
        match m2 with
        | Leaf => xcombine_l m1
        | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2)
        end
    end.

  Theorem gcombine:
      forall m1 m2 (i: positive),
      get i (combine m1 m2) = f (get i m1) (get i m2).

  End COMBINE.
Arguments combine [A B C].

Relational operators

Notation "R **" := (@clos_refl_trans _ R) (at level 30).
Lemma Rstar_refl : forall A R (i:A), R** i i.

Lemma Rstar_R : forall A (R:A->A->Prop) (i j:A), R i j -> R** i j.
  
Lemma Rstar_trans : forall A (R:A->A->Prop) (i j k:A),
  R** i j -> R** j k -> R** i k.

Global Hint Resolve Rstar_trans Rstar_refl Rstar_R: core.
 
Lemma star_eq : forall A (R1 R2:A->A->Prop),
  (forall i j, R1 i j -> R2 i j) ->
  forall i j, R1** i j -> R2** i j.