Require Import Vbase List extralib.
Require Import Classical ClassicalDescription.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fsl ghosts fsl_addons.
Require Import permission GpsSepAlg.
Require Import QArith helpers_rationals fslassnlemmas2 normalizability.
Require Import arc_permissions arc_ghosts.

Definition arc_assn := assn (Fractional_Permissions :: nil) (TokenMonoid :: nil).

Program Definition Pointsto l q v :=
  match excluded_middle_informative (0 ≤ q ≤ 1) return arc_assn with
    | right _ ⇒ Afalse
    | left _ ⇒ match excluded_middle_informative (q == 0) return arc_assn with
                   | left _ ⇒ Aemp
                   | right _ ⇒ Apt Fractional_Permissions (in_eq _ _) (QP (Qred q) _ (eq_sym (Qred_Qred q))) _ l v
                  end
  end.

Definition GhostPlus l q :=
  match excluded_middle_informative (0 ≤ Qred q) return arc_assn with
    | left GE ⇒ Aghost TokenMonoid (in_eq _ _) l (TokPlus (Qred q) GE (eq_sym (Qred_Qred q)))
    | right _ ⇒ Afalse
  end.

Definition GhostMinus l q :=
  match excluded_middle_informative (0 ≤ Qred q) return arc_assn with
    | right _ ⇒ Afalse
    | left GE ⇒ Aghost TokenMonoid (in_eq _ _) l (TokMinus (Qred q) GE (eq_sym (Qred_Qred q)))
  end.

Lemma empty_pointsto d v: Pointsto d 0 v = Aemp.

Lemma Pointsto_eq x v f f': f == f' → Pointsto x f v = Pointsto x f' v.

Lemma GhostPlus_eq g f f' : f == f' → GhostPlus g f = GhostPlus g f'.

Lemma GhostMinus_eq g f f' : f == f' → GhostMinus g f = GhostMinus g f'.

Lemma triangle_GhostPlus g q: equivalent (Atriangle (GhostPlus g q)) (GhostPlus g q).

Lemma triangle_GhostMinus g q: equivalent (Atriangle (GhostMinus g q)) (GhostMinus g q).

Lemma nabla_GhostPlus g q: equivalent (Anabla (GhostPlus g q)) (GhostPlus g q).

Lemma nabla_GhostMinus g q: equivalent (Anabla (GhostMinus g q)) (GhostMinus g q).

Lemma normalizable_GhostPlus: ∀ g q, normalizable (GhostPlus g q).

Lemma normalizable_Pointsto: ∀ x q v, normalizable (Pointsto x q v).

Lemma consume_token g f q: implies (GhostMinus g f &*& GhostPlus g q) (GhostMinus g (f - q)).

Lemma consume_token2 g f q: implies (GhostPlus g q &*& GhostMinus g f) (GhostMinus g (f - q)).

Lemma produce_one_token g q: equivalent (GhostMinus g q) (GhostMinus g (q + 1) &*& GhostPlus g 1).

Lemma combine_tokens g f q: implies (GhostPlus g f &*& GhostPlus g q) (GhostPlus g (f + q)).

Lemma split_tokens g a b c :
  a == b + c → b ≥ 0 → c ≥ 0 → equivalent (GhostPlus g a) (GhostPlus g b &*& GhostPlus g c).

Lemma empty_ghost_r g a Ghost:
  Ghost = GhostPlus ∨ Ghost = GhostMinus → equivalent (Ghost g a &*& GhostPlus g 0) (Ghost g a).

Lemma empty_ghost_l g a Ghost:
  Ghost = GhostPlus ∨ Ghost = GhostMinus → equivalent (GhostPlus g 0 &*&Ghost g a) (Ghost g a).

Lemma split_pointsto x v a b c :
  a == b + c → b ≥ 0 → c ≥ 0 → equivalent (Pointsto x a v) (Pointsto x b v &*& Pointsto x c v).

Lemma rule_alloc_na_with_two_ghosts:
  triple Aemp
         Ealloc
         (fun x ⇒ Aexists (fun g ⇒ Aexists (fun g' ⇒ Aptu x &*& GhostMinus g 0 &*& GhostMinus g' 0))).

Lemma rule_load_poinsto x q v:
  0 < q → q ≤ 1 →
  triple (Pointsto x q v) (Eload ATna x) (fun y ⇒ if (y == v)%bool then Pointsto x q v else Afalse).