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 Ascii.
Require String.
Require Import Relation_Operators.
Require Psatz.
Require Import Permutation.

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 Zsucc 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'.
Hint Resolve option_map_some.

Properties about PTree

Lemma add_set_or : forall i j s,
  (PTree.set i tt s) ! j = Some tt -> i=j \/ s ! j = Some tt.

Lemma xmap_assoc:
  forall (A B C: Type) (f1: positive -> A -> B) (f2: positive -> B -> C) (m: PTree.t A) (i : positive),
    PTree.xmap f2 (PTree.xmap f1 m i) i =
    PTree.xmap (fun i x => f2 i (f1 i x)) m i.

Lemma map_assoc:
  forall (A B C: Type) (f1: positive -> A -> B) (f2: positive -> B -> C) (m: PTree.t A),
    PTree.map f2 (PTree.map f1 m) =
    PTree.map (fun i x => f2 i (f1 i x)) m.

Lemma xmap_ext:
  forall (A B: Type) (f1 f2: positive -> A -> B) (m: PTree.t A) (i : positive),
    (forall i x, f1 i x = f2 i x) ->
    PTree.xmap f1 m i = PTree.xmap f2 m i.

Lemma map_ext:
  forall (A B: Type) (f1 f2: positive -> A -> B) (m: PTree.t A),
    (forall i x, f1 i x = f2 i x) ->
    PTree.map f1 m = PTree.map f2 m.

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_xfold_same : forall (A B:Type) (f:A->positive->B->A) (m1 m2:PTree.t B) (x y:A) p',
  (forall p, m1!p = m2!p) ->
  x = y ->
  PTree.xfold f p' m1 x = PTree.xfold f p' m2 y.

Lemma PTree_fold_same : forall (A B:Type) (f:A->positive->B->A) (m1 m2:PTree.t B) (x:A),
  (forall p, m1!p = m2!p) ->
  PTree.fold f m1 x = PTree.fold f m2 x.

Properties of Regmap

Lemma val_eqdec: forall (v1 v2:val), {v1 = v2}+{v1 <> v2}.
  
Definition regset := Regmap.t val.

Lemma gsregset: forall (j: reg) (v:val) (m: regset) ,
  (m#j) = v -> (forall r, (m#j <- v)#r = m#r).


Lemma ptree_set_permut: forall r r0 r1 (v0 v1:val) t ,
  r0 <> r1 ->
  (PTree.set r0 v0 (PTree.set r1 v1 t)) ! r =
  (PTree.set r1 v1 (PTree.set r0 v0 t)) ! r.

Lemma ptree_setset: forall r dst (v1 v2:val) t,
(PTree.set r v2 (PTree.set r v1 t)) ! dst =
(PTree.set r v2 t) ! dst.
  
Lemma regset_permut: forall rs r (v:val) r1 r0,
  r <> r0 -> r <> r1 ->
  forall dst, (rs # r <- v) # r0 <- (rs # r1) # dst =
              (rs # r0 <- (rs # r1)) # r <- v # dst.

Lemma regset_setset: forall rs r (v1 v2:val),
  forall dst, (rs # r <- v1) # r <- v2 # dst =
              (rs # r <- v2) # dst.

Definition forall_ptree {A:Type} (f:positive->A->bool) (m:PTree.t A) : bool :=
  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: PTree.t A),
  PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true = true ->
  forall i x, m!i = Some x -> f i x = true.

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

PTrees over pairs of positive

Lemmas about lists

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).

Hint Resolve in_tl_in_cons.
Hint Resolve in_hd_in_cons.

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

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

Lemma nth_error_app_length {A :Type} : forall l l' (a:A),
  nth_error (l++a::l') (length l) = Some a.

Lemma nth_error_app_length2 : forall (A: Type) (l1 l2: list A),
  nth_error (l1 ++ l2) (S (length l1)) =
  nth_error (l2) 1.

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 in_nth_error_app : forall (A: Type) (l l': list A) (a: A) k,
  In a l' ->
  nth_error (l++l') k = Some a ->
  (k >= length l)%nat ->
  (exists k', (k' <= k)%nat /\ nth_error l' k' = Some a).

Lemma nth_error_app_gt_in : forall (A: Type) (l l': list A) (a: A) k,
  nth_error (l ++ l') k = Some a ->
  (k > (length l))%nat ->
  In a l'.

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

Lemma nth_error_some_length {A: Type} : forall (l: list A) a k,
  nth_error l k = Some a ->
  (k < List.length l)%nat.

Lemma nth_error_some {A:Type}: forall l k (v:A),
  nth_error l k = Some v ->
  forall dft, nth k l dft = v.

Lemma nth_error_length : forall (A:Type) (l:list A) x,
  (x < length l)%nat -> exists y, nth_error l x = Some y.

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

Lemma map_cons_inv {A B:Type} : forall (f:A->B) (l:list A) (l':list B) (b:B),
  map f l = b :: l' ->
  exists a, exists m, b = (f a) /\ l = a::m /\ l' = map f m.

Lemma map_in {A B:Type}: forall (f:A->B) (l:list A) (a:A),
  In a l -> In (f a) (map f l).

Lemma map_length {A B : Type} : forall (f : A -> B) (l: list A),
  List.length l = List.length (map f 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 (Psucc p2).

Lemmas about bool

Lemma negb_false : forall b, negb b = false -> b = true.

Lemma negb_true : forall b, negb b = true -> b = false.

Ltac negInv :=
  match goal with
    | [H : negb _ = true |- _ ] => apply negb_true in H ; negInv
    | [H : negb _ = false |- _ ] => apply negb_false in H ; negInv
    | _ => idtac
  end.

The nth_okp predicate

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 (Datatypes.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_nth {A:Type} : forall (l: list A) k e v,
  nth_okp k l ->
  nth k l v = e ->
  nth_error l k = Some e.

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 length_nth_ok {A: Type} : forall (l: list A) k,
  (k < List.length l)%nat -> nth_okp k l.

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).

Lemma alln_is_alln {A:Type}: forall (v' n v:A) l k,
  alln n l ->
  nth_error l k = Some v ->
  nth k l v' = n.

Lemma alln_is_alln2 {A:Type}: forall (n:A) l,
  alln n l ->
  forall k, (exists r, nth_error l k = Some r) -> nth_error l k = Some n.

Lemma alln_spec {A:Type}: forall (n:A) l,
  (forall k a, nth_error l k = Some a -> a = n) -> alln n l.

Additional definitions and properties of lists

Definition z_to_nat (n: Z) : nat :=
  match n with
    | Z0 => O
    | Zpos p => nat_of_P p
    | _ => O
  end.

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 (Zpred n)) .

Lemma arith_utils2: forall (n:Z) (n1: nat) ,
  n > 0 ->
  n1 = (z_to_nat (Zpred 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.

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).

Lemma Permutation_NoDup: forall (A:Type),
  forall (l l': list A), Permutation l l' -> NoDup l -> NoDup 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).

Lemma list_forall1_app: forall a2 a1,
  list_forall1 a1 -> list_forall1 a2 ->
  list_forall1 (a1 ++ a2).

End FORALL1.

Set Implicit Arguments.

Lemma list_forall1_imply:
  forall (A : Type) (P1: A -> Prop) (l: list A),
  list_forall1 A P1 l ->
  forall (P2: A -> Prop),
  (forall v, In v l -> P1 v -> P2 v) ->
  list_forall1 A P2 l.

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 i o None None &&
            (xforall3_l l PTree.Leaf (PTree.append i (xO xH))) &&
            (xforall3_l r PTree.Leaf (PTree.append i (xI xH)))
          | PTree.Node l3 o3 r3 =>
            f i o None o3 &&
            (xforall3_l l l3 (PTree.append i (xO xH))) &&
            (xforall3_l r r3 (PTree.append i (xI xH)))
        end
      end.

  Lemma xgforall3_l :
    forall i m m3 j,
      xforall3_l m m3 j = true ->
      f (PTree.append j i) (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 i None o None) &&
            (xforall3_r l PTree.Leaf (PTree.append i (xO xH))) &&
            (xforall3_r r PTree.Leaf (PTree.append i (xI xH)))
          | PTree.Node l3 o3 r3 =>
            (f i None o o3) &&
            (xforall3_r l l3 (PTree.append i (xO xH))) &&
            (xforall3_r r r3 (PTree.append i (xI xH)))
        end
      end.

  Lemma xgforall3_r :
    forall i m m3 j,
      xforall3_r m m3 j = true ->
      f (PTree.append j i) 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 (PTree.append i (xO xH))) &&
              (f i o1 o2 None) &&
              (xforall3_ptree r1 r2 PTree.Leaf (PTree.append i (xI xH)))
            | PTree.Node l3 o3 r3 =>
              (xforall3_ptree l1 l2 l3 (PTree.append i (xO xH))) &&
              (f i o1 o2 o3) &&
              (xforall3_ptree r1 r2 r3 (PTree.append i (xI xH)))
          end
        end
    end.

  Lemma xgforall3_ptree :
    forall i m1 m2 m3 j,
      xforall3_ptree m1 m2 m3 j = true ->
      f (PTree.append j i) (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.
Implicit 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.
Implicit 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.

Hint Resolve Rstar_trans Rstar_refl Rstar_R.
 
Lemma Rstar_left_case : forall A R (i j:A), R** i j ->
  i = j \/ exists k, R i k /\ R** k j.

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.




  Lemma repr_mod_prop: forall x y,
    Int.repr (x + y * Int.modulus) = Int.repr x.

  Lemma Z_of_nat_gt: forall n, (n > 0)%nat -> Z_of_nat n > 0.

  Lemma sign_ext_same : forall n m i,
    (m > 0)%nat ->
    Int.wordsize = ((S n)+m)%nat ->
    -(two_power_nat n) <= Int.signed i <= (two_power_nat n) -1 ->
    Int.sign_ext (Z_of_nat (S n)) i = i.

  Lemma two_power_nat_div2 : forall n,
    two_power_nat (S n) / 2 = two_power_nat n.

  Lemma neg_signed_unsigned : forall x,
    Int.repr (- (Int.signed x)) = Int.repr (- (Int.unsigned x)).

  Lemma zle_and_case: forall x y z t,
    zle x y && zle z t = false -> x > y \/ z > t.

  Lemma add_signed_unsigned : forall x y,
    Int.repr (Int.signed x + Int.signed y) = Int.repr (Int.unsigned x + Int.unsigned y).

  Lemma sub_signed_unsigned : forall x y,
    Int.repr (Int.signed x - Int.signed y) = Int.repr (Int.unsigned x - Int.unsigned y).

  Require Export z_extra_props.

  Lemma mult_signed_unsigned : forall x y,
    Int.repr (Int.signed x * Int.signed y) = Int.repr (Int.unsigned x * Int.unsigned y).

  Lemma zle_true_iff : forall x y: Z,
    proj_sumbool (zle x y) = true <-> x <= y.