Module FPLemmas

Require Import Footprint InteractionSemantics GAST GMemory
        GlobDefs ETrace GlobSemantics GlobSemantics_Lemmas NPSemantics TypedSemantics .

Require Import DRF USimDRF NPDRF.

Require Import Classical Wf Arith.
Lemma tauN_taustar:
  forall i ge (step:@ProgConfig ge->glabel->FP.t->@ProgConfig ge->Prop) pc fp pc',
    tau_N step i pc fp pc'->tau_star step pc fp pc'.
Lemma GE_mod_wd_tp_inv:
  forall GE pc l fp pc',
    GlobEnv.wd GE ->
    ThreadPool.inv (thread_pool pc) ->
    @glob_step GE pc l fp pc' ->
    ThreadPool.inv (thread_pool pc').
Section Loc_FP_Lemmas.
  Lemma union_sym_eq:
    forall l1 l2,Locs.union l1 l2=Locs.union l2 l1.
  Lemma intersect_sym_eq:
    forall l1 l2,Locs.intersect l1 l2 =Locs.intersect l2 l1.
  Lemma union_assoc_eq:
    forall l1 l2 l3,Locs.union l1 (Locs.union l2 l3)=Locs.union (Locs.union l1 l2) l3.
  Lemma union_intersect_distr_eq:
    forall l1 l2 l3,Locs.union (Locs.intersect l1 l3)(Locs.intersect l2 l3) =
               Locs.intersect(Locs.union l1 l2) l3.
  Lemma union_intersect_dist2:
    forall l1 l2 l3 l4,
      Locs.intersect(Locs.union l1 l2)(Locs.union l3 l4) =
      Locs.union (Locs.union (Locs.intersect l1 l3)(Locs.intersect l1 l4))(Locs.union (Locs.intersect l2 l3) (Locs.intersect l2 l4)).
  Lemma locs_smile_comm:
    forall l1 l2,
      Locs.smile l1 l2 ->
      Locs.smile l2 l1.
  Lemma FPSmile_EffectSmile:
    forall fp1 fp2,
      FP.smile fp1 fp2 ->
      Locs.smile (effects fp1)(effects fp2).
  Lemma smile_subset:
    forall l1 l2 l3,
      Locs.smile l1 l2 ->
      Locs.subset l3 l2 ->
      Locs.smile l1 l3.
  Lemma fpsmile_subset:
    forall fp1 fp2 fp3,
      FP.smile fp1 fp2 ->
      FP.subset fp3 fp2->
      FP.smile fp1 fp3.
  Lemma disj_comm{A:Type}: forall s1 s2,@MemAux.disj A s1 s2->MemAux.disj s2 s1.
  Lemma fpsmile_sym: forall fp1 fp2,FP.smile fp1 fp2->FP.smile fp2 fp1.
  Lemma fpsmile_union_elim:
    forall fp1 fp2 fp3,
      FP.smile fp1 (FP.union fp2 fp3)->
      FP.smile fp1 fp2.
  Lemma fpsmile_union_elim2:
    forall fp1 fp2 fp3,
      FP.smile fp1 (FP.union fp2 fp3)->
      FP.smile fp1 fp3.
  Lemma fpsmile_union_sp:
    forall fp1 fp2 fp3,
      FP.smile fp1 (FP.union fp2 fp3)->
      FP.smile fp1 fp2 /\ FP.smile fp1 fp3.
  Lemma locsmile_union':
    forall l1 l2 l3,
      Locs.smile l1 l2->
      Locs.smile l1 l3->
      Locs.smile l1 (Locs.union l2 l3).
  Lemma fpconflict_dif_trans:
    forall fp1 fp2 fp3,
      FP.conflict fp1 (FP.union fp2 fp3)->
      FP.smile fp1 fp2->
      FP.conflict fp1 fp3.
  
  Lemma fpsmile_union:
    forall fp1 fp2 fp3,
      FP.smile fp1 fp3 ->
      FP.smile fp2 fp3 ->
      FP.smile (FP.union fp1 fp2) fp3.
  
  Lemma fpconflict_union:
    forall fp1 fp2 fp3,
      FP.conflict fp1 (FP.union fp2 fp3)->
      FP.conflict fp1 fp2 \/ FP.conflict fp1 fp3.
  Lemma star_cons_step{GE}:
    forall step l fp l2 fp2 (pc pc1 pc2:@ProgConfig GE),
      star step pc l fp pc1 ->
      step pc1 l2 fp2 pc2 ->
      exists l',star step pc l' (FP.union fp fp2) pc2.
  Lemma fpconflict_tauN_rule1{GE}:
    forall i pc1 pc fp1 fp2,
      FP.conflict fp1 fp2->
      tau_N (@glob_step GE) i pc fp2 pc1 ->
      exists j k pc' pc'' fp0' fp1' fp2',
        tau_N glob_step j pc fp0' pc' /\
        glob_step pc' tau fp1' pc'' /\
        tau_N glob_step k pc'' fp2' pc1 /\
        FP.union fp0' (FP.union fp1' fp2') = fp2 /\
        FP.conflict fp1 fp1' /\
        j + k + 1 = i.
  Lemma fpconflict_taustar_rule1{GE}:
    forall pc1 pc fp1 fp2,
      FP.conflict fp1 fp2->
      tau_star (@glob_step GE) pc fp2 pc1 ->
      exists pc' pc'' fp0' fp1' fp2',
        tau_star glob_step pc fp0' pc' /\
        glob_step pc' tau fp1' pc'' /\
        tau_star glob_step pc'' fp2' pc1 /\
        FP.union fp0' (FP.union fp1' fp2') = fp2 /\
        FP.conflict fp1 fp1'.

  Lemma fpfrees_union_alloc:
    forall fp1 fp2,
      FP.frees (FP.union fp1 fp2) = Locs.union (FP.frees fp1)(FP.frees fp2).
  Lemma fpreads_union_alloc:
    forall fp1 fp2,
      FP.reads (FP.union fp1 fp2) = Locs.union (FP.reads fp1)(FP.reads fp2).
  Lemma fpwrites_union_alloc:
    forall fp1 fp2,
      FP.writes (FP.union fp1 fp2) = Locs.union (FP.writes fp1)(FP.writes fp2).
  Lemma fpcmps_union_alloc:
    forall fp1 fp2,
      FP.cmps (FP.union fp1 fp2) = Locs.union (FP.cmps fp1)(FP.cmps fp2).

  Lemma fpsubset_trans:
    forall l1 l2 l3,
      FP.subset l1 l2 ->
      FP.subset l2 l3 ->
      FP.subset l1 l3.
  Lemma conflict_min_rule{ge}:
    forall pc1 fp1 pc1' pc2 fp2 pc2',
      tau_star (@np_step ge) pc1 fp1 pc1' -> atom_bit pc1 = atom_bit pc1' ->
      tau_star (@np_step ge) pc2 fp2 pc2' ->
      FP.conflict fp1 fp2 ->
      exists pc10 pc11 fp10 fp11,
        tau_star np_step pc1 fp10 pc10 /\ atom_bit pc1 = atom_bit pc10 /\
        np_step pc10 tau fp11 pc11 /\ atom_bit pc10 = atom_bit pc11 /\
        FP.smile fp10 fp2 /\
        FP.conflict fp11 fp2 /\
        FP.subset fp10 fp1 /\ FP.subset fp11 fp1.

  Lemma conflict_min_rule_extended{ge}:
    forall pc1 fp1 pc1' pc2 fp2 pc2',
      tau_star (@np_step ge) pc1 fp1 pc1' -> atom_bit pc1 = atom_bit pc1' ->
      tau_star (@np_step ge) pc2 fp2 pc2' -> atom_bit pc2 = atom_bit pc2' ->
      FP.conflict fp1 fp2 ->
      exists pc10 pc11 fp10 fp11,
        tau_star np_step pc1 fp10 pc10 /\ atom_bit pc1 = atom_bit pc10 /\
        np_step pc10 tau fp11 pc11 /\ atom_bit pc10 = atom_bit pc11 /\
        exists pc20 pc21 fp20 fp21,
          tau_star np_step pc2 fp20 pc20 /\ atom_bit pc2 = atom_bit pc20 /\
          np_step pc20 tau fp21 pc21 /\ atom_bit pc20 = atom_bit pc21 /\
          FP.smile fp10 fp20 /\ FP.smile fp10 fp21 /\ FP.smile fp11 fp20 /\
          FP.conflict fp11 fp21 /\
          FP.subset fp10 fp1 /\ FP.subset fp11 fp1 /\ FP.subset fp20 fp2 /\ FP.subset fp21 fp2.

End Loc_FP_Lemmas.

Lemma MemEffect_MemPost_fpsmile_memeq:
  forall m0 m1 m1' m2' m2 fp1 fp2,
    MemEffect m0 m1 fp1 ->
    MemEffect m1 m2 fp2->
    FP.smile fp1 fp2 ->
    MemEffect m0 m1' fp2 ->
    MemPost m2 m1' fp2 ->
    MemEffect m1' m2' fp1 ->
    MemPost m1 m2' fp1 ->
    GMem.eq' m2' m2.
Lemma LEffect_LPost_fpsmile_memeq:
  forall m0 m1 m1' m2' m2 f1 f2 fp1 fp2,
    LEffect m0 m1 fp1 f1 ->
    LEffect m1 m2 fp2 f2->
    FP.smile fp1 fp2 ->
    LEffect m0 m1' fp2 f2 ->
    LPost m2 m1' fp2 f2 ->
    LEffect m1' m2' fp1 f1 ->
    LPost m1 m2' fp1 f1 ->
    GMem.eq' m2' m2.