Library aux_for_hoare_lemmas

Require Import Coq.Bool.IfProp.
Require Import Coq.Logic.Classical_Prop.
Open Scope nat_scope.
Require Import Recdef.
Require Import Coq.Init.Wf.
Require Import Coq.Arith.Wf_nat.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import inferules.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import memdata.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import hoare_conseq.
Require Import Integers.
Require Import baseTac.
Require Import LibTactics.
Require Import val.
Require Import derivedrules.
Require Import BaseAsrtDef.
Require Import simulation.
Require Import os_code_notations.
Require Export include.
Set Implicit Arguments.
Open Scope Z_scope.
Open Scope code_scope.
  Fixpoint type_eq (t1 t2:type):=
         match t1,t2 with
           | Void, Void => true
           | Tnull, Tnull => true
           | Int8u, Tint8 =>true
           | Int16u, Int16u => true
           | Int32u, Int32u =>true
           | Tptr t1´, Tptr t2´ => type_eq t1´ t2´
           | Tstruct id dl,Tstruct id´ dl´ => andb ( Zeq_bool id id´) (dl_eq dl dl´)
           | Tarray t n,Tarray t´ n´ =>andb( type_eq t t´) (beq_nat n n´)
           | _,_=>false
         end
  with dl_eq (d1 d2:decllist):=
    match d1 with
      | dnil => match d2 with
                  |dnil =>true
                  |_ => false
                end
      | dcons a b d1´=> match d2 with
                            | dnil =>false
                            | dcons a´ b´ d2´ =>
                              andb (andb ( Zeq_bool a a´) (type_eq b b´)) (dl_eq d1´ d2´)
                          end
    end.

  Fixpoint assign_type_match_fun (t1 t2:type) :=
    match t1,t2 with
      | ( t ∗), Tnull => true
      | Tnull, Tnull => true
      | Void, Void => true
      | (t ∗), (t´ ∗) => true
      | Tarray t n, Tarray t´ n´ => andb (type_eq t t´) (beq_nat n n´)
      | (t ∗) , Tarray t´ n => type_eq t t´
      | Tstruct id dl, Tstruct id´ dl´=> andb (dl_eq dl dl´) (Zeq_bool id id´)
      | Tint8 , Tint8 => true
      | Tint8, Int16u => true
      | Tint8, Int32u => true
      | Int16u, Tint8 => true
      | Int16u , Int16u => true
      | Int16u, Int32u => true
      | Int32u , Tint8 =>true
      | Int32u, Int16u =>true
      | Int32u, Int32u => true
      | Tcom_ptr _ , Tnull => true
      | (t ∗), (Tcom_ptr t´) => true
      | (Tcom_ptr t), (Tcom_ptr t´) => true
      | (Tcom_ptr t), (t´ ∗ ) => true
      | _, _ => false
    end.

  Lemma assign_type_match_true: forall t1 t2, assign_type_match_fun t1 t2 = true -> assign_type_match t1 t2.
Scheme type_ind2 := Induction for type Sort Prop with decllist_ind2 := Induction for decllist Sort Prop.
Lemma type_eq_true_eq : forall t1 t2, type_eq t1 t2 = true -> t1 = t2.

Lemma dl_eq_true_eq : forall d1 d2, dl_eq d1 d2 = true -> d1 = d2.

Qed.
Close Scope Z_scope.

Require Export tst_prop.
Require Import ZArith.

Lemma nth_id_some_in_decllist_true : forall n dls id, nth_id n dls = Some id -> in_decllist id dls = true.

Lemma in_decllist_field_offsetfld_some : forall dls id, in_decllist id dls = true -> forall n, exists off, field_offsetfld id dls n = Some off.
Lemma field_offsetfld_pos_mono : forall dls id pos1 off1,
  field_offsetfld id dls pos1 = Some off1
  -> forall pos2 off2, field_offsetfld id dls pos2 = Some off2
  -> forall n, Int.add n pos1 = pos2
  -> Int.add n off1 = off2.

Lemma nth_id_field_offsetfld_some : forall decl n id, nth_id n decl = Some id -> forall pos, exists off, field_offsetfld id decl pos = Some off.

Lemma id_nth_ge:forall decl n id m, id_nth´ id decl n = Some m -> m>=n.

Lemma id_nth´_suc: forall id decl n m, id_nth´ id decl (S n) = Some (S m) ->
                                       id_nth´ id decl n = Some m .

Lemma id_nth_eq:
  forall n id decl,
    good_decllist decl = true -> id_nth id decl = Some n -> nth_id n decl = Some id.

Lemma up_val_op_ex: forall vl v n vl´ , update_nth_val_op n vl v = Some vl´ -> update_nth_val n vl v = vl´ /\ (exists vi, nth_val n vl = Some vi).

 Lemma eval_type_addr_eq : forall e ge le m t, evaltype (eaddrof e) (ge, le, m) = Some (Tptr t) -> evaltype e (ge, le, m) = Some t.
Lemma eval_addr_eq: forall e ge le m b i, evalval (eaddrof e) (ge, le, m) = Some (Vptr (b, i)) -> evaladdr e (ge,le,m) = Some (Vptr (b,i)).

Lemma gooddecl_gettype:
  forall i t dls n t´ id,
    good_decllist (dcons i t dls)=true -> nth_id n dls = Some id -> ftype id (dcons i t dls) = Some t´ -> ftype id dls = Some t´.
  Lemma nth_id_Some_imply_in_decllist :
    forall n id dls,
      nth_id n dls = Some id ->
        in_decllist id dls = true.
Qed.

Lemma gooddecl_off_add:
  forall i t dls n id off,
    good_decllist (dcons i t dls)=true -> nth_id n dls = Some id ->
    field_offset id (dcons i t dls) = Some off ->
    exists off´, field_offset id dls = Some off´ /\ Int.add (Int.repr (BinInt.Z_of_nat (typelen t))) off´= off.

Lemma gooddecl_neq:
  forall i t dls n id,
    good_decllist (dcons i t dls)=true -> nth_id n dls = Some id ->
    Zbool.Zeq_bool id i = false.

Lemma loadbytes_local: forall m1 m2 m bls b i t, MemMod.join m1 m2 m -> loadbytes m1 (b,i) (typelen t) = Some bls -> loadbytes m (b,i) (typelen t) = Some bls.

Lemma nth_id_exists_off: forall decl n id, nth_id n decl = Some id -> exists off, field_offset id decl = Some off.

Require Import lmachLib.
Lemma load_local:
  forall m t l v m1 m2, MemMod.join m1 m2 m ->
                        load t m1 l = Some v ->
                        load t m l = Some v.

Lemma insert_star:forall s p r q l, p <==> q ** r -> (s |= l ** p <-> s |= q ** l **r).

Lemma asrt_eq_trans: forall p q r, p <==> q -> q <==> r -> p <==> r.

Lemma star_star_eq_rep:
  forall p q r q´ A, (A <==> p ** q ** r) -> (q <==> q´) -> (A <==> p ** q´ ** r).

Lemma star_star_comm: forall p q r, p ** q ** r <==> q ** p ** r.

Lemma field_asrt_impl:
    forall p id x tid decl b i off tp,
      ftype id decl = Some tp ->
      field_offset id decl = Some off ->
      ((LV x @ Tptr (Tstruct tid decl) |-> Vptr (b, i)) ** p) ==> (Lv (efield (ederef (evar x)) id) @ tp == (b,Int.add i off)).

  Lemma field_asrt_impl_g:
    forall p id x tid decl b i off tp,
      ftype id decl = Some tp ->
      field_offset id decl = Some off ->
      ((A_notin_lenv x ** GV x @ Tptr (Tstruct tid decl) |-> Vptr (b, i)) ** p) ==> (Lv (efield (ederef (evar x)) id) @ tp == (b,Int.add i off)).

  Lemma eq_impl_trans: forall p q r, p <==> q -> q ==> r -> p ==> r.
  Lemma star3_comm: forall p q r l, p ** (q ** l) ** r <==> q ** p ** l ** r.
   Lemma star3_comm´:forall s p q r l, s |= p ** q ** r ** l -> s |= (p ** r) ** q ** l.

Lemma update_nth: forall vl n v vi, nth_val n vl = Some vi -> nth_val n (update_nth_val n vl v) = Some v.

 Lemma array_rm_update_eq: forall s b i vl v vi n m t, m < n -> nth_val m vl = Some vi -> s |= Aarray_rm (b,i) n t vl m -> s |= Aarray_rm (b,i) n t (update_nth_val m vl v) m.

Lemma unsigned_zero: forall i , Int.unsigned i = Int.unsigned Int.zero -> i = Int.zero.

Lemma ge_zero_eq: forall m, negb (Int.lt m Int.zero) = true -> Int.repr (BinInt.Z.of_nat (BinInt.Z.abs_nat (Int.unsigned m))) = m.


Lemma int_Z_lt:
    forall m n, negb (Int.lt m Int.zero) = true ->
                Int.lt m (Int.repr (BinInt.Z.of_nat n)) = true ->
                BinInt.Z.abs_nat (Int.unsigned m) < n.

 Lemma arrayelem_asrt_impl:
    forall n m p p´ b i t e2 x,
      t = Tint8 \/ t = Tint16 \/ t = Tint32 ->
      p <==>
      Alvarenv x (Tarray t n) (addrval_to_addr (b, i)) ** p´ ->
      p ==> Rv e2 @ t == Vint32 (Int.repr (BinInt.Z.of_nat m)) ->
      p ==>
         (Lv (earrayelem (evar x) e2) @ t == (b,Int.add i (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) (Int.repr (BinInt.Z.of_nat m))))).

Lemma arrayelem_asrt_impl_g:
    forall n m p p´ b i t e2 x,
      t = Tint8 \/ t = Tint16 \/ t = Tint32 ->
      p <==>
      (A_notin_lenv x ** Agvarenv x (Tarray t n) (addrval_to_addr (b, i))) ** p´ ->
      p ==> Rv e2 @ t == Vint32 (Int.repr (BinInt.Z.of_nat m)) ->
      p ==>
         (Lv (earrayelem (evar x) e2) @ t == (b,Int.add i (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) (Int.repr (BinInt.Z.of_nat m))))).

Lemma int_count_eq: forall i t m, Int.add (Int.add i (Int.repr (BinInt.Z.of_nat (typelen t))))
               (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t)))
                  (Int.repr (BinInt.Z.of_nat m))) = Int.add i
           (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t)))
              (Int.repr (BinInt.Z.of_nat (S m)))).


Lemma array_asrt_imp_length :
  forall s l t n vl P,
    s|= Aarray l (Tarray t n) vl ** P ->
       length vl = n.
  Require Import tacticsforseplog.

Close Scope code_scope.