Require Export List_addons.
Load param.


Ltac autoi := automem ; auto.

(** ** Memory *)

Section Memory.

Variable A : Set.
Variable valid : A -> bool.
Variable roots : list A.
Variable children : A -> list A.
Variable raw : A -> bool.

Inductive points_to source target : Prop :=
| points_to_intro : raw source = false -> member target (children source) -> valid target = true ->
  @points_to source target.

Inductive used : A -> Prop :=
| used_root :
   forall n, member n roots -> valid n = true -> used n
| used_child :
   forall k, used k -> forall n, points_to k n ->
   used n
.

Lemma used_valid : forall a, used a -> valid a = true.
Proof.
simple induction 1; auto.
inversion 3; auto.
Qed.

End Memory.

(* used is extensional wrt valid, children, raw *)

Section Used_ext.

Variable A : Set.
Variables valid1 valid2 : A -> bool.
Variable roots : list A.
Variables children1 children2 : A -> list A.
Variables raw1 raw2 : A -> bool.

Section Used_ext_weak.


Hypothesis children_ext : forall a, children1 a = children2 a.
Hypothesis raw_ext : forall a, raw1 a = raw2 a.
Hypothesis valid_ext : forall a, valid1 a = valid2 a.


Theorem used_ext : forall a, used valid1 roots children1 raw1 a -> used valid2 roots children2 raw2 a.
Proof.
induction 1.
 apply used_root.
 assumption.
 rewrite <- valid_ext.
 assumption.
inversion H0.
eapply used_child.
 eassumption.
apply points_to_intro.
  rewrite <- raw_ext.
  assumption.
 rewrite <- children_ext.
 assumption.
rewrite <- valid_ext.
assumption.
Qed.

End Used_ext_weak.

Section Used_ext_strong.

Hypothesis children_ext : forall a, used valid1 roots children1 raw1 a -> children1 a = children2 a.
Hypothesis raw_ext : forall a, used valid1 roots children1 raw1 a -> raw1 a = raw2 a.
Hypothesis valid_ext : forall a, used valid1 roots children1 raw1 a -> valid2 a = true.

Theorem used_ext_strong_direct : forall a, used valid1 roots children1 raw1 a -> used valid2 roots children2 raw2 a.
Proof.
induction 1.
apply used_root.
assumption.
apply valid_ext.
apply used_root.
assumption.
assumption.

inversion H0.
eapply used_child.
eassumption.
apply points_to_intro.
rewrite <- raw_ext.
assumption.
assumption.
rewrite <- children_ext.
assumption.
assumption.
apply valid_ext.
eapply used_child.
eassumption.
assumption.
Qed.

Hypothesis valid2_back_roots : forall a, member a roots -> valid2 a = true -> valid1 a = true.
Hypothesis valid2_back_children : forall a, used valid1 roots children1 raw1 a -> forall b, member b (children2 a) -> valid2 b = true -> valid1 b = true.

Theorem used_ext_strong_recip : forall a, used valid2 roots children2 raw2 a -> used valid1 roots children1 raw1 a.
Proof.
induction 1.
apply used_root.
assumption.
eauto.
inversion H0.
eapply used_child.
eassumption.
apply points_to_intro.
rewrite raw_ext.
assumption.
assumption.
rewrite children_ext.
assumption.
assumption.
eauto.
Qed.

End Used_ext_strong.

End Used_ext.

(** *** Morphisms

(not yet used)

Section Memory_morphisms.

Variable A1 A2 : Set.
Variables (r1 : list A1) (r2 : list A2)
 (c1 : A1 -> list A1) (c2 : A2 -> list A2)
 (raw1 : A1 -> bool) (raw2 : A2 -> bool)
 (f : A1 -> A2)
.

Definition morphism_forward
:=
 (forall n, member n r1 -> member (f n) r2,
 forall p q, points_to c1 raw1 p q -> points_to c2 raw2 (f p) (f q))
.

Definition morphism_backward
:=
 (forall n, member (f n) r2 -> member (n) r1,
 forall p q, points_to c2 raw2 (f p) (f q) -> points_to c1 raw1 (p) (q))

.

Definition injective
:=
 forall i j, f i = f j -> i = j
.

End Memory_morphisms.
*)


Hint Constructors used.