Library cancel_absdata

Require Import include.
Require Import memory.
Require Import memdata.
Require Import assertion.
Require Import simulation.
Require Import language.
Require Import opsem.
Require Import os_program.
Require Import os_spec.
Require Import inferules.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import baseTac.
Require Import auxdef.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import derivedrules.
Require Import hoare_conseq.
Require Import symbolic_execution.
Require Import hoare_assign.
Require Import hoare_lemmas.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Require Import seplog_tactics.
Require Import sep_pure.
Require Import tst_prop.
Require Import ruleLib.
Require Import asrtLib.

Set Implicit Arguments.


Lemma abst_get_set_disj: forall O id Of x y,
  OSAbstMod.get O id = Some x -> OSAbstMod.disj O Of -> OSAbstMod.disj (OSAbstMod.set O id y) Of.

Lemma eqdomO_same:forall O,eqdomO O O.
Lemma get_set_idneq:forall O Of id id´ x y, OSAbstMod.disj O Of -> OSAbstMod.get O id = Some x ->
                                            id <> id´ ->
                                            OSAbstMod.get (OSAbstMod.merge (OSAbstMod.set O id´ y) Of) id = Some x.

Lemma get_set_ideq:forall O Of id y,
                                            OSAbstMod.get (OSAbstMod.merge (OSAbstMod.set O id y) Of) id = Some y.

Lemma abst_disj_merge_set_eq: forall x y id O Of, OSAbstMod.disj O Of -> OSAbstMod.get O id = Some x -> OSAbstMod.merge (OSAbstMod.set O id y) Of = OSAbstMod.set (OSAbstMod.merge O Of) id y.

Lemma abst_disj_merge_set_eq´: forall x y y´ x´ id id´ O Of, OSAbstMod.disj O Of -> OSAbstMod.get O id = Some x -> OSAbstMod.get O id´ = Some x´ -> OSAbstMod.merge (OSAbstMod.set (OSAbstMod.set O id y) id´ y´) Of =OSAbstMod.set ( OSAbstMod.set (OSAbstMod.merge O Of) id y) id´ y´.

Lemma abst_set_get_neq´´: forall id1 id2 y O, id1<>id2 -> OSAbstMod.get (OSAbstMod.set O id2 y) id1 = OSAbstMod.get O id1.

Lemma join_sig_set_join: forall a b O O1 id, OSAbstMod.join (OSAbstMod.sig id a) O1 O -> OSAbstMod.join (OSAbstMod.sig id b) O1 (OSAbstMod.set O id b).
Lemma fu: forall a b,absdataidspec.beq a b = false -> a <> b.



Qed.

Ltac find_absdata´ Hp id :=
  match Hp with
    | ?A ** ?B =>
      match find_absdata´ A id with
        | some ?a => constr:(some a)
        | none ?a =>
          match find_absdata´ B id with
            | some ?b => constr:(some (a + b)%nat)
            | none ?b => constr:(none (a + b)%nat)
          end
      end
    | Aabsdata id _ => constr:(some 1%nat)
    | _ => constr:(none 1%nat)
  end.

Ltac find_absdata Hp id :=
  let x := find_absdata´ Hp id in
  eval compute in x.

Lemma get_none_joinisig:
  forall qls qid x,EcbMod.get qls qid = None -> EcbMod.joinsig qid x qls (EcbMod.set qls qid x).

Lemma joinisig_get_none:
  forall qls qls´ qid x, EcbMod.joinsig qid x qls qls´ -> EcbMod.get qls qid = None /\ qls´= (EcbMod.set qls qid x).

Ltac absdata_solver :=
  match goal with
    | H : (_,?O,_) |= ?P |- OSAbstMod.get (OSAbstMod.merge ?O _) ?id = Some _ =>
      match find_absdata P id with
        | none _ => fail 1
        | some ?n =>
          sep lift n in H; eapply absdata_elim´ in H; eauto
      end
    | H : (_,?O,_) |= ?P |- OSAbstMod.get ?O ?id = Some _ =>
      match find_absdata P id with
        | none _ => fail 1
        | some ?n =>
          sep lift n in H; eapply absdata_elim in H; eauto
      end
    | |- OSAbstMod.merge (OSAbstMod.set (OSAbstMod.set _ _ _) _ _) _ =
         OSAbstMod.set ( OSAbstMod.set (OSAbstMod.merge _ _) _ _) _ _ =>
      eapply abst_disj_merge_set_eq´;first [absdata_solver | eauto ]
    | |- OSAbstMod.merge (OSAbstMod.set _ _ _ ) _ = OSAbstMod.set (OSAbstMod.merge _ _) _ _ =>
      eapply abst_disj_merge_set_eq;first [absdata_solver | eauto ]
    | |- OSAbstMod.get (OSAbstMod.set _ _ _) _ = Some _ =>
      try solve [ eapply OSAbstMod.set_a_get_a; apply absdataidspec.eq_beq_true; auto
                 | erewrite abst_set_get_neq´´;[ absdata_solver | auto ]]
| |- _ _ _ _ _ => try solve [eapply get_none_joinisig;eauto]
  end.


Lemma cancel_absdata_p:
  forall s O gamma gamma´ P Q id a b,
    (forall O´, (s, O´, gamma) |= P -> (s, O´, gamma´) |= Q) ->
    ((s, O, gamma) |= Aabsdata id a ** P -> (s, OSAbstMod.set O id b, gamma´) |= Aabsdata id b ** Q).

Lemma cancel_absdata_p´:
  forall s O gamma P id a b,
    (s, O, gamma) |= Aabsdata id a ** P -> (s, OSAbstMod.set O id b, gamma) |= Aabsdata id b ** P.

Ltac get_absdata_number´ P id :=
  match P with
    | ?A ** ?B => match get_absdata_number´ A id with
                    | (some ?m) => constr:(some m)
                    | (none ?m) => match get_absdata_number´ B id with
                                     | (some ?n) => constr:(some (m + n)%nat)
                                     | (none ?n) => constr:(none (m + n)%nat)
                                   end
                  end
    | Aabsdata id _ => constr:(some 1%nat)
    | _ => constr:(none 1%nat)
  end.

Ltac get_absdata_number P id :=
  let y := get_absdata_number´ P id in
  eval compute in y.

Ltac cancel_absdata :=
  match goal with
    | H: (?s,?O,_) |= ?P |- (?s,OSAbstMod.set ?O ?id _,_) |= ?Q =>
      match (get_absdata_number P id) with
        | some ?n => match (get_absdata_number Q id) with
                     | some ?m =>
                       sep lift n in H; sep lift m;
                       generalize dependent H; eapply cancel_absdata_p; intros
                     | _ => idtac
                   end
        | _ => idtac
      end
  end.

Ltac cancel_absdata´ :=
  match goal with
    | |- (?s,OSAbstMod.set ?O ?id _,_) |= ?P =>
      match (get_absdata_number P id) with
        | some ?n => sep lift n; eapply cancel_absdata_p´; cancel_absdata´
        | _ => idtac
      end
    | _ =>idtac
  end.

Ltac ins_aop :=
  match goal with
    | H: (_, ?O, ?aop) |= _ |- _ |= <|| ?aop´ ||> ** _ =>
      instantiate (1:=aop´)
  end.

Ltac ins_abst´ P O tm:=
  match P with
    | ?P1 ** ?P2 => match (ins_abst´ P2 O tm) with
                      | ?O´ => ins_abst´ P1 O´ tm
                    end
    | HECBList (EcbMod.set ?ecbls ?x ?b) =>
      constr:(OSAbstMod.set O absecblsid (absecblist (EcbMod.set ecbls x b)))
    | HTCBList (TcbMod.set ?tcbls ?x ?b) =>
      constr:(OSAbstMod.set O abstcblsid (abstcblist (TcbMod.set tcbls x b)))
    | HTime tm => constr:(O)
    | HTime ?tm´ => constr:(OSAbstMod.set O ostmid (ostm tm´))
    | _ => constr:(O)
  end.

Ltac ins_abst:=
  match goal with
    | H: (_,?O,_) |= HECBList _ ** HTCBList _ ** HTime ?tm ** HCurTCB _ ** _ |- _|= ?P =>
      match ins_abst´ P O tm with
        | ?O´ => instantiate (1:=O´)
      end
  end.
Ltac exists_O_aop:=
  do 2 eexists;splits;[ ins_aop;ins_abst | | ].

Definition absimp´´:= fun p p´ : asrt =>
forall (s : taskst) (O : osabst) (gamma : absop),
(s, O, gamma) |= p ->
forall Of : OSAbstMod.map,
OSAbstMod.disj O Of ->
exists O´ gamma´,
(s, O´, gamma´) |= p´/\
OSAbstMod.disj O´ Of /\
hmstepstar gamma (OSAbstMod.merge O Of) gamma´ (OSAbstMod.merge O´ Of) .

Lemma absimp´_imp_absimp:
 forall P P´,absimp´ P P´ -> absimp´ P P´.

Ltac disj_solver:=
    match goal with
      | |- OSAbstMod.disj (OSAbstMod.set _ _ _) _ =>
        eapply abst_get_set_disj;[ auto;absdata_solver | disj_solver;auto ]
      | _ => auto
    end.


Lemma hmstepS_One:
  forall a b c d,
    hmstep a b c d->
    hmstepstar a b c d.