Require Import VST.msl.msl_standard.
Require Import VST.msl.Coqlib2.
Set Implicit Arguments.

Inductive fold_rel (A: Type) (f: A -> A -> A -> Prop):  A -> list A -> A -> Prop :=
| fold_rel_nil: forall w, fold_rel f w nil w
| fold_rel_cons: forall a l w w1 w2,
            f w a w1 ->
            fold_rel f w1 l w2 ->
            fold_rel f w (a::l) w2.

Inductive list_forall2 {A B} (P: A -> B -> Prop): list A -> list B -> Prop :=
  | list_forall2_nil:
      list_forall2 P nil nil
  | list_forall2_cons:
      forall a1 al b1 bl,
      P a1 b1 ->
      list_forall2 P al bl ->
      list_forall2 P (a1 :: al) (b1 :: bl).

Fixpoint replace (A: Type) (l: list A) (n:nat) (new: A) {struct n} : option (list A) :=
  match (l, n) with
    | (nil, n) => None
    | (x :: xs, O) => Some (new :: xs)
    | (x :: xs, S n) =>
      match (replace xs n new) with
        |  None => None
        |  Some xs => Some (x :: xs)
      end
  end.



Definition list_join {A} {JA: Join A}: A -> list A -> A -> Prop :=
   fold_rel join.

Lemma list_join_assoc1 {A} {JA: Join A}{PA: Perm_alg A}:
 forall {a b cl d e},
   join a b d -> list_join d cl e ->
  exists f, list_join b cl f /\ join a f e.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
intros.
(* Goal: @ex A (fun f : A => and (@list_join A JA b cl f) (@join A JA a f e)) *)
revert a b H.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
induction H0; intros.
(* Goal: @ex A (fun f : A => and (@list_join A JA b (@nil A) f) (@join A JA a f w)) *)
(* Goal: @ex A (fun f : A => and (@list_join A JA b (@cons A a l) f) (@join A JA a0 f w2)) *)
exists b. split; auto. constructor.
(* Goal: @ex A (fun f : A => and (@list_join A JA b (@cons A a l) f) (@join A JA a0 f w2)) *)
destruct (join_assoc H1 H) as [ba [? ?]].
(* Goal: @ex A (fun f : A => and (@list_join A JA b (@cons A a l) f) (@join A JA a0 f w2)) *)
destruct (IHfold_rel _ _ H3) as [f [? ?]]; clear IHfold_rel.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
exists f; split; auto.
(* Goal: @list_join A JA b (@cons A a l) f *)
econstructor; eauto.
Qed.

Lemma list_join_assoc2 {A}  {JA: Join A}{PA: Perm_alg A}:
  forall {a b: A} {cl e f},
   list_join b cl f -> join a f e ->
   exists d,  join a b d /\ list_join d cl e.
Proof.
(* Goal: forall (a b : A) (cl : list A) (e f : A) (_ : @list_join A JA b cl f) (_ : @join A JA a f e), @ex A (fun d : A => and (@join A JA a b d) (@list_join A JA d cl e)) *)
do 3 intro; revert a b; induction cl; intros; inv H.
(* Goal: @fold_rel A (@join A JA) c (@nil A) c *)
(* Goal: @join A JA a b c *)
exists e; split; auto; constructor.
(* Goal: @ex A (fun d : A => and (@join A JA a0 b d) (@list_join A JA d (@cons A a cl) e)) *)
destruct (IHcl _ _ _ _ H6 H0) as [d [? ?]].
(* Goal: @ex A (fun d : A => and (@join A JA a0 b d) (@list_join A JA d (@cons A a cl) e)) *)
destruct (join_assoc (join_comm H4) (join_comm H)) as [g [? ?]].
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
exists g; split; auto.
(* Goal: @list_join A JA g (@cons A a cl) e *)
constructor 2 with d; auto.
Qed.

Lemma list_join_app {A} {JA: Join A}:
  forall {a: A} {bl c dl e},
   list_join a bl c -> list_join c dl e -> list_join a (bl++dl) e.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
intros a bl; revert a; induction bl; intros.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
simpl.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
auto.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
rewrite <- app_comm_cons.
econstructor 2.
apply H4.
eapply IHbl.
apply H6.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
auto.
Qed.

Lemma list_join_unapp {A}  {JA: Join A}:
  forall {a:A}  {bl dl e},
  list_join a (bl++dl) e -> exists c, list_join a bl c /\ list_join c dl e.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
intros a bl; revert a; induction bl; intros.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
simpl in H. exists a; split; auto. constructor.
(* Goal: @ex A (fun c : A => and (@list_join A JA a0 (@cons A a bl) c) (@list_join A JA c dl e)) *)
rewrite <- app_comm_cons in H.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
(* Goal: @ex A (fun c : A => and (@list_join A JA a0 (@cons A a bl) c) (@list_join A JA c dl e)) *)
destruct (IHbl _ _ _ H5) as [c [? ?]]. clear IHbl.
(* Goal: @ex A (fun c : A => and (@list_join A JA a0 (@cons A a bl) c) (@list_join A JA c dl e)) *)
exists c.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
econstructor 2; eauto.
Qed.

Lemma list_join_1 {A} {JA: Join A}:
  forall a b c: A, join a b c = list_join a (b::nil) c.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
intros; apply prop_ext; split; intros.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
econstructor 2; eauto.
(* Goal: @fold_rel A (@join A JA) c (@nil A) c *)
(* Goal: @join A JA a b c *)
constructor.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
(* Goal: @join A JA a b c *)
inv H5.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
auto.
Qed.

Definition age1_list {A} `{ageable A} := list_forall2 age.

Lemma age1_list_join {A} {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall l (phi phi' phi2: A),
        age phi phi' ->
        list_join phi l phi2 ->
        exists l', exists phi2', age1_list l l' /\ age phi2 phi2' /\ list_join phi' l' phi2'.
Proof.
(* Goal: forall (l : list A) (phi phi2 phi2' : A) (_ : @eq (option A) (@age1 A agA phi2) (@Some A phi2')) (_ : @list_join A JA phi l phi2), @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA l l') (@list_join A JA phi' l' phi2')))) *)
induction l; intros; inv H0.
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi2) (@Some A phi')) (and (@age1_list A agA (@nil A) l') (@list_join A JA phi' l' phi2')))) *)
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
exists (@nil A).
(* Goal: @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) (@cons A a' l')) (@list_join A JA phi' (@cons A a' l') phi2'))) *)
exists phi'.
(* Goal: @fold_rel A (@join A JA) c (@nil A) c *)
(* Goal: @join A JA a b c *)
repeat split; auto; constructor.
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
rename w1 into phi1.
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi2' : A => and (@age1_list A agA (@cons A a l) l') (and (@age A agA phi2 phi2') (@list_join A JA phi' l' phi2')))) *)
destruct (age1_join _ H4 H) as [a' [phi1' [? [? ?]]]].
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi2' : A => and (@age1_list A agA (@cons A a l) l') (and (@age A agA phi2 phi2') (@list_join A JA phi' l' phi2')))) *)
specialize ( IHl phi1 phi1' phi2 H2 H6).
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi2' : A => and (@age1_list A agA (@cons A a l) l') (and (@age A agA phi2 phi2') (@list_join A JA phi' l' phi2')))) *)
destruct IHl as [l' [phi2' [? [? ?]]]].
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
exists (a' :: l').
(* Goal: @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi2) (@Some A phi')) (and (@age1_list A agA (@nil A) (@nil A)) (@list_join A JA phi' (@nil A) phi2'))) *)
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
exists phi2'.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
repeat split; auto; econstructor 2; eauto.
Qed.

Lemma age1_list_join2 {A} {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall (l: list A) phi phi2 phi2',  age1 phi2 = Some phi2' -> list_join phi l phi2 ->
        exists l', exists phi',  age1 phi = Some phi' /\ age1_list l l' /\ list_join phi' l' phi2'.
Proof.
(* Goal: forall (l : list A) (phi phi2 phi2' : A) (_ : @eq (option A) (@age1 A agA phi2) (@Some A phi2')) (_ : @list_join A JA phi l phi2), @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA l l') (@list_join A JA phi' l' phi2')))) *)
induction l; intros; inv H0.
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi2) (@Some A phi')) (and (@age1_list A agA (@nil A) l') (@list_join A JA phi' l' phi2')))) *)
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
exists (@nil A).
(* Goal: @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi2) (@Some A phi')) (and (@age1_list A agA (@nil A) (@nil A)) (@list_join A JA phi' (@nil A) phi2'))) *)
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
exists phi2'.
(* Goal: @fold_rel A (@join A JA) c (@nil A) c *)
(* Goal: @join A JA a b c *)
repeat split; auto; constructor.
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
rename w1 into phi1.
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
destruct (IHl phi1 phi2 phi2' H H6) as [l' [phi1' [? [? ?]]]].
(* Goal: @ex (list A) (fun l' : list A => @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) l') (@list_join A JA phi' l' phi2')))) *)
destruct (age1_join2 _ H4 H0) as [phi' [a' [? [? ?]]]].
(* Goal: @ex A (fun phi' : A => and (@eq (option A) (@age1 A agA phi) (@Some A phi')) (and (@age1_list A agA (@cons A a l) (@cons A a' l')) (@list_join A JA phi' (@cons A a' l') phi2'))) *)
exists (a'::l'). exists phi'.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
repeat split; auto; econstructor 2; eauto.
Qed.

Lemma list_join_split_nth {A}{JA: Join A}{PA: Perm_alg A}:
 forall n (l: list A) phin phi phia phib phi2,
  nth_error l n = Some phin -> list_join phi l phi2 -> join phib phia phin ->
           exists phic, exists l',
                 replace l n phib = Some l' /\ join phi phia phic /\ list_join phic l' phi2.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
induction n; intros.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
destruct l.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@nil A) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@cons A a l) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
discriminate.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) O phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A l (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
inv H3.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
inv H0.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
simpl.
destruct (join_assoc H1 (join_comm H4))
      as [f [? ?]].
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@Some (list A) (@cons A phib l)) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
exists f; exists (phib::l).
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
repeat split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
econstructor 2; eauto.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
simpl in H.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
destruct l.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
inv H0.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) match @replace A l n phic with | Some xs => @Some (list A) (@cons A a xs) | None => @None (list A) end (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
destruct (IHn _ _ _ _ _ _ H H7 H1) as [phic [l' [? [? ?]]]].
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
simpl. rewrite H0.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l'0 : list A => and (@eq (option (list A)) (@Some (list A) (@cons A a l')) (@Some (list A) l'0)) (and (@join A JA phi phia phic) (@list_join A JA phic l'0 phi2)))) *)
destruct (join_assoc (join_comm H5) H2) as [f [? ?]].
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
exists f; exists (a::l'); repeat split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
econstructor 2; eauto.
Qed.

Lemma list_join_join_nth {A} {JA: Join A}{PA: Perm_alg A}:
 forall n (l: list A) phin phi phia phib phi2,
  nth_error l n = Some phin -> list_join phi l phi2 -> join phi2 phia phib ->
           exists phic, exists l',
                 join phin phia phic /\ replace l n phic = Some l' /\ list_join phi l' phib.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
induction n; intros.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@nil A) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@cons A a l) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
destruct l; try discriminate.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
inv H0.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) O phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A l (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
inv H3.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
simpl.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@Some (list A) (@cons A phic l)) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A l (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
destruct (list_join_assoc2 H7 (join_comm H1)) as [f [? ?]].
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@Some (list A) (@cons A phic l)) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A l (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
destruct (join_assoc H5 (join_comm H)) as [g [? ?]].
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
exists g; exists (g::l); repeat split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
econstructor 2; eauto.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
destruct l; simpl in H.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
inv H.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
inv H0.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
simpl.
destruct (IHn _ _ _ _ _ _ H H7 H1) as [phic  [l' [? [? ?]]]].
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) match @replace A l n phic with | Some xs => @Some (list A) (@cons A a xs) | None => @None (list A) end (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
exists phic. rewrite H2. exists (a::l').
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
repeat split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
econstructor 2; eauto.
Qed.

(*****************************)

Lemma list_join_comparable {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall (phi1: A) l phi2, list_join phi1 l phi2 -> comparable phi1 phi2.
Proof.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA O phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA O phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
  intros; revert phi1 phi2 H; induction l; simpl; intros; inv H.
(* Goal: @comparable A JA SA phi phi *)
  apply comparable_refl.
(* Goal: @comparable A JA SA phi1 phi2 *)
  rename w1 into phi0.
(* Goal: @comparable A JA SA phi1 phi2 *)
  apply comparable_trans with phi0.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
  apply join_comparable with a; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
  auto.
Qed.

Lemma join_comparable'  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall phi1 phi2 phi3: A, join phi1 phi2 phi3 -> comparable phi2 phi3.
Proof. intros; apply join_comparable with phi1; apply join_comm; auto. Qed.

Lemma join_comparable2'  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall phi1 phi2 phi3: A, join phi1 phi2 phi3 -> comparable phi2 phi1.
Proof. intros; apply comparable_sym; eapply join_comparable2; eauto. Qed.

Lemma list_join_comparable'  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall (phi1: A) l phi2, list_join phi1 l phi2 -> comparable phi2 phi1.
Proof. intros; apply comparable_sym; eapply list_join_comparable; eauto. Qed.

Lemma join_comparable''  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall phi1 phi2 phi3: A, join phi1 phi2 phi3 -> comparable phi3 phi2.
Proof. intros; apply comparable_sym; eapply join_comparable'; eauto. Qed.

Lemma join_comparable'''  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall phi1 phi2 phi3: A, join phi1 phi2 phi3 -> comparable phi3 phi1.
Proof. intros; apply comparable_sym; eapply join_comparable; eauto. Qed.

Lemma joins_comparable  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall phi1 phi2: A, joins phi1 phi2 -> comparable phi1 phi2.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
  unfold joins; intros.
(* Goal: @comparable A JA SA phi1 phi2 *)
  destruct H as [phi3 ?].
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
  eapply join_comparable2; eauto.
Qed.

Lemma joins_comparable2 {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
     forall phi1 phi2: A, joins phi2 phi1 -> comparable phi1 phi2.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
unfold joins; intros.
(* Goal: @comparable A JA SA phi1 phi2 *)
destruct H as [phi3 ?].
(* Goal: @comparable A JA SA phi1 phi2 *)
apply comparable_sym.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
eapply join_comparable2; eauto.
Qed.

Lemma join_sub_comparable  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall phi1 phi2: A, join_sub phi1 phi2 -> comparable phi1 phi2.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
unfold joins; intros.
(* Goal: @comparable A JA SA phi1 phi2 *)
destruct H as [phi3 ?].
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
eapply join_comparable; eauto.
Qed.

Lemma join_sub_comparable2 {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
     forall phi1 phi2: A, join_sub phi2 phi1 -> comparable phi1 phi2.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
unfold joins; intros.
(* Goal: @comparable A JA SA phi1 phi2 *)
destruct H as [phi3 ?].
(* Goal: @comparable A JA SA phi1 phi2 *)
apply comparable_sym.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
eapply join_comparable; eauto.
Qed.

Lemma eq_comparable {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
   forall phi1 phi2: A, phi1=phi2 -> comparable phi1 phi2.
Proof.
(* Goal: @comparable A JA SA phi phi *)
intros; subst; apply comparable_refl.
Qed.

Lemma eq_comparable2 {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
   forall phi1 phi2: A, phi2=phi1 -> comparable phi1 phi2.
Proof.
(* Goal: @comparable A JA SA phi phi *)
intros; subst; apply comparable_refl.
Qed.

Lemma ageN_join {A}  {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall n (w1 w2 w3 w1': A),
   join w1 w2 w3 ->
      ageN n w1 = Some w1' ->
      exists w2', exists w3',
        ageN n w2 = Some w2' /\ ageN n w3 = Some w3' /\ join w1' w2' w3'.
Proof.
(* Goal: forall (n : nat) (w1 w2 w1' w2' : A) (_ : @eq (option A) (@ageN A agA n w1) (@Some A w1')) (_ : @eq (option A) (@ageN A agA n w2) (@Some A w2')) (_ : @comparable A JA SA w1 w2), @comparable A JA SA w1' w2' *)
unfold ageN in *.
(* Goal: forall (n : nat) (w1 w2 w1' w2' : A) (_ : @eq (option A) (@composeOptN A (@age1 A agA) n w1) (@Some A w1')) (_ : @eq (option A) (@composeOptN A (@age1 A agA) n w2) (@Some A w2')) (_ : @comparable A JA SA w1 w2), @comparable A JA SA w1' w2' *)
induction n; intros; simpl in *.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
exists w2; exists w3; repeat split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
inv H0; auto.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@nil A) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@cons A a l) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
case_eq (age1 w1); intros; rewrite H1 in H0; try discriminate.
(* Goal: @ex A (fun w2' : A => @ex A (fun w3' : A => and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2')) (and (@eq (option A) match @age1 A agA w3 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w3')) (@join A JA w1' w2' w3')))) *)
destruct (age1_join _ H H1) as [w2' [w3' [? [? ?]]]].
(* Goal: @ex A (fun w2' : A => @ex A (fun w3' : A => and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2')) (and (@eq (option A) match @age1 A agA w3 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w3')) (@join A JA w1' w2' w3')))) *)
destruct (IHn _ _ _ _ H2 H0) as [w2'' [w3'' [? [? ?]]]].
(* Goal: @ex A (fun w1' : A => @ex A (fun w2' : A => and (@eq (option A) match @age1 A agA w1 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w1')) (and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2')) (@join A JA w1' w2' w3')))) *)
clear IHn.
(* Goal: @ex A (fun w2' : A => @ex A (fun w3' : A => and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2')) (and (@eq (option A) match @age1 A agA w3 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w3')) (@join A JA w1' w2' w3')))) *)
exists w2''; exists w3''. rewrite H3; rewrite H4.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
repeat split; auto.
Qed.

Lemma ageN_join2 {A}  {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall n (w1 w2 w3 w3': A),
   join w1 w2 w3 ->
      ageN n w3 = Some w3' ->
      exists w1', exists w2',
        ageN n w1 = Some w1' /\ ageN n w2 = Some w2' /\ join w1' w2' w3'.
Proof.
(* Goal: forall (n : nat) (w1 w2 w1' w2' : A) (_ : @eq (option A) (@ageN A agA n w1) (@Some A w1')) (_ : @eq (option A) (@ageN A agA n w2) (@Some A w2')) (_ : @comparable A JA SA w1 w2), @comparable A JA SA w1' w2' *)
unfold ageN in *.
(* Goal: forall (n : nat) (w1 w2 w1' w2' : A) (_ : @eq (option A) (@composeOptN A (@age1 A agA) n w1) (@Some A w1')) (_ : @eq (option A) (@composeOptN A (@age1 A agA) n w2) (@Some A w2')) (_ : @comparable A JA SA w1 w2), @comparable A JA SA w1' w2' *)
induction n; intros; simpl in *.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
exists w1; exists w2; repeat split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
inv H0; auto.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@nil A) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@cons A a l) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
case_eq (age1 w3); intros; rewrite H1 in H0; try discriminate.
(* Goal: @ex A (fun w1' : A => @ex A (fun w2' : A => and (@eq (option A) match @age1 A agA w1 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w1')) (and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2')) (@join A JA w1' w2' w3')))) *)
destruct (age1_join2 _ H H1) as [w1' [w2' [? [? ?]]]].
(* Goal: @ex A (fun w1' : A => @ex A (fun w2' : A => and (@eq (option A) match @age1 A agA w1 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w1')) (and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2')) (@join A JA w1' w2' w3')))) *)
destruct (IHn _ _ _ _ H2 H0) as [w1'' [w2'' [? [? ?]]]].
(* Goal: @ex A (fun w1' : A => @ex A (fun w2' : A => and (@eq (option A) match @age1 A agA w1 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w1')) (and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2')) (@join A JA w1' w2' w3')))) *)
clear IHn.
(* Goal: and (@eq (option A) match @age1 A agA w1 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w1'')) (and (@eq (option A) match @age1 A agA w2 with | Some w' => @composeOptN A (@age1 A agA) n w' | None => @None A end (@Some A w2'')) (@join A JA w1'' w2'' w3')) *)
exists w1''; exists w2''. rewrite H3; rewrite H4.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
repeat split; auto.
Qed.

Lemma ageN_comparable {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall n (w1 w2 w1' w2': A),
        ageN n w1 = Some w1' -> ageN n w2 = Some w2' -> comparable w1 w2 -> comparable w1' w2'.
Proof.
(* Goal: forall (n : nat) (w1 w2 w1' w2' : A) (_ : @eq (option A) (@ageN A agA n w1) (@Some A w1')) (_ : @eq (option A) (@ageN A agA n w2) (@Some A w2')) (_ : @comparable A JA SA w1 w2), @comparable A JA SA w1' w2' *)
unfold ageN in *.
(* Goal: forall (n : nat) (w1 w2 w1' w2' : A) (_ : @eq (option A) (@composeOptN A (@age1 A agA) n w1) (@Some A w1')) (_ : @eq (option A) (@composeOptN A (@age1 A agA) n w2) (@Some A w2')) (_ : @comparable A JA SA w1 w2), @comparable A JA SA w1' w2' *)
induction n; intros; simpl in *.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
inv H; inv H0; auto.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@nil A) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A (@cons A a l) O phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@eq (option (list A)) (@replace A l (S n) phib) (@Some (list A) l')) (and (@join A JA phi phia phic) (@list_join A JA phic l' phi2)))) *)
revert H H0; case_eq (age1 w1); case_eq (age1 w2); intros; try discriminate.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
eapply IHn; eauto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
eapply age_comparable; eauto.
Qed.

Lemma join_unage  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall (phi3 phi1' phi2' phi3': A),
    age1 phi3 = Some phi3' ->
    join phi1' phi2' phi3' ->
    exists phi1, exists phi2, join phi1 phi2 phi3 /\
      age1 phi1 = Some phi1' /\ age1 phi2 = Some phi2'.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
  intros.
(* Goal: @ex A (fun phi1 : A => @ex A (fun phi2 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@age1 A agA phi1) (@Some A phi1')) (@eq (option A) (@age1 A agA phi2) (@Some A phi2'))))) *)
  apply (unage_join2 _ H0 H).
Qed.

Lemma join_unage'  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
    forall phi1 phi1' phi2' phi3' : A,
      age1 phi1 = Some phi1' ->
      join phi1' phi2' phi3' ->
      exists phi2, exists phi3, join phi1 phi2 phi3 /\
        age1 phi2 = Some phi2' /\ age1 phi3 = Some phi3'.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
   intros. apply (unage_join _ H0 H).
Qed.

Lemma unageN'  {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall n (phi1 phi1' phi2' phi3' : A),
    ageN n phi1 = Some phi1' ->
    join phi1' phi2' phi3' ->
    exists phi2, exists phi3, join phi1 phi2 phi3 /\
      ageN n phi2 = Some phi2' /\ ageN n phi3 = Some phi3'.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
induction n; intros.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
inv H. exists phi2'; exists phi3'; split; auto.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
 unfold ageN in H. simpl in H.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
 revert H; case_eq (age1 phi1); intros.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
  specialize ( IHn a phi1' phi2' phi3' H1 H0).
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
  destruct IHn as [phi2 [phi3 [? [? ?]]]].
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
  destruct (join_unage' _ _ _ H H2) as [phi4 [phi5 [? [? ?]]]].
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
  exists phi4; exists phi5. split; auto.
(* Goal: @ex A (fun phic : A => @ex (list A) (fun l' : list A => and (@join A JA phin phia phic) (and (@eq (option (list A)) (@replace A (@cons A a l) (S n) phic) (@Some (list A) l')) (@list_join A JA phi l' phib)))) *)
 split; unfold ageN; simpl. rewrite H6; auto. rewrite H7; auto.
(* Goal: @ex A (fun phi2 : A => @ex A (fun phi3 : A => and (@join A JA phi1 phi2 phi3) (and (@eq (option A) (@ageN A agA (S n) phi2) (@Some A phi2')) (@eq (option A) (@ageN A agA (S n) phi3) (@Some A phi3'))))) *)
 inv H1.
Qed.


Hint Resolve @join_comparable @join_comparable'  @join_comparable'' @join_comparable'''
      @join_comparable2 @join_comparable2'  @list_join_comparable @list_join_comparable'
      @joins_comparable  @joins_comparable2  @join_sub_comparable  @join_sub_comparable2
      @eq_comparable  @eq_comparable2
  : comparable.

Hint Immediate @comparable_refl  @comparable_sym  : comparable.

Ltac Comp1 phi1 phi2 :=
   solve [ eauto 3 with comparable typeclass_instances |
  match goal with
  | H: comparable phi1 ?phi |- _ => Comp2 H phi1 phi phi2
  | H: comparable ?phi phi1 |- _ => Comp2 H phi1 phi phi2
  | H: join phi1 ?phia ?phib |- _ =>  Comp3 H phi1 phia phib phi2
  | H: join ?phia phi1 ?phib |- _ =>   Comp3 H phi1 phia phib phi2
  | H: join ?phia ?phib phi1 |- _ =>   Comp3 H phi1 phia phib phi2
  | H: joins phi1 ?phi |- _ =>  Comp2 H phi1 phi phi2
  | H: joins ?phi phi1 |- _ =>  Comp2 H phi1 phi phi2
  | H: join_sub phi1 ?phi |- _ => Comp2 H phi1 phi phi2
  | H: join_sub ?phi phi1 |- _ => Comp2 H phi1 phi phi2
  | H: list_join phi1 _ ?phi |- _ =>  Comp2 H phi1 phi phi2
  | H: list_join ?phi _ phi1 |- _ =>  Comp2 H phi1 phi phi2
  | H: phi1 = ?phi  |- _ => Comp2 H phi1 phi phi2
  | H: ?phi = phi1  |- _ => Comp2 H phi1 phi phi2
 end]
  with Comp2 H phi1 phi phi2 :=
            solve [apply comparable_trans with phi;
                         [eauto 3 with comparable  typeclass_instances |clear H; Comp1 phi phi2]
                   | clear H; Comp1 phi1 phi2]
  with Comp3 H phi1 phia phib phi2 :=
           solve [apply comparable_trans with phia;
                          [eauto 3 with comparable typeclass_instances |clear H; Comp1 phia phi2]
                  |apply comparable_trans with phib;
                          [eauto 3 with comparable  typeclass_instances | clear H; Comp1 phib phi2]
                   | clear H; Comp1 phi1 phi2].

Ltac Comp := match goal with
                | |- comparable ?phi1 ?phi2 => Comp1 phi1 phi2
                | |-  level ?phi1 = level ?phi2 => apply comparable_fashionR; Comp1 phi1 phi2
(*                | |- level _ = level _ => rewrite comparable_level; Comp *)
                end.


Definition not_any_younger {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A} (phi phi': A)  : Prop :=
     exists phi1, necR phi phi1 /\ comparable phi1 phi'.

Lemma comparable_not_any_younger {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A} :
    forall phi phi' : A , comparable phi phi' -> not_any_younger phi phi'.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
  intros.
(* Goal: @not_any_younger A JA PA SA agA AgeA phi phi' *)
  exists phi; split; auto; apply rt_refl.
Qed.

Lemma necR_not_any_younger {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall phi phi' : A, necR phi phi' -> not_any_younger phi phi'.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
Proof. intros; exists phi'; split; auto. apply comparable_refl. Qed.

Lemma not_any_younger_refl {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
 forall phi : A, not_any_younger phi phi.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
Proof. intros; exists phi; split; auto. apply comparable_refl. Qed.

Lemma not_any_younger_trans {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall phi1 phi2 phi3, not_any_younger phi1 phi2 -> not_any_younger phi2 phi3 ->
            not_any_younger phi1 phi3.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
intros.
(* Goal: @not_any_younger A JA PA SA agA AgeA phi1 phi3 *)
destruct H as [phi1' [? ?]].
(* Goal: @not_any_younger A JA PA SA agA AgeA phi1 phi3 *)
destruct H0 as [phi2' [? ?]].
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
generalize (comparable_common_unit H1); intros [e1 [? ?]].
(* Goal: @not_any_younger A JA PA SA agA AgeA phi1 phi3 *)
generalize (nec_join2 H4 H0); intros [a [b [? [? _]]]].
(* Goal: @not_any_younger A JA PA SA agA AgeA phi1 phi3 *)
generalize (nec_join H3 H6); intros [u [v [? [? _]]]].
(* Goal: @not_any_younger A JA PA SA agA AgeA phi1 phi3 *)
exists u.
(* Goal: and (@necR A agA phi1 u) (@comparable A JA SA u phi3) *)
split.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
econstructor 3; eauto.
(* Goal: @comparable A JA SA u phi3 *)
Comp.
Qed.

Lemma not_any_younger_None {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall phi phi', age1 phi = None -> not_any_younger phi phi' -> age1 phi' = None.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
intros.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
destruct H0 as [phi1 [? ?]].
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
revert phi' H1.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
induction H0; intros.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
unfold age in H0.
(* Goal: @eq A x y *)
(* Goal: @eq A x x *)
(* Goal: @eq A x z *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
inversion2 H H0.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
generalize (comparable_common_unit H1); intros [e1 [? ?]].
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
case_eq (age1 phi'); [intros w ? | intro]; auto.
(* Goal: @eq (option A) (@Some A w) (@None A) *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
elimtype False.
(* Goal: False *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
generalize (age1_join2 _ H2 H3); intros [a [b [? [? ?]]]].
(* Goal: False *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
generalize (age1_join _ H0 H5); intros [c [d [? [? ?]]]].
(* Goal: False *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
unfold age in H8; inversion2 H H8.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
assert (x=y).
(* Goal: @eq A x y *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
clear - H0_ H.
(* Goal: @eq A x y *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
induction H0_.
(* Goal: @eq A x y *)
(* Goal: @eq A x x *)
(* Goal: @eq A x z *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
 unfold age in *.
(* Goal: @eq A x y *)
(* Goal: @eq A x x *)
(* Goal: @eq A x z *)
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
inversion2 H H0.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
rewrite <- IHH0_2; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
rewrite <- IHH0_1; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
subst y.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
auto.
Qed.

Lemma nec_join3 {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}: forall {x x' y' z' : A},
       join x' y' z' ->
       necR x x' ->
       exists y,
         exists z,
           join x y z /\ necR y y' /\ necR z z'.
Proof.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
intros.
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
revert y' z' H.
(* Goal: forall (x x' y' z' : A) (_ : @join A JA x' y' z') (_ : @necR A agA x x'), @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
induction H0; intros.
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
destruct (unage_join _ H0 H) as [y0 [z0 [? [? ?]]]].
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
exists y0; exists z0; split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
split; constructor 1; auto.
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
exists y'; exists z'.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
split; auto.
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
rename z into x'.
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
rename y into x1.
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
destruct (IHclos_refl_trans2 _ _ H) as [x'' [y'' [? [? ?]]]].
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
destruct (IHclos_refl_trans1 _ _ H0) as [x0 [y0 [? [? ?]]]].
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA x y z) (and (@necR A agA y y') (@necR A agA z z')))) *)
exists x0; exists y0.
(* Goal: and (@join A JA x x0 y0) (and (@necR A agA x0 y') (@necR A agA y0 z')) *)
split; auto.
(* Goal: @eq (option A) (@age1 A agA phi') (@None A) *)
split; econstructor 3; eauto.
Qed.

