Library OracleLanguages.Imp.DisjointStates

Require Import Common.
Require Import Imp.Lang.

Module Make
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT).

  Definition store_is_union (s s₁ s₂ : store) : Prop :=
    (∀ x v, M.MapsTo x v s₁ → M.MapsTo x v s)
    ∧ (∀ x v, M.MapsTo x v s₂ → M.MapsTo x v s)
    ∧ (∀ x v, M.MapsTo x v s → M.MapsTo x v s₁ ∨ M.MapsTo x v s₂).

  Lemma store_is_union_sym:
    ∀ s s₁ s₂,
      store_is_union s s₁ s₂ → store_is_union s s₂ s₁.

  Hint Resolve store_is_union_sym.

  Lemma equal_store_is_union:
    ∀ s₁ s₂ s s₁' s₂',
      M.Equal s₁' s₁ →
      M.Equal s₂' s₂ →
      store_is_union s s₁ s₂ →
      store_is_union s s₁' s₂'.

  Lemma store_is_union_add:
    ∀ s₁ s₂ s x v,
      store_is_union s s₁ s₂ →
      (¬ M.In x s₂) →
      store_is_union (M.add x v s) (M.add x v s₁) s₂.

  Hint Resolve store_is_union_add.

  Definition In_var_cont (x : varid) (k : cont) : Prop :=
    ∃ c, In c k ∧ In_var x c.

  Definition cont_classified (k : cont) (V : varid → Prop) : Prop :=
    ∀ x, In_var_cont x k → V x.

  Definition store_classified (s : store) (V : varid → Prop) : Prop :=
    ∀ x, M.In x s → V x.

  Property cont_classified_1:
    ∀ c k V,
    cont_classified (c::k) V →
    ∀ x, In_var x c → V x.

  Property cont_classified_2:
    ∀ c k V,
      cont_classified (c::k) V →
      cont_classified k V.

  Definition disjoint_states (S₁ S₂ : state) : Prop :=
    let '(k₁, s₁) := S₁ in
    let '(k₂, s₂) := S₂ in
    ∃ (V₁ V₂ : varid → Prop),
      cont_classified k₁ V₁
      ∧ cont_classified k₂ V₂
      ∧ store_classified s₁ V₁
      ∧ store_classified s₂ V₂
      ∧ (∀ x, V₁ x → V₂ x → Logic.False).

  Lemma disjoint_states_sym:
    ∀ S₁ S₂,
      disjoint_states S₁ S₂ → disjoint_states S₂ S₁.

  Hint Resolve disjoint_states_sym.

  Lemma step_disjoint_states:
    ∀ S₁ S₁' S₂,
      disjoint_states S₁ S₂ →
      step tt S₁ = Some S₁' →
      disjoint_states S₁' S₂.

  Lemma step_2_disjoint_states:
    ∀ S₁ S₁' S₂ S₂',
      disjoint_states S₁ S₂ →
      step tt S₁ = Some S₁' →
      step tt S₂ = Some S₂' →
      disjoint_states S₁' S₂'.

  Lemma disjoint_eval_exp:
    ∀ (e : exp) (s : store) (V₁ V₂ : varid → Prop) (x : varid) v,
      (∀ y, In_exp_var y e → V₁ y) →
      V₂ x →
      (∀ x, V₁ x → V₂ x → Logic.False) →
      eval_exp (M.add x v s) e = eval_exp s e.

  Lemma disjoint_eval_bexp:
    ∀ (b : bexp) (s : store) (V₁ V₂ : varid → Prop) (x : varid) v,
      (∀ y, In_bexp_var y b → V₁ y) →
      V₂ x →
      (∀ x, V₁ x → V₂ x → Logic.False) →
      eval_bexp (M.add x v s) b = eval_bexp s b.

  Lemma disjoint_union_eval_exp_same:
    ∀ (e : exp) (s₁ s₂ s : store) (V₁ V₂ : varid → Prop),
      store_is_union s s₁ s₂ →
      (∀ x, In_exp_var x e → V₁ x) →
      (∀ x, M.In x s₁ → V₁ x) →
      (∀ y, M.In y s₂ → V₂ y) →
      (∀ x, V₁ x → V₂ x → Logic.False) →
      eval_exp s₁ e = eval_exp s e.

  Lemma disjoint_union_eval_bexp_same:
    ∀ (b : bexp) (s₁ s₂ s : store) (V₁ V₂ : varid → Prop),
      store_is_union s s₁ s₂ →
      (∀ x, In_bexp_var x b → V₁ x) →
      (∀ x, M.In x s₁ → V₁ x) →
      (∀ y, M.In y s₂ → V₂ y) →
      (∀ x, V₁ x → V₂ x → Logic.False) →
      eval_bexp s₁ b = eval_bexp s b.

  Lemma step_disjoint_states_union:
    ∀ S₁ S₁' s s' k' S₂,
      disjoint_states S₁ S₂ →
      store_is_union s (snd S₁) (snd S₂) →
      step tt S₁ = Some S₁' →
      step tt (fst S₁, s) = Some (k', s') →
      k' = fst S₁' ∧ store_is_union s' (snd S₁') (snd S₂).

  Lemma step_disjoint_states_union_same_crashes:
    ∀ S₁ s S₂,
      disjoint_states S₁ S₂ →
      store_is_union s (snd S₁) (snd S₂) →
      step tt S₁ = None ↔ step tt (fst S₁, s) = None.

  Lemma step_disjoint_union_states:
    ∀ S₁ S₁' s s' k' S₂,
      disjoint_states S₁ S₂ →
      store_is_union s (snd S₁) (snd S₂) →
      step tt S₁ = Some S₁' →
      step tt (fst S₁, s) = Some (k', s') →
      k' = fst S₁' ∧ store_is_union s' (snd S₁') (snd S₂)
      ∧ disjoint_states S₁' S₂.
End Make.