(*
 * Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

Require Import VST.msl.base.
Require Import VST.msl.sepalg.

Definition constructive_join_sub {A} {JOIN: Join A} (w1 w3: A) := {w2 | join w1 w2 w3}.

Lemma cjoin_sub_join_sub{A} {JOIN: Join A}:
    forall {w1 w3}, constructive_join_sub w1 w3 -> join_sub w1 w3.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @join_sub A JOIN w1 w3 *)
destruct X as [w2 ?]; exists w2; auto.
Qed.

Lemma cjoin_sub_irr {A} `{Perm_alg A}{CA: Canc_alg A}:
    forall {w1 w3: A} (j1 j2: constructive_join_sub w1 w3), proj1_sig j1 = proj1_sig j2.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @eq A (@proj1_sig A (fun w2 : A => @join A J w1 w2 w3) j1) (@proj1_sig A (fun w2 : A => @join A J w1 w2 w3) j2) *)
destruct j1 as [w2 ?].
(* Goal: @eq A (@proj1_sig A (fun w2 : A => @join A J w1 w2 w3) (@exist A (fun w2 : A => @join A J w1 w2 w3) w2 j)) (@proj1_sig A (fun w2 : A => @join A J w1 w2 w3) j2) *)
destruct j2 as [w2' ?].
(* Goal: @eq A (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) (@exist A (fun w3 : A => @join A J w1 w2 w3) w3 j)) (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) (@exist A (fun w3 : A => @join A J w1 w2 w3) w3' j0)) *)
simpl.
(* Goal: @eq A w2 w2' *)
apply (join_canc (join_comm j) (join_comm j0)).
Qed.

Lemma cjoin_sub_trans {A} `{Perm_alg A}: forall a b c,
          constructive_join_sub a b -> constructive_join_sub b c -> constructive_join_sub a c.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @constructive_join_sub A J a c *)
destruct X as [u ?H].
(* Goal: @constructive_join_sub A J a c *)
destruct X0 as [v ?H].
(* Goal: @constructive_join_sub A J a c *)
destruct (join_assoc H0 H1) as [f [? ?]].
(* Goal: @constructive_join_sub A J a c *)
exists f; auto.
Qed.


Lemma constructive_join_sub_refl {A} `{Perm_alg A}{SA: Sep_alg A}: forall x, constructive_join_sub x x.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @constructive_join_sub A J x x *)
destruct (join_ex_units x).
(* Goal: @constructive_join_sub A J x x *)
exists x0. apply join_comm; apply u.
Qed.

Hint Resolve @constructive_join_sub_refl.
Definition constructive_joins {A}  {JOIN: Join A} (w1 w2 : A) := {w3 | join w1 w2 w3}.

Lemma cjoins_joins {A}  {JOIN: Join A}: forall {w1 w2}, constructive_joins w1 w2 -> joins w1 w2.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @joins A JOIN w1 w2 *)
destruct X as [w3 ?]; exists w3; auto.
Qed.

Lemma cjoins_irr {A} `{Perm_alg A}: forall {w1 w2: A}
    (j1 j2: constructive_joins w1 w2), proj1_sig j1 = proj1_sig j2.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @eq A (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) j1) (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) j2) *)
destruct j1 as [w3 ?].
(* Goal: @eq A (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) (@exist A (fun w3 : A => @join A J w1 w2 w3) w3 j)) (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) j2) *)
destruct j2 as [w3' ?].
(* Goal: @eq A (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) (@exist A (fun w3 : A => @join A J w1 w2 w3) w3 j)) (@proj1_sig A (fun w3 : A => @join A J w1 w2 w3) (@exist A (fun w3 : A => @join A J w1 w2 w3) w3' j0)) *)
simpl.
apply  (join_eq j j0).
Qed.

Lemma constructive_joins_sym {A} `{Perm_alg A}: forall a b,
      constructive_joins a b = constructive_joins b a.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @eq Type (@constructive_joins A J a b) (@constructive_joins A J b a) *)
unfold constructive_joins.
(* Goal: @eq Type (@sig A (fun w3 : A => @join A J a b w3)) (@sig A (fun w3 : A => @join A J b a w3)) *)
f_equal.
(* Goal: @eq (forall _ : A, Prop) (fun w3 : A => @join A J a b w3) (fun w3 : A => @join A J b a w3) *)
extensionality w3.
(* Goal: @eq Prop (@join A J a b w3) (@join A J b a w3) *)
apply prop_ext; split; auto.
Qed.

Definition same_constructive_silhouette {A} {JOIN: Join A} (a b: A) :=
    forall c, (constructive_joins c a -> constructive_joins c b) *
                 (constructive_joins c b -> constructive_joins c a).


  Definition sub_constructive_silhouette {A} {JOIN: Join A}  (a b: A) :=
    forall c, constructive_joins c b -> constructive_joins c a.

  Lemma sub_constructive_silhouette_refl {A} {JOIN: Join A} : forall a, sub_constructive_silhouette a a.
  Proof. unfold sub_constructive_silhouette; intuition. Qed.

  Lemma sub_constructive_silhouette_trans {A} {JOIN: Join A} : forall a b c,
    sub_constructive_silhouette a b -> sub_constructive_silhouette b c -> sub_constructive_silhouette a c.
  Proof. unfold sub_constructive_silhouette; intuition. Qed.

  Lemma same_constructive_silhouette_refl {A} {JOIN: Join A} : forall a, same_constructive_silhouette a a.
  Proof. unfold same_constructive_silhouette; intuition. Qed.

  Lemma same_constructive_silhouette_sym {A} {JOIN: Join A}: forall a b,
    same_constructive_silhouette a b -> same_constructive_silhouette b a.
  Proof. unfold same_constructive_silhouette; intuition; destruct (X c); auto. Qed.

  Lemma same_constructive_silhouette_trans {A} {JOIN: Join A}: forall a b c,
    same_constructive_silhouette a b -> same_constructive_silhouette b c -> same_constructive_silhouette a c.
 Proof. unfold same_constructive_silhouette; intuition;
             destruct (X c0); destruct (X0 c0);   auto. Qed.

  Lemma same_constructive_silhouette_sub1{A} {JOIN: Join A}: forall a b,
    same_constructive_silhouette a b -> sub_constructive_silhouette a b.
  Proof. unfold same_constructive_silhouette, sub_constructive_silhouette; intuition; destruct (X c); auto. Qed.

  Lemma same_constructive_silhouette_sub2 {A} {JOIN: Join A}: forall a b,
     same_constructive_silhouette a b -> sub_constructive_silhouette b a.
  Proof. unfold same_constructive_silhouette, sub_constructive_silhouette; intuition; destruct (X c); auto. Qed.


  Lemma sub_same_constructive_silhouette {A} {JOIN: Join A}:
    forall a b, sub_constructive_silhouette a b -> sub_constructive_silhouette b a -> same_constructive_silhouette a b.
  Proof. unfold same_constructive_silhouette, sub_constructive_silhouette; intuition; destruct (H0 c); auto. Qed.

  Lemma same_constructive_silhouette_join {A} `{HA: Perm_alg A}:
    forall phi phi' phiy phiz phiz',
      same_constructive_silhouette phi phi' ->
      join phi phiy phiz ->
      join phi' phiy phiz' ->
      same_constructive_silhouette phiz phiz'.
  Proof.
(* Goal: forall (phi phi' phiy phiz phiz' : A) (_ : @same_constructive_silhouette A J phi phi') (_ : @join A J phi phiy phiz) (_ : @join A J phi' phiy phiz'), @same_constructive_silhouette A J phiz phiz' *)
    intros * H ? ?.
(* Goal: @same_constructive_silhouette A J phiz phiz' *)
    intro phiu.
(* Goal: prod (forall _ : @constructive_joins A J phiu phiz, @constructive_joins A J phiu phiz') (forall _ : @constructive_joins A J phiu phiz', @constructive_joins A J phiu phiz) *)
    split; intros [phix ?H].
(* Goal: @constructive_joins A J phiu phiz' *)
(* Goal: @constructive_joins A J phiu phiz *)
    destruct (join_assoc H0 (join_comm H2)) as [phif [? ?]].
(* Goal: @constructive_joins A J phiu phiz *)
    specialize (H phif).
(* Goal: @constructive_joins A J phiu phiz *)
    destruct H as [?H ?H].
(* Goal: @constructive_joins A J phiu phiz' *)
(* Goal: @constructive_joins A J phiu phiz *)
    assert (H6: constructive_joins phi phif) by (econstructor; eauto).
(* Goal: @constructive_joins A J phiu phiz' *)
(* Goal: @constructive_joins A J phiu phiz *)
    spec H. rewrite constructive_joins_sym.  auto.
(* Goal: @constructive_joins A J phiu phiz' *)
(* Goal: @constructive_joins A J phiu phiz *)
    clear H5 H6.
(* Goal: @constructive_joins A J phiu phiz' *)
(* Goal: @constructive_joins A J phiu phiz *)
    destruct H as [phix' ?H].
(* Goal: @constructive_joins A J phiu phiz *)
    destruct (join_assoc (join_comm H3) H) as [phig [? ?]].
(* Goal: @constructive_joins A J phiu phiz' *)
(* Goal: @constructive_joins A J phiu phiz *)
    generalize (join_eq H1 (join_comm H5)); intro. rewrite <- H7 in *; clear H7 phig.
(* Goal: @constructive_joins A J phiu phiz *)
    clear H5.
(* Goal: @constructive_joins A J phiu phiz *)
    exists phix'.
(* Goal: @join A J phiu phiz phix' *)
    auto.
(* Goal: @constructive_joins A J phiu phiz *)
    destruct (join_assoc H1 (join_comm H2)) as [phif [? ?]].
(* Goal: @constructive_joins A J phiu phiz *)
    specialize (H phif).
(* Goal: @constructive_joins A J phiu phiz *)
    destruct H as [?H ?H].
(* Goal: @constructive_joins A J phiu phiz *)
    assert (H6: constructive_joins phi' phif) by (econstructor; eauto).
(* Goal: @constructive_joins A J phif phi' *)
(* Goal: @constructive_joins A J phiu phiz *)
    spec H5. rewrite constructive_joins_sym.  auto.
(* Goal: @constructive_joins A J phiu phiz *)
    clear H H6.
(* Goal: @constructive_joins A J phiu phiz *)
    destruct H5 as [phix' ?H].
(* Goal: @constructive_joins A J phiu phiz *)
    destruct (join_assoc (join_comm H3) H) as [phig [? ?]].
(* Goal: @constructive_joins A J phiu phiz *)
    generalize (join_eq H0 (join_comm H5)); intro. rewrite <- H7 in *; clear H7  phig.
(* Goal: @constructive_joins A J phiu phiz *)
    clear H5.
(* Goal: @constructive_joins A J phiu phiz *)
    exists phix'.
(* Goal: @join A J phiu phiz phix' *)
    auto.
  Qed.

Lemma constructive_join_sub_joins_trans {A} {JA: Join A}{PA: Perm_alg A}: forall {a b c},
  constructive_join_sub a c -> constructive_joins c b -> constructive_joins a b.
Proof.
(* Goal: forall (a b c : A) (_ : @constructive_join_sub A JA a c) (_ : @constructive_joins A JA c b), @constructive_joins A JA a b *)
intros.
(* Goal: @constructive_joins A JA a b *)
destruct X as [wx X].
(* Goal: @constructive_joins A JA a b *)
destruct X0 as [wy X0].
(* Goal: @constructive_joins A JA a b *)
destruct (join_assoc (join_comm X) X0) as [wf [? ?]].
(* Goal: @join A J phiu phiz phix' *)
econstructor; eauto.
Qed.

Lemma join_constructive_join_sub1 {A} {JA: Join A}{PA: Perm_alg A}: forall {a b c},
  join a b c -> constructive_join_sub a c.
Proof. intros; exists b; auto. Qed.

Lemma join_constructive_join_sub2 {A} {JA: Join A}{PA: Perm_alg A}: forall {a b c},
  join a b c -> constructive_join_sub b c.
Proof. intros; exists a; auto. Qed.

Lemma join_constructive_joins {A} {JA: Join A}{PA: Perm_alg A}: forall {a b c},
  join a b c -> constructive_joins a b.
Proof. intros; exists c; auto. Qed.
