Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Logic.lib.Coqlib.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.lib.EnsemblesProperties.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.Complete.ContextProperty.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.RewriteClass.
Require Import Logic.PropositionalLogic.ProofTheory.ProofTheoryPatterns.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.ProofTheory.SeparationLogic.
Require Import Logic.SeparationLogic.ProofTheory.RewriteClass.
Require Import Logic.SeparationLogic.ProofTheory.DerivedRules.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.
Import SeparationLogicNotation.

Section ContextProperties.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {Gamma: ProofTheory L}.

Definition context_sepcon (Phi Psi: context): context :=
  fun z => exists x y, z = x * y /\ Phi |-- x /\ Psi |-- y.

Definition context_sepcon_included_l (Phi2 Psi: context): context -> Prop :=
  fun Phi1 => Included _ (context_sepcon Phi1 Phi2) Psi.

Definition context_sepcon_included_r (Phi1 Psi: context): context -> Prop :=
  fun Phi2 => Included _ (context_sepcon Phi1 Phi2) Psi.

Context {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {fwSC: FiniteWitnessedSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {AX: NormalAxiomatization L Gamma}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma}.

Lemma context_sepcon_derivable:
  forall (Phi Psi: context) z,
    context_sepcon Phi Psi |-- z ->
    exists x y, |-- x * y --> z /\ Phi |-- x /\ Psi |-- y.
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y : @expr L => and (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi y)))) *)
  rewrite derivable_provable in H.
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y : @expr L => and (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi y)))) *)
  destruct H as [xs [? ?]].
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  revert z H0; induction H; intros.
  + exists TT, TT.
(* Goal: and (@provable L Gamma (@impp L minL (@sepcon L sL (@andp L pL x x') (@andp L pL y y')) z)) (and (@derivable L Gamma Phi (@andp L pL x x')) (@derivable L Gamma Psi (@andp L pL y y'))) *)
    split; [| split].
    - apply aux_minimun_rule00; auto.
    - apply derivable_impp_refl.
    - apply derivable_impp_refl.
  + pose proof provable_multi_imp_arg_switch1 l x z.
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y : @expr L => and (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi y)))) *)
    pose proof modus_ponens _ _ H2 H1.
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y : @expr L => and (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi y)))) *)
    specialize (IHForall _ H3); clear H1 H2 H3.
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y : @expr L => and (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi y)))) *)
    destruct H as [x' [y' [? [? ?]]]]; subst x.
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y : @expr L => and (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi y)))) *)
    destruct IHForall as [x [y [? [? ?]]]].
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y : @expr L => and (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi y)))) *)
    exists (x && x'), (y && y').
(* Goal: and (@provable L Gamma (@impp L minL (@sepcon L sL (@andp L pL x x') (@andp L pL y y')) z)) (and (@derivable L Gamma Phi (@andp L pL x x')) (@derivable L Gamma Psi (@andp L pL y y'))) *)
    split; [| split].
    - clear l H0 H1 H2 H3 H4.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL (@andp L pL x x') (@andp L pL y y')) z) *)
      rewrite (provable_sepcon_andp_right (x && x') y y').
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL (@andp L pL x x') y) (@sepcon L sL (@andp L pL x x') y')) z) *)
      rewrite (provable_sepcon_andp_left x x' y).
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@andp L pL (@sepcon L sL x y) (@sepcon L sL x' y)) (@sepcon L sL (@andp L pL x x') y')) z) *)
      rewrite (provable_sepcon_andp_left x x' y').
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@andp L pL (@sepcon L sL x y) (@sepcon L sL x' y)) (@andp L pL (@sepcon L sL x y') (@sepcon L sL x' y'))) z) *)
      rewrite (andp_elim1 (x * y) _).
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@andp L pL (@sepcon L sL x y') (@sepcon L sL x' y'))) z) *)
      rewrite (andp_elim2 _ (x' * y')).
      rewrite <- impp_curry_uncurry.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
      auto.
    - apply deduction_andp_intros; auto.
    - apply deduction_andp_intros; auto.
Qed.

Lemma context_sepcon_consistent_rev_left:
  forall (Phi1 Phi2 Psi: context),
    Included _ (context_sepcon Phi1 Phi2) Psi ->
    consistent Psi ->
    consistent Phi1.
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
  rewrite consistent_spec in H0 |- *.
(* Goal: not (@derivable L Gamma Phi1 (@falsep L pL)) *)
  intro; apply H0; clear H0.
  rewrite <- (falsep_sepcon TT).
(* Goal: @derivable L Gamma Psi (@sepcon L sL z y) *)
  apply derivable_assum.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
  apply H; exists FF, TT; split; [| split]; auto.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL x x) *)
  apply derivable_impp_refl.
Qed.

Lemma context_sepcon_included_l_derivable_subset_preserved: forall Phi2 Psi,
  derivable_subset_preserved (context_sepcon_included_l Phi2 Psi).
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
(* Goal: @finite_captured (@expr L) (context_sepcon_included_l Phi2 Psi) *)
  unfold context_sepcon_included_l.
(* Goal: @derivable_subset_preserved L Gamma (fun Phi1 : @context L => Included (@expr L) (context_sepcon Phi1 Phi2) Psi) *)
  hnf; intros Phi1 Phi1' ? ?.
(* Goal: Included (@expr L) (context_sepcon Phi1 Phi2) Psi *)
  eapply Included_trans; [clear Psi H0 | exact H0].
(* Goal: Included (@expr L) (context_sepcon Phi Phi2) Psi *)
  unfold Included, Ensembles.In; intros z ?.
(* Goal: Psi z *)
  destruct H0 as [x [y [? [? ?]]]].
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
  exists x, y; split; [| split]; auto.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
  apply H; auto.
Qed.

Lemma context_sepcon_included_l_subset_preserved: forall Phi2 Psi,
  subset_preserved (context_sepcon_included_l Phi2 Psi).
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
(* Goal: @subset_preserved (@expr L) (context_sepcon_included_l Phi2 Psi) *)
  apply derivable_subset_preserved_subset_preserved.
(* Goal: @derivable_subset_preserved L Gamma (context_sepcon_included_l Phi2 Psi) *)
  apply context_sepcon_included_l_derivable_subset_preserved.
Qed.

Lemma context_sepcon_included_l_finite_captured: forall Phi2 Psi,
  finite_captured (context_sepcon_included_l Phi2 Psi).
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
(* Goal: @finite_captured (@expr L) (context_sepcon_included_l Phi2 Psi) *)
  unfold context_sepcon_included_l.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  hnf; intros.
(* Goal: Included (@expr L) (context_sepcon Phi Phi2) Psi *)
  unfold Included, Ensembles.In; intros z ?.
(* Goal: Psi z *)
  destruct H0 as [x [y [? [? ?]]]].
(* Goal: Psi z *)
  apply derivable_finite_witnessed in H1.
(* Goal: Psi z *)
  destruct H1 as [xs [? ?]].
(* Goal: Psi z *)
  specialize (H _ H1).
(* Goal: Psi z *)
  subst z.
(* Goal: Psi (@sepcon L sL x y) *)
  apply H; auto; unfold Ensembles.In.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
  exists x, y; split; [| split]; auto.
Qed.

Lemma context_sepcon_included_l_context_orp_captured: forall Phi2 Psi
      (DC: derivable_closed Psi)
      (OW: orp_witnessed Psi),
  context_orp_captured (context_sepcon_included_l Phi2 Psi).
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
(* Goal: @finite_captured (@expr L) (context_sepcon_included_l Phi2 Psi) *)
  unfold context_sepcon_included_l.
  hnf; intros Phi1 Phi1' ?.
  assert (forall z1 z2,
            context_sepcon Phi1 Phi2 z1  ->
            ~ Psi z1 ->
            context_sepcon Phi1' Phi2 z2 ->
            ~ Psi z2 ->
            False) as HH.
  Focus 2. {
    clear - HH; unfold Included, Ensembles.In.
    apply NNPP; intro.
    apply not_or_and in H; destruct H.
    apply not_all_ex_not in H.
    apply not_all_ex_not in H0.
    destruct H as [z1 ?], H0 as [z2 ?].
    specialize (HH z1 z2).
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    tauto.
  } Unfocus.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
  destruct H0 as [x1 [y1 [? [? ?]]]], H2 as [x2 [y2 [? [? ?]]]].
  subst z1 z2.
  assert (context_orp Phi1 Phi1' (x1 || x2));
  [| assert (context_sepcon (context_orp Phi1 Phi1') Phi2 ((x1 || x2) * (y1 && y2)));
     [| assert (Psi |-- (x1 * y1) || (x2 * y2))]].
  + exists x1, x2.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    split; [| split]; auto.
  + exists (x1 || x2), (y1 && y2).
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    split; [| split]; auto.
    - apply derivable_assum; auto.
    - apply deduction_andp_intros; auto.
  + apply H in H2.
    apply derivable_assum in H2.
    rewrite sepcon_orp_distr_l in H2.
    rewrite (andp_elim1 y1 y2) in H2 at 1.
    rewrite (andp_elim2 y1 y2) in H2 at 1.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    auto.
  + rewrite <- derivable_closed_element_derivable in H8 by auto.
    apply OW in H8.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    tauto.
Qed.

Lemma wand_deduction_theorem:
  forall (Phi: context) x y,
    context_sepcon Phi (Union _ empty_context (Singleton _ x)) |-- y <->
    Phi |-- x -* y.
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  split; intros.
  + apply context_sepcon_derivable in H.
(* Goal: @derivable L Gamma Phi (@wand L sL x y) *)
    destruct H as [x' [y' [? [? ?]]]].
    rewrite deduction_theorem, <- provable_derivable in H1.
    rewrite <- H1 in H.
(* Goal: @derivable L Gamma Phi (@wand L sL x y) *)
    apply wand_sepcon_adjoint in H.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    rewrite H in H0; auto.
  + rewrite <- (provable_wand_sepcon_modus_ponens1 x y).
(* Goal: @derivable L Gamma Psi (@sepcon L sL z y) *)
    apply derivable_assum.
    exists (x -* y), x.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    split; [| split]; auto.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) x)) x *)
    rewrite deduction_theorem.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL x x) *)
    apply derivable_impp_refl.
Qed.

Lemma context_sepcon_included_equiv: forall Phi Psi,
  derivable_closed Psi ->
  Same_set _ (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi).
Proof.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  intros.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  rewrite Same_set_spec; intros Phi'; split; intros.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  + hnf; intros.
(* Goal: Ensembles.In (@expr L) Psi x *)
    destruct H1 as [y [z [? [? ?]]]].
(* Goal: Ensembles.In (@expr L) Psi x *)
    subst x.
(* Goal: Ensembles.In (@expr L) Psi (@sepcon L sL y z) *)
    apply H.
    rewrite <- sepcon_comm.
(* Goal: @derivable L Gamma Psi (@sepcon L sL z y) *)
    apply derivable_assum.
(* Goal: Ensembles.In (@expr L) Psi (@sepcon L sL z y) *)
    apply H0.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    exists z, y; split; [| split]; auto.
(* Goal: forall (Phi Psi : @context L) (_ : @derivable_closed L Gamma Psi), Same_set (@context L) (context_sepcon_included_l Phi Psi) (context_sepcon_included_r Phi Psi) *)
  + hnf; intros.
(* Goal: Ensembles.In (@expr L) Psi x *)
    destruct H1 as [y [z [? [? ?]]]].
(* Goal: Ensembles.In (@expr L) Psi x *)
    subst x.
(* Goal: Ensembles.In (@expr L) Psi (@sepcon L sL y z) *)
    apply H.
    rewrite <- sepcon_comm.
(* Goal: @derivable L Gamma Psi (@sepcon L sL z y) *)
    apply derivable_assum.
(* Goal: Ensembles.In (@expr L) Psi (@sepcon L sL z y) *)
    apply H0.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@impp L minL (@sepcon L sL x' y') z)) *)
    exists z, y; split; [| split]; auto.
Qed.

End ContextProperties.
