Library mathlib_join

Require Export include.
Require Export memory.
Require Export memdata.
Require Export assertion.
Require Export absop.
Require Export simulation.
Require Export language.
Require Export opsem.
Require Export os_program.
Require Export os_spec.
Require Export inferules.
Require Export os_code_notations.
Require Export os_code_defs.
Require Export os_ucos_h.
Require Export os_time.
Require Export baseTac.
Require Export auxdef.
Require Export seplog_lemmas.
Require Export seplog_tactics.
Require Export derivedrules.
Require Export hoare_conseq.
Require Export symbolic_execution.
Require Export hoare_assign.
Require Export hoare_lemmas.
Require Export BaseAsrtDef.
Require Export inv_prop.
Require Export InternalFunSpec.
Require Export IntLib.
Require Export List.
Require Export can_change_aop_proof.
Require Export cancel_absdata.
Require Export hoare_tactics.
Require Export type_val_match.
Require Export init_spec.
Require Export sep_pure.
Require Export absop_rules.
Require Import Coq.Logic.FunctionalExtensionality.
Set Implicit Arguments.

Close Scope nat_scope.
Open Scope Z_scope.
Open Scope code_scope.

Lemma join_prop1_my:
  forall ma mb mab x1 v1 v2 mc´ mc md,
    TcbMod.join ma mb mab ->
    TcbJoin x1 v1 mc´ mc ->
    TcbMod.join md mc ma ->
    TcbMod.join (TcbMod.set ma x1 v2) mb
                (TcbMod.set mab x1 v2).

Lemma join_prop1:
  forall v´44 v´43 v´7 v´58 prio st msg v´59 v´49 v´47 x00,
    TcbMod.join v´44 v´43 v´7 ->
    TcbJoin (v´58 , Int.zero ) (prio , st , msg ) v´59 v´49 ->
    TcbMod.join v´47 v´49 v´44 ->
    TcbMod.join
      (TcbMod.set v´44 (v´58 , Int.zero )
                  (prio , rdy , Vptr x00 )) v´43
      (TcbMod.set v´7 (v´58 , Int.zero )
                  (prio , rdy , Vptr x00 )).

Lemma join_prop2_my:
  forall m1 m2 m12 b1 prio st msg m3 ma3 m4 p1,
    TcbMod.join m1 m2 m12 ->
    TcbJoin (b1 , Int.zero ) (prio , st , msg ) m3 ma3 ->
    TcbMod.join m4 ma3 m2 ->
    TcbMod.join m1
                (TcbMod.set m2 (b1 , Int.zero ) (prio , rdy , Vptr p1 ))
                (TcbMod.set m12 (b1 , Int.zero ) (prio , rdy , Vptr p1 )).

Lemma join_prop2: forall v´44 v´43 v´7 v´57 prio st msg v´58 v´48 v´46 x00,
                    TcbMod.join v´44 v´43 v´7 ->
                    TcbJoin (v´57 , Int.zero ) (prio , st , msg ) v´58 v´48 ->
                    TcbMod.join v´46 v´48 v´43->
                    TcbMod.join v´44
                                (TcbMod.set v´43 (v´57 , Int.zero )
                                            (prio , rdy , Vptr x00 ))
                                (TcbMod.set v´7 (v´57 , Int.zero )
                                            (prio , rdy , Vptr x00 )).

Lemma joinsig_join_ex_my:
  forall x1 v1 ma mb mab m,
    EcbMod.joinsig x1 v1 mab m ->
    EcbMod.join ma mb mab ->
    exists mm, EcbMod.joinsig x1 v1 ma mm /\ EcbMod.join mm mb m.

Lemma joinsig_join_ex:
  forall x0 x x1 t x4 x5,
    EcbMod.joinsig x0 x x1 t ->
    EcbMod.join x4 x5 x1 ->
    exists y, EcbMod.joinsig x0 x x4 y /\ EcbMod.join y x5 t.

Lemma ecbmod_join_sigg_my:
  forall m1 m2 m3 x1 v1,
    EcbMod.join m1 m2 m3 ->
    EcbMod.joinsig x1 v1 EcbMod.emp m2 ->
    EcbMod.joinsig x1 v1 m1 m3.

Lemma ecbmod_join_sigg:
  forall x0 x2 x1 x3 x,
    EcbMod.join x0 x x2 ->
    EcbMod.joinsig x1 x3 EcbMod.emp x ->
    EcbMod.joinsig x1 x3 x0 x2.

Use '+' indicate the operation EcbMod.join Then, this lemma means: (x1,v1) + m1 = m2 -> mm1 + m2 = mm2 -> exists me = mm1 + m1, (x1,v1) + me = mm2

The proof is obvious: (x1,v1) + me = (x1,v1) + mm1 + m1 = (x1,v1) + m1 + mm1 = m2 + mm1 = mm1 + m2 = mm2

Lemma joinsig_join_sig2_my:
  forall x1 v1 m1 m2 mm1 mm2,
    EcbMod.joinsig x1 v1 m1 m2 ->
    EcbMod.join mm1 m2 mm2 ->
    exists me, EcbMod.joinsig x1 v1 me mm2 /\ EcbMod.join mm1 m1 me.

Lemma joinsig_join_sig2:
  forall x1 x3 x4 x x0 x2,
    EcbMod.joinsig x1 x3 x4 x ->
    EcbMod.join x0 x x2 ->
    exists x5, EcbMod.joinsig x1 x3 x5 x2 /\ EcbMod.join x0 x4 x5.

Lemma tcbjoin_set_my:
  forall x1 v1 v2 m´ m,
    TcbJoin x1 v1 m´ m ->
    TcbJoin x1 v2 m´ (TcbMod.set m x1 v2).

Lemma tcbjoin_set:
  forall x y x2 x1 tcbls,
    TcbJoin x x2 x1 tcbls ->
    TcbJoin x y x1 (TcbMod.set tcbls x y).

Lemma tcbjoin_get_my:
  forall x1 v1 m´ m v2,
    TcbJoin x1 v1 m´ m ->
    TcbMod.get m x1 = Some v2 -> v1 = v2.

Lemma tcbjoin_get:
  forall x a x1 tcbls a´,
    TcbJoin x a x1 tcbls ->
    TcbMod.get tcbls x = Some a´ -> a = a´.

Lemma tcbjoin_get_get_my:
  forall x1 v1 m´ m x2 v2,
    TcbJoin x1 v1 m´ m ->
    TcbMod.get m´ x2 = Some v2 ->
    TcbMod.get m x2 = Some v2.

Lemma tcbjoin_get_get:
  forall x x2 x1 tcbls v tid ,
    TcbJoin x x2 x1 tcbls ->
    TcbMod.get x1 tid = Some v->
    TcbMod.get tcbls tid = Some v.

Lemma tcbjoin_get_a_my:
  forall x v m´ m,
    TcbJoin x v m´ m ->
    TcbMod.get m x = Some v.

Lemma tcbjoin_get_a :
  forall x a x1 tcbls,
    TcbJoin x a x1 tcbls ->
    TcbMod.get tcbls x = Some a.

Lemma not_eq_comm:
  forall T (x y:T),
    x <> y -> y <> x.

Lemma tcbjoin_get_getneq_my:
  forall x1 v1 x2 v2 m´ m,
    TcbJoin x1 v1 m´ m ->
    TcbMod.get m´ x2 = Some v2 ->
    TcbMod.get m x2 = Some v2 /\ x2 <> x1.

Lemma tcbjoin_get_getneq:
  forall x a x1 tcbls tid b,
    TcbJoin x a x1 tcbls ->
    TcbMod.get x1 tid = Some b ->
    TcbMod.get tcbls tid = Some b /\ tid <> x.

Lemma tcbjoin_join_get_neq_my:
  forall x1 v1 x2 v2 ma mb´ mb mab,
    TcbJoin x1 v1 mb´ mb ->
    TcbMod.join ma mb mab ->
    TcbMod.get ma x2 = Some v2 ->
    x2 <> x1 /\ TcbMod.get mab x2 = Some v2.

Lemma tcbjoin_join_get_neq:
  forall ptcb a x1 tid tcs tcbls tcs´ b,
    TcbJoin ptcb a x1 tcs ->
    TcbMod.join tcbls tcs tcs´ ->
    TcbMod.get tcbls tid = Some b ->
    tid <> ptcb /\ TcbMod.get tcs´ tid = Some b.

Lemma tcbjoin_join_ex2_main:
  forall x v ma´ ma mb mab,
    TcbJoin x v ma´ ma ->
    TcbMod.join ma mb mab ->
    exists mab´, TcbMod.join ma´ mb mab´ /\ TcbJoin x v mab´ mab.

Lemma tcbjoin_join_ex2 :
  forall x x4 x3 a0 b c,
    TcbJoin x x4 x3 a0 ->
    TcbMod.join a0 b c ->
    exists z, TcbMod.join x3 b z /\ TcbJoin x x4 z c.

Lemma tcbjoin_set_ex_main:
  forall x v ma´ ma mb mab v´,
    TcbJoin x v ma´ ma ->
    TcbMod.join mb ma mab ->
    exists ma´´,
      TcbJoin x v´ ma´ ma´´ /\
      TcbMod.join mb ma´´ (TcbMod.set mab x v´).

Lemma tcbjoin_set_ex :
  forall ptr st st´ x y z a ,
    TcbJoin ptr st x y ->
    TcbMod.join z y a ->
    exists b,
      TcbJoin ptr st´ x b /\
      TcbMod.join z b (TcbMod.set a ptr st´).