Library SLSET

Require Import ZArith.
Require Import String Ascii.
Require Import Bool.
Require Import PAInfTheoryDi.
Require Import Sets.Ensembles.

Module Type STRVAR <: VARIABLE.
  Parameter var : Type.   Parameter var_eq_dec : forall v1 v2 : var, {v1 = v2} + {v1 <> v2}.
  Parameter var2string : var -> string.
  Parameter string2var : string -> var.
  Parameter freshvar : var.
  Axiom var2String2var : forall v, string2var(var2string v) = v.
  Axiom String2var2String : forall s, var2string(string2var s) = s.
End STRVAR.

Module HeapSolver(sv:STRVAR).

Import sv.

Definition heap := Ensemble nat.

Definition empty_heap := Empty_set nat.

Definition single_heap n := Singleton nat n.

Definition heap_union h1 h2 := Union nat h1 h2.

Definition heap_is_disjoint h1 h2 := Disjoint nat h1 h2.

Inductive SE : Type :=
  | H_Set_Union : SE -> SE -> SE
  | H_Set : heap -> SE
  | H_Set_Single : nat -> SE
  | H_Set_Emp : SE
.

Inductive SF : Type :=
  | H_Set_Eq : SE -> SE -> SF
  | H_Set_Disj : SE -> SE -> SF
  | H_Set_And : SF -> SF -> SF
.

Inductive HF : Type :=
  | H_Emp : HF
  | H_Ptto : nat -> nat -> HF
  | H_Star : HF -> HF -> HF
  | H_List : nat -> heap -> HF
.

Fixpoint SE2Set (s:SE) : heap :=
match s with
 | H_Set_Emp => empty_heap
 | H_Set h => h
 | H_Set_Single n => single_heap n
 | H_Set_Union s1 s2 => heap_union (SE2Set s1) (SE2Set s2)
end.

Inductive LL (e:nat) : heap -> Prop :=
  | NIL_LL : LL e empty_heap
  | CONS_LL : forall h h1 h2 e1, h = heap_union h1 h2
              -> heap_is_disjoint h1 h2
              -> h1 = single_heap e
              -> LL e1 h2 -> LL e h.

Inductive LLSET (n:nat) (S: heap): Prop :=
  | NIL_LLSET : S = empty_heap -> LLSET n S
  | CONS_LLSET : forall S1 S2 n1, S = heap_union S1 S2
              -> heap_is_disjoint S1 S2
              -> S1 = single_heap n
              -> LLSET n1 S2 -> LLSET n S.

Theorem LL_is_same_as_LLSET: forall h e, LLSET e h <-> LL e h.
Proof.
intros.
split.
intro Hx.
induction Hx.
subst S.
apply NIL_LL.
subst.
eapply CONS_LL.
reflexivity.
trivial.
trivial.
apply IHHx.
intro Hx.
induction Hx.
apply NIL_LLSET. trivial.
subst. eapply CONS_LLSET.
reflexivity. trivial. trivial. apply IHHx.
Qed.

Fixpoint valid (form: HF) (h:heap) : Prop :=
match form with
   H_Emp => h = empty_heap
 | H_Ptto n1 _ => h = (single_heap n1)
 | H_Star f1 f2 => exists h1 h2, (valid f1 h1) /\ (valid f2 h2)
                   /\ (heap_is_disjoint h1 h2) /\ h = (heap_union h1 h2)
 | H_List n h => LLSET n h
end.

Fixpoint set_valid (form: SF) : Prop :=
match form with
   H_Set_Eq s1 s2 => (SE2Set s1) = (SE2Set s2)
 | H_Set_And f1 f2 => set_valid f1 /\ set_valid f2
 | H_Set_Disj s1 s2 => heap_is_disjoint (SE2Set s1) (SE2Set s2)
end.

Fixpoint XMem (f: HF) : SE :=
match f with
  | H_Emp => H_Set_Emp
  | H_Ptto n1 _ => (H_Set_Single n1)
  | H_List n h => H_Set h
  | H_Star f1 f2 => H_Set_Union (XMem f1) (XMem f2)
end.

Fixpoint XMem_Form (f: HF) x : Prop :=
match f with
 | H_Star f1 f2 =>
         exists x1 x2 x3 x4, (set_valid
         (H_Set_And
         (H_Set_Disj (H_Set x1) (H_Set x2))
         (H_Set_Eq (H_Set x) (H_Set_Union (H_Set x1) (H_Set x2)))))
         /\ (XMem_Form f1 x3) /\ (XMem_Form f2 x4)
 | _ => set_valid (H_Set_Eq (H_Set x) (XMem f))
end.

Theorem valid_xmem_form: forall f, (exists h, (valid f h))
-> (exists x, (XMem_Form f x)).
Proof.

intros.
induction f.
unfold valid,set_valid.
simpl.

tauto.

unfold valid,set_valid.
simpl. tauto.

destruct H.
simpl.
simpl in H.
exists x.
destruct H,H.
destruct IHf1.
destruct H.
exists x0. tauto.

destruct IHf2.
destruct H.
destruct H1.
exists x1. tauto.

exists x0,x1,x2,x3.
split.
tauto. tauto.

simpl.
intros.
exists h. tauto.
Qed.

End HeapSolver.