Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.RelationClasses.
From ChargeCore.Logics Require Import ILogic ILEmbed.

Set Implicit Arguments.
Unset Strict Implicit.
Set Maximal Implicit Insertion.

Section BILogic.
  Definition BILogicType := Type.

  Context {A : BILogicType}.
  Context {HILOp: ILogicOps A}.

(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp (@sepSP A BILOp a b) c) *)
  Class BILogicOps (A : BILogicType) : Type := {
    empSP  : A;
    sepSP  : A -> A -> A;
    wandSP : A -> A -> A
  }.

(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp (@sepSP A BILOp a b) c) *)
  Class BILogic {BILOp: BILogicOps A} : Type := {
    bilil :> ILogic A;
    sepSPC1 P Q : sepSP P Q |-- sepSP Q P;
    sepSPA1 P Q R : sepSP (sepSP P Q) R |-- sepSP P (sepSP Q R);
    wandSepSPAdj P Q R : sepSP P Q |-- R <-> P |-- wandSP Q R;
    bilsep P Q R : P |-- Q -> sepSP P R |-- sepSP Q R;
    empSPR P : sepSP P empSP -|- P
  }.

End BILogic.

Arguments BILogic _ {BILOp HILOp} : rename.

Notation "a '**' b"  := (sepSP a b)
  (at level 58, right associativity).
Notation "a '-*' b"  := (wandSP a b)
  (at level 60, right associativity).

Section CoreInferenceRules.

  Context {A T : Type} `{HBIL: BILogic A}.

  Lemma wandSPAdj P Q C (HSep: C ** P |-- Q) : C |-- P -* Q.
  Proof.
(* Goal: @lentails A HILOp (@sepSP A BILOp C P) Q *)
    apply wandSepSPAdj; assumption.
  Qed.

  Lemma wandSPAdj' P Q C (HSep: P ** C |-- Q) : C |-- P -* Q.
  Proof.
(* Goal: @lentails A HILOp (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) (@wandSP A BILOp (@lexists A HILOp T P) Q) *)
    apply wandSepSPAdj. etransitivity; [apply sepSPC1|]. assumption.
  Qed.

  Lemma sepSPAdj P Q C (HWand: C |-- P -* Q) : C ** P |-- Q.
  Proof.
(* Goal: @lentails A HILOp (@sepSP A BILOp C P) Q *)
    apply wandSepSPAdj; assumption.
  Qed.

  Lemma sepSPAdj' P Q C (HWand: C |-- P -* Q) : P ** C |-- Q.
  Proof.
(* Goal: @lentails A HILOp (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) (@wandSP A BILOp (@lexists A HILOp T P) Q) *)
    etransitivity; [apply sepSPC1|]. apply wandSepSPAdj. assumption.
  Qed.

  Lemma sepSPC (P Q : A) : P ** Q -|- Q ** P.
  Proof.
(* Goal: @lequiv A HILOp (@sepSP A BILOp P Q) (@sepSP A BILOp Q P) *)
    split; apply sepSPC1.
  Qed.

  Lemma sepSPA2 (P Q R : A) : P ** (Q ** R) |-- (P ** Q) ** R.
  Proof.
(* Goal: @lentails A HILOp (@sepSP A BILOp p (@empSP A BILOp)) (@sepSP A BILOp p (@ltrue A HILOp)) *)
    rewrite sepSPC.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@sepSP A BILOp R P) Q) (@sepSP A BILOp (@sepSP A BILOp P Q) R) *)
    etransitivity; [apply sepSPA1|].
(* Goal: @lentails A HILOp (@sepSP A BILOp p (@empSP A BILOp)) (@sepSP A BILOp p (@ltrue A HILOp)) *)
    rewrite sepSPC.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@sepSP A BILOp R P) Q) (@sepSP A BILOp (@sepSP A BILOp P Q) R) *)
    etransitivity; [apply sepSPA1|].
(* Goal: @lentails A HILOp (@sepSP A BILOp p (@empSP A BILOp)) (@sepSP A BILOp p (@ltrue A HILOp)) *)
    rewrite sepSPC.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    reflexivity.
  Qed.

  Lemma sepSPA (P Q R : A) : (P ** Q) ** R -|- P ** (Q ** R).
  Proof.
(* Goal: @lequiv A HILOp (@sepSP A BILOp (@sepSP A BILOp P Q) R) (@sepSP A BILOp P (@sepSP A BILOp Q R)) *)
    split; [apply sepSPA1 | apply sepSPA2].
  Qed.

  Lemma wandSPI (P Q R : A) (HQ : P ** Q |-- R) : (P |-- Q -* R).
  Proof.
(* Goal: @lentails A HILOp C (@wandSP A BILOp P Q) *)
    apply wandSPAdj; assumption.
  Qed.

  Lemma wandSPE (P Q R S : A) (HQR: Q |-- S -* R) (HP : P |-- Q ** S) : P |-- R.
  Proof.
(* Goal: @lentails A HILOp P R *)
    apply sepSPAdj in HQR.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    rewrite <- HQR, HP. reflexivity.
  Qed.

  Lemma empSPL P : empSP ** P -|- P.
  Proof.
(* Goal: @lequiv A HILOp (@sepSP A BILOp (@empSP A BILOp) P) P *)
    rewrite sepSPC; apply empSPR.
  Qed.

  Lemma bilexistsscR1 (P : A) (f : T -> A):
    Exists x : T, P ** f x |-- P ** lexists f.
  Proof.
(* Goal: @lentails A HILOp (@lexists A HILOp T (fun x : T => @sepSP A BILOp (@lforall A HILOp T (fun x0 : T => @wandSP A BILOp (P x0) Q)) (P x))) Q *)
  	apply lexistsL; intro x.
(* Goal: @lentails A HILOp (@sepSP A BILOp p (@empSP A BILOp)) (@sepSP A BILOp p (@ltrue A HILOp)) *)
    rewrite sepSPC. etransitivity; [|rewrite <- sepSPC; reflexivity].
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    apply bilsep. eapply lexistsR; reflexivity.
  Qed.

  Lemma bilexistsscR2 (P : A) (f : T -> A):
    Exists x : T, f x ** P |-- lexists f ** P.
  Proof.
(* Goal: @lentails A HILOp (@lexists A HILOp T (fun x : T => @sepSP A BILOp (f x) P)) (@sepSP A BILOp (@lexists A HILOp T f) P) *)
    rewrite sepSPC, <- bilexistsscR1.
(* Goal: @lentails A HILOp (@lexists A HILOp T (fun x : T => @sepSP A BILOp P (f x))) (@lexists A HILOp T (fun x : T => @sepSP A BILOp (f x) P)) *)
    setoid_rewrite sepSPC at 1.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    reflexivity.
  Qed.

    Lemma bilexistsscL1 (P : A) (f : T -> A) :
    P ** lexists f |-- Exists x : T, P ** f x.
  Proof.
    rewrite sepSPC; rewrite wandSepSPAdj.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    apply lexistsL; intro x; erewrite <- wandSPAdj. reflexivity.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    eapply lexistsR; rewrite sepSPC; reflexivity.
  Qed.

  Lemma bilexistsscL2 (P : A) (f : T -> A) :
    lexists f ** P |-- Exists x : T, f x ** P.
  Proof.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@lexists A HILOp T f) P) (@lexists A HILOp T (fun x : T => @sepSP A BILOp (f x) P)) *)
    rewrite sepSPC, bilexistsscL1.
(* Goal: @lentails A HILOp (@lexists A HILOp T (fun x : T => @sepSP A BILOp P (f x))) (@lexists A HILOp T (fun x : T => @sepSP A BILOp (f x) P)) *)
    setoid_rewrite sepSPC at 1.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    reflexivity.
  Qed.

    Lemma bilexistssc (P : A) (Q : T -> A) :
    Exists x : T, P ** Q x -|- P ** lexists Q.
  Proof.
(* Goal: @lequiv A HILOp (@lexists A HILOp T (fun x : T => @sepSP A BILOp P (Q x))) (@sepSP A BILOp P (@lexists A HILOp T Q)) *)
    split; [apply bilexistsscR1 | apply bilexistsscL1].
  Qed.

  Lemma bilforallscR (P : A) (Q : T -> A) :
    P ** lforall Q |-- Forall x : T, P ** Q x.
  Proof.
(* Goal: @lentails A HILOp (@wandSP A BILOp (@lexists A HILOp T P) Q) (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) *)
    apply lforallR; intro x.
(* Goal: @lentails A HILOp (@sepSP A BILOp (f x) P) (@sepSP A BILOp P (@lexists A HILOp T f)) *)
    rewrite sepSPC; etransitivity; [|rewrite <- sepSPC; reflexivity].
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    apply bilsep. apply lforallL with x; reflexivity.
  Qed.

  Lemma bilandscDL (P Q R : A) : (P //\\ Q) ** R |-- (P ** R) //\\ (Q ** R).
  Proof.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@land A HILOp P Q) R) (@land A HILOp (@sepSP A BILOp P R) (@sepSP A BILOp Q R)) *)
  	apply landR.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
  	+ apply wandSepSPAdj; apply landL1; apply wandSepSPAdj; reflexivity.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
  	+ apply wandSepSPAdj; apply landL2; apply wandSepSPAdj; reflexivity.
  Qed.

  Lemma bilorscDL (P Q R : A) : (P \\// Q) ** R -|- (P ** R) \\// (Q ** R).
  Proof.
(* Goal: @lequiv A HILOp (@wandSP A BILOp (@lexists A HILOp T P) Q) (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) *)
  	split.
  	+ apply wandSepSPAdj; apply lorL; apply wandSepSPAdj;
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
  	  [apply lorR1 | apply lorR2]; reflexivity.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
  	+ apply lorL; apply bilsep; [apply lorR1 | apply lorR2]; reflexivity.
  Qed.

End CoreInferenceRules.

Section BILogicMorphisms.
  Context {A : BILogicType} `{BIL: BILogic A}.

  Global Instance sepSP_lentails_m:
    Proper (lentails ++> lentails ++> lentails) sepSP.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : A), A) (@respectful A (forall _ : A, A) (@lequiv A HILOp) (@respectful A A (@lequiv A HILOp) (@lequiv A HILOp))) (@wandSP A BILOp) *)
    intros P P' HP Q Q' HQ.
(* Goal: @lentails A HILOp (@sepSP A BILOp P Q) (@sepSP A BILOp P' Q') *)
    etransitivity; [eapply bilsep; exact HP|].
(* Goal: @lentails A HILOp (@sepSP A BILOp p (@empSP A BILOp)) (@sepSP A BILOp p (@ltrue A HILOp)) *)
    rewrite -> sepSPC.
(* Goal: @lentails A HILOp (@sepSP A BILOp Q P') (@sepSP A BILOp P' Q') *)
    etransitivity; [eapply bilsep; exact HQ|].
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    rewrite -> sepSPC. reflexivity.
  Qed.

  Global Instance sepSP_lequiv_m:
    Proper (lequiv ==> lequiv ==> lequiv) sepSP.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : A), A) (@respectful A (forall _ : A, A) (@lequiv A HILOp) (@respectful A A (@lequiv A HILOp) (@lequiv A HILOp))) (@wandSP A BILOp) *)
    intros P P' HP Q Q' HQ.
(* Goal: @lequiv A HILOp (@sepSP A BILOp P Q) (@sepSP A BILOp P' Q') *)
    split; apply sepSP_lentails_m; (apply HP || apply HQ).
  Qed.

  Global Instance wandSP_lentails_m:
    Proper (lentails --> lentails ++> lentails) wandSP.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : A), A) (@respectful A (forall _ : A, A) (@lequiv A HILOp) (@respectful A A (@lequiv A HILOp) (@lequiv A HILOp))) (@wandSP A BILOp) *)
    intros P P' HP Q Q' HQ. red in HP.
(* Goal: @lentails A HILOp (@wandSP A BILOp P Q) (@wandSP A BILOp P' Q') *)
    apply wandSPAdj. rewrite <- HQ, -> HP.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    apply sepSPAdj. reflexivity.
  Qed.

  Global Instance wandSP_lequiv_m:
    Proper (lequiv ==> lequiv ==> lequiv) wandSP.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : A), A) (@respectful A (forall _ : A, A) (@lequiv A HILOp) (@respectful A A (@lequiv A HILOp) (@lequiv A HILOp))) (@wandSP A BILOp) *)
    intros P P' HP Q Q' HQ.
(* Goal: @lequiv A HILOp (@wandSP A BILOp P Q) (@wandSP A BILOp P' Q') *)
    split; apply wandSP_lentails_m; (apply HP || apply HQ).
  Qed.

End BILogicMorphisms.

Section DerivedInferenceRules.

  Context {A : BILogicType} `{BILogic A}.

  Lemma sepSP_falseR P : P ** lfalse -|- lfalse.
  Proof.
(* Goal: @lequiv A HILOp (@sepSP A BILOp P (@lfalse A HILOp)) (@lfalse A HILOp) *)
    rewrite lfalse_is_exists, <- bilexistssc.
(* Goal: @lequiv A HILOp (@lexists A HILOp Empty_set (fun x : Empty_set => @sepSP A BILOp P (Empty_set_rect (fun _ : Empty_set => A) x))) (@lexists A HILOp Empty_set (fun x : Empty_set => Empty_set_rect (fun _ : Empty_set => A) x)) *)
    split; apply lexistsL; intro x; destruct x.
  Qed.

  Lemma sepSP_falseL P : lfalse ** P -|- lfalse.
  Proof.
(* Goal: @lequiv A HILOp (@sepSP A BILOp (@lfalse A HILOp) P) (@lfalse A HILOp) *)
    rewrite -> sepSPC; apply sepSP_falseR.
  Qed.

  Lemma scME (P Q R S : A) (HPR: P |-- R) (HQS: Q |-- S) :
    P ** Q |-- R ** S.
  Proof.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    rewrite HPR, HQS; reflexivity.
  Qed.

  Lemma wandSPL P Q CL CR (HP: CL |-- P) (HR: Q |-- CR) :
    (P -* Q) ** CL |-- CR.
  Proof.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
    rewrite <-HR, <-HP. apply sepSPAdj. reflexivity.
  Qed.


(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp (@sepSP A BILOp a b) c) *)
  Lemma siexistsE {T : Type} (P : T -> A) (Q : A) :
    lexists P -* Q -|- Forall x, (P x -* Q).
  Proof.
(* Goal: @lequiv A HILOp (@wandSP A BILOp (@lexists A HILOp T P) Q) (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) *)
    split.
(* Goal: @lentails A HILOp (@wandSP A BILOp (@lexists A HILOp T P) Q) (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) *)
	+ apply lforallR; intro x. apply wandSepSPAdj; eapply wandSPL; [|reflexivity].
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
	  apply lexistsR with x. reflexivity.
(* Goal: @lentails A HILOp (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) (@wandSP A BILOp (@lexists A HILOp T P) Q) *)
	+ apply wandSepSPAdj. rewrite bilexistsscL1. apply lexistsL; intro x.
(* Goal: @lentails A HILOp (@sepSP A BILOp p (@empSP A BILOp)) (@sepSP A BILOp p (@ltrue A HILOp)) *)
	  rewrite sepSPC, bilforallscR. apply lforallL with x. rewrite sepSPC.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
	  apply wandSPL; reflexivity.
  Qed.

  Lemma septrue : forall p, p |-- p ** ltrue.
  Proof.
(* Goal: forall p : A, @lentails A HILOp p (@sepSP A BILOp p (@ltrue A HILOp)) *)
    intros. rewrite <- empSPR at 1.
(* Goal: @lentails A HILOp (@sepSP A BILOp p (@empSP A BILOp)) (@sepSP A BILOp p (@ltrue A HILOp)) *)
    rewrite sepSPC. rewrite (sepSPC p).
(* Goal: @lentails A HILOp (@sepSP A BILOp (@empSP A BILOp) p) (@sepSP A BILOp (@ltrue A HILOp) p) *)
    apply bilsep. apply ltrueR.
  Qed.

  Lemma wand_curry : forall a b c, (a ** b) -* c -|- a -* (b -* c).
  Proof.
(* Goal: @lequiv A HILOp (@wandSP A BILOp (@lexists A HILOp T P) Q) (@lforall A HILOp T (fun x : T => @wandSP A BILOp (P x) Q)) *)
    intros; split.
(* Goal: @lentails A HILOp (@wandSP A BILOp P Q) (@wandSP A BILOp P' Q') *)
    { eapply wandSPAdj.
(* Goal: @lentails A HILOp (@wandSP A BILOp P Q) (@wandSP A BILOp P' Q') *)
      eapply wandSPAdj.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@sepSP A BILOp (@wandSP A BILOp (@sepSP A BILOp a b) c) a) b) c *)
      rewrite sepSPA.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@wandSP A BILOp CL Q) CL) Q *)
      eapply sepSPAdj.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
      reflexivity. }
(* Goal: @lentails A HILOp (@wandSP A BILOp P Q) (@wandSP A BILOp P' Q') *)
    { eapply wandSPAdj.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@sepSP A BILOp a b)) c *)
      rewrite <- sepSPA.
(* Goal: @lentails A HILOp (@sepSP A BILOp (@wandSP A BILOp CL Q) CL) Q *)
      eapply sepSPAdj.
(* Goal: @lentails A HILOp (@wandSP A BILOp a (@wandSP A BILOp b c)) (@wandSP A BILOp a (@wandSP A BILOp b c)) *)
      eapply sepSPAdj. reflexivity. }
  Qed.

End DerivedInferenceRules.