Require Import RelationClasses Setoid Morphisms.
From ChargeCore.Logics Require Import ILogic ILInsts BILInsts BILogic Pure.
From ChargeCore.SepAlg Require Import SepAlg.

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

Section IBILogicSect.
  Context {A : Type} {ILOps : ILogicOps A} {BIOps: BILogicOps A}.
  Context {BIL : BILogic A}.

  Class IBILogic := {
    ibil_bil :> BILogic A;
    emp_trueE : |-- empSP
  }.

End IBILogicSect.

Arguments IBILogic _ {ILOps BIOps} : rename.

Section IBILogicProperties.

  Context {A : Type} `{HIBI: IBILogic A}.

  Lemma sep_forget (p q : A) : p ** q |-- p.
  Proof.
(* Goal: @lentails A ILOps (@sepSP A BIOps p q) p *)
    rewrite <- empSPR, sepSPA.
(* Goal: @lentails A ILOps (@sepSP A BIOps p (@sepSP A BIOps q (@empSP A BIOps))) p *)
    rewrite ltrueR with (C := q ** empSP).
(* Goal: @lentails A ILOps (@sepSP A BIOps p (@ltrue A ILOps)) p *)
    rewrite emp_trueE, empSPR.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
    reflexivity.
  Qed.

  Lemma ibilsepand (p q : A) : p ** q |-- p //\\ q.
  Proof.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
  	apply landR; [|rewrite sepSPC]; apply sep_forget; reflexivity.
  Qed.

End IBILogicProperties.

Section IBISepAlg.
  Context {A} `{sa : SepAlg A}.
  Context {B} `{IL: ILogic B}.

  Program Instance SAIBIOps: BILogicOps (ILPreFrm subheap B) := {
    empSP := mkILPreFrm (fun x => ltrue) _;
    sepSP P Q := mkILPreFrm (fun x => Exists x1, Exists x2, Exists H : sa_mul x1 x2 x,
                                                (ILPreFrm_pred P) x1 //\\ (ILPreFrm_pred Q) x2) _;
    wandSP P Q := mkILPreFrm (fun x => Forall x1, Forall x2, Forall H : sa_mul x x1 x2,
                                                 (ILPreFrm_pred P) x1 -->> (ILPreFrm_pred Q) x2) _
  }.
  Next Obligation.
(* Goal: @lentails B ILOps (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ltrue B ILOps))))) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) *)
    apply lexistsL; intro x1; apply lexistsL; intro x2; apply lexistsL; intro H1.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 t') (fun _ : @sa_mul A SAOps x1 x2 t' => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) *)
    unfold subheap in H.
(* Goal: @lentails B ILOps (@lforall B ILOps A (fun x1 : A => @lforall B ILOps A (fun x2 : A => @lforall B ILOps (@sa_mul A SAOps t x1 x2) (fun _ : @sa_mul A SAOps t x1 x2 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) *)
    destruct H as [t'' H].
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 t') (fun _ : @sa_mul A SAOps x1 x2 t' => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) *)
    destruct (sa_mulA H1 H) as [ac [H2 H3]].
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 t') (fun _ : @sa_mul A SAOps x1 x2 t' => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) *)
    apply lexistsR with x1; apply lexistsR with ac. apply lexistsR. assumption. apply landR.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
    + apply landL1; reflexivity.
    + apply landL2; apply ILPreFrm_closed; simpl.
(* Goal: @sa_mul A SAOps x1 x2 x *)
      exists t''; assumption.
  Qed.
  Next Obligation.
(* Goal: @lentails B ILOps (@lforall B ILOps A (fun x1 : A => @lforall B ILOps A (fun x2 : A => @lforall B ILOps (@sa_mul A SAOps t x1 x2) (fun _ : @sa_mul A SAOps t x1 x2 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) (@lforall B ILOps A (fun x1 : A => @lforall B ILOps A (fun x2 : A => @lforall B ILOps (@sa_mul A SAOps t' x1 x2) (fun _ : @sa_mul A SAOps t' x1 x2 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) *)
    apply lforallR; intro x1; apply lforallR; intro x2; apply lforallR; intro H1.
(* Goal: @lentails B ILOps (@lforall B ILOps A (fun x1 : A => @lforall B ILOps A (fun x2 : A => @lforall B ILOps (@sa_mul A SAOps t x1 x2) (fun _ : @sa_mul A SAOps t x1 x2 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) *)
    destruct H as [t'' H].
(* Goal: @lentails B ILOps (@lforall B ILOps A (fun x1 : A => @lforall B ILOps A (fun x2 : A => @lforall B ILOps (@sa_mul A SAOps t x1 x2) (fun _ : @sa_mul A SAOps t x1 x2 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) *)
    destruct (sa_mulA H H1) as [ac [H2 H3]].
(* Goal: @lentails B ILOps (@lforall B ILOps A (fun x1 : A => @lforall B ILOps A (fun x2 : A => @lforall B ILOps (@sa_mul A SAOps t x1 x2) (fun _ : @sa_mul A SAOps t x1 x2 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2))))) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) *)
    apply lforallL with ac; apply lforallL with x2. apply lforallL; [assumption|].
(* Goal: @lentails B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
    apply limplAdj. apply limplL.
(* Goal: @sa_mul A SAOps x1 x2 x *)
    apply ILPreFrm_closed. exists t''. eapply sa_mulC. assumption.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
    apply landL1. reflexivity.
  Qed.

  Local Existing Instance ILPre_Ops.
  Local Existing Instance ILPre_ILogic.
  Local Transparent ILPre_Ops.

  Definition SAIBILogic_aux : BILogic (ILPreFrm subheap B).
  Proof.
(* Goal: @IBILogic ((fun x y : Type => forall _ : x, y) T A) (@ILFun_Ops T A ILOps) (@BILFun_Ops T A BIOps) *)
    split.
    + apply _.
    + intros P Q x; simpl.
(* Goal: @lentails B ILOps (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ltrue B ILOps))))) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) *)
      apply lexistsL; intro x1; apply lexistsL; intro x2; apply lexistsL; intro H1.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x2))))) *)
      apply lexistsR with x2; apply lexistsR with x1.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@lexists B ILOps (@sa_mul A SAOps x2 x1 x) (fun _ : @sa_mul A SAOps x2 x1 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1))) *)
      apply lexistsR; [apply sa_mulC; assumption | apply landC].
    + intros P Q R x; simpl.
(* Goal: @lentails B ILOps (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2))))) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2))))) *)
      apply lexistsL; intro x1; apply lexistsL; intro x2; apply lexistsL; intro Hx.
(* Goal: @lentails B ILOps (@land B ILOps (@lexists B ILOps A (fun x2 : A => @lexists B ILOps A (fun x3 : A => @lexists B ILOps (@sa_mul A SAOps x2 x3 x1) (fun _ : @sa_mul A SAOps x2 x3 x1 => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x2) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x3))))) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@lexists B ILOps A (fun x3 : A => @lexists B ILOps A (fun x4 : A => @lexists B ILOps (@sa_mul A SAOps x3 x4 x2) (fun _ : @sa_mul A SAOps x3 x4 x2 => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x3) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x4))))))))) *)
      repeat setoid_rewrite landexistsD1.
(* Goal: @lentails B ILOps (@lexists B ILOps A (fun a : A => @lexists B ILOps A (fun a0 : A => @lexists B ILOps (@sa_mul A SAOps a a0 x1) (fun _ : @sa_mul A SAOps a a0 x1 => @land B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P a) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q a0)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2))))) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@lexists B ILOps A (fun x3 : A => @lexists B ILOps A (fun x4 : A => @lexists B ILOps (@sa_mul A SAOps x3 x4 x2) (fun _ : @sa_mul A SAOps x3 x4 x2 => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x3) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x4))))))))) *)
      apply lexistsL; intro x3; apply lexistsL; intro x4; apply lexistsL; intro Hx1.
(* Goal: @lentails B ILOps (@land B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x3) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x4)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@lexists B ILOps A (fun x3 : A => @lexists B ILOps A (fun x4 : A => @lexists B ILOps (@sa_mul A SAOps x3 x4 x2) (fun _ : @sa_mul A SAOps x3 x4 x2 => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x3) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x4))))))))) *)
      apply lexistsR with x3.
(* Goal: @lentails B ILOps (@land B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x3) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x4)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x3 x2 x) (fun _ : @sa_mul A SAOps x3 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x3) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x3 : A => @lexists B ILOps (@sa_mul A SAOps x1 x3 x2) (fun _ : @sa_mul A SAOps x1 x3 x2 => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x3)))))))) *)
      destruct (sa_mulA Hx1 Hx) as [x5 [Hx2 Hx5]].
(* Goal: @lentails B ILOps (@land B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x3) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x4)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x3 x2 x) (fun _ : @sa_mul A SAOps x3 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x3) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x3 : A => @lexists B ILOps (@sa_mul A SAOps x1 x3 x2) (fun _ : @sa_mul A SAOps x1 x3 x2 => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x3)))))))) *)
      apply lexistsR with x5; apply lexistsR with Hx5.
(* Goal: @lentails B ILOps (@land B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x3) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x4)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x3) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x5) (fun _ : @sa_mul A SAOps x1 x2 x5 => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)))))) *)
      rewrite landA; apply landR; [apply landL1; reflexivity | apply landL2].
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
      apply lexistsR with x4. apply lexistsR with x2; apply lexistsR with Hx2. reflexivity.
    + intros P Q R; split; intros H x; simpl.
      - apply lforallR; intro x1; apply lforallR; intro x2; apply lforallR; intro Hx1.
(* Goal: @lentails B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
        apply limplAdj.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2) *)
        specialize (H x2); simpl in H.
        rewrite <- H.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
        apply lexistsR with x; apply lexistsR with x1; apply lexistsR with Hx1. reflexivity.
(* Goal: @lentails B ILOps (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2))))) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2))))) *)
      - apply lexistsL; intro x1; apply lexistsL; intro x2; apply lexistsL; intro Hx.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x) *)
        specialize (H x1); simpl in H.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x) *)
        setoid_rewrite H.
(* Goal: @lentails B ILOps (@land B ILOps (@lforall B ILOps A (fun x2 : A => @lforall B ILOps A (fun x3 : A => @lforall B ILOps (@sa_mul A SAOps x1 x2 x3) (fun _ : @sa_mul A SAOps x1 x2 x3 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x3))))) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x) *)
        apply landAdj.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
        apply lforallL with x2; apply lforallL with x; apply lforallL with Hx; reflexivity.
    + intros P Q R H x; simpl.
(* Goal: @lentails B ILOps (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2))))) (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2))))) *)
      apply lexistsL; intro x1; apply lexistsL; intro x2; apply lexistsL; intro Hx.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x) *)
      apply lexistsR with x1; apply lexistsR with x2; apply lexistsR with Hx; specialize (H x1); setoid_rewrite H.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
      reflexivity.
    + intros P; split; intros x; simpl.
(* Goal: @lentails B ILOps (@lexists B ILOps A (fun x1 : A => @lexists B ILOps A (fun x2 : A => @lexists B ILOps (@sa_mul A SAOps x1 x2 x) (fun _ : @sa_mul A SAOps x1 x2 x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ltrue B ILOps))))) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) *)
      - apply lexistsL; intro x1; apply lexistsL; intro x2; apply lexistsL; intro H1. apply landL1.
(* Goal: @lentails B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) *)
        apply ILPreFrm_closed; simpl.
(* Goal: @sa_mul A SAOps x1 x2 x *)
        exists x2. assumption.
      - destruct (sa_unit_ex x) as [u [H1 H2]]. apply lexistsR with x; apply lexistsR with u.
(* Goal: @lentails B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@lexists B ILOps (@sa_mul A SAOps x u x) (fun _ : @sa_mul A SAOps x u x => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@ltrue B ILOps))) *)
        apply lexistsR with H2. apply landR; [reflexivity | apply ltrueR].
  Qed.

  Local Existing Instance SAIBILogic_aux.

  Definition SAIBILogic : IBILogic (ILPreFrm subheap B).
  Proof.
(* Goal: @IBILogic ((fun x y : Type => forall _ : x, y) T A) (@ILFun_Ops T A ILOps) (@BILFun_Ops T A BIOps) *)
    split.
    + apply _.
    + simpl; intros _. apply ltrueR.
  Qed.

  Instance pureop_pure_ibi_sepalg : PureOp _ := {
    pure := fun (P : ILPreFrm subheap B) => forall h h', (ILPreFrm_pred P) h |-- (ILPreFrm_pred P) h'
  }.

  Instance pure_ibi_sepalg : Pure pureop_pure_ibi_sepalg.
  Proof.
    constructor.
    { intros.
      unfold pure in H; simpl in H; repeat split; intros;
      unfold pure in *; simpl in *; intros h; simpl.
      * destruct (sa_unit_ex h) as [u [H1 H2]].
        apply lexistsR with u. apply lexistsR with h.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@lexists B ILOps (@sa_mul A SAOps x1 ac t') (fun _ : @sa_mul A SAOps x1 ac t' => @land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q ac))) *)
        eapply lexistsR. apply sa_mulC; apply H2.
        apply landR; [apply landL1; apply H| apply landL2; reflexivity].
      * apply lexistsL; intros x1.
        apply lexistsL; intros x2.
        apply lexistsL; intros Hx.
        apply landR; [apply landL1; apply H | apply landL2; apply H0].
      * apply lexistsL; intros x1; apply lexistsL; intro x2; apply lexistsL; intros Hx.
        rewrite landA. apply landR; [apply landL1; apply H|].
        apply lexistsR with x1; apply lexistsR with x2; apply lexistsR with Hx.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
        apply landL2. reflexivity.
(* Goal: @lentails B ILOps (@land B ILOps (@lforall B ILOps A (fun x2 : A => @lforall B ILOps A (fun x3 : A => @lforall B ILOps (@sa_mul A SAOps x1 x2 x3) (fun _ : @sa_mul A SAOps x1 x2 x3 => @limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x3))))) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x2)) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x) *)
      * rewrite landC. apply landAdj.
        apply lexistsL; intros x1; apply lexistsL; intro x2; apply lexistsL; intros Hx.
(* Goal: @lentails B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
        apply limplAdj.
        apply lexistsR with x1. apply lexistsR with x2. apply lexistsR with Hx.
        rewrite landC, landA.
        apply landR; [apply landL1; apply H | apply landL2; reflexivity].
      * apply lforallR; intro x1; apply lforallR; intro Hx.
        destruct Hx as [x2 Hx].
        apply lforallL with x2; apply lforallL with x1. apply lforallL.
(* Goal: @sa_mul A SAOps x1 x2 x *)
        - assumption.
(* Goal: @lentails B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
        - apply limplAdj. apply limplL; [apply H | apply landL1; reflexivity].
      * apply lforallR; intro x1; apply lforallR; intro x2; apply lforallR; intro Hx.
        apply lforallL with h. apply lforallL; [reflexivity|].
(* Goal: @lentails B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps P x) (@limpl B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
        apply limplAdj. apply limplL; [apply H| apply landL1; apply H0]. }
    { unfold pure; simpl. do 2 red; intros.
      red in H. simpl in H.
      split; intro. intros.
      destruct H.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
      rewrite H1. rewrite H0. rewrite H. reflexivity.
      intros. destruct H.
(* Goal: @lentails B ILOps (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) (@land B ILOps (@ILPreFrm_pred A (@subheap A SAOps) B ILOps Q x1) (@ILPreFrm_pred A (@subheap A SAOps) B ILOps R x2)) *)
      rewrite H. rewrite H0. rewrite H1. reflexivity. }
  Qed.

End IBISepAlg.

Section IBILPre.
  Context T (ord: relation T) {ord_Pre: PreOrder ord}.
  Context {A : Type} `{HBI: IBILogic A}.
  Context {BIL : BILogic A} {IL : ILogic A}.

  Local Existing Instance ILPre_Ops.
  Local Existing Instance ILPre_ILogic.
  Local Existing Instance BILPre_Ops.

  Local Transparent ILPre_Ops.

  Definition IBILPreLogic : IBILogic (ILPreFrm ord A).
  Proof.
(* Goal: @IBILogic ((fun x y : Type => forall _ : x, y) T A) (@ILFun_Ops T A ILOps) (@BILFun_Ops T A BIOps) *)
    split.
(* Goal: @BILogic (@ILPreFrm T ord A ILOps) (@ILPre_Ops T ord ord_Pre A ILOps IL) (@BILPre_Ops T ord ord_Pre A ILOps BIOps BIL IL) *)
(* Goal: @lentails (@ILPreFrm T ord A ILOps) (@ILPre_Ops T ord ord_Pre A ILOps IL) (@ltrue (@ILPreFrm T ord A ILOps) (@ILPre_Ops T ord ord_Pre A ILOps IL)) (@empSP (@ILPreFrm T ord A ILOps) (@BILPre_Ops T ord ord_Pre A ILOps BIOps BIL IL)) *)
    apply BILPreLogic.
(* Goal: @lentails (forall _ : T, A) (@ILFun_Ops T A ILOps) (@ltrue (forall _ : T, A) (@ILFun_Ops T A ILOps)) (@empSP (forall _ : T, A) (@BILFun_Ops T A BIOps)) *)
    intro x; simpl; apply emp_trueE.
  Qed.

End IBILPre.

Section IBILogic_Fun.
  Context (T: Type).
  Context {A : Type} `{BIL: IBILogic A}.

  Local Existing Instance ILFun_Ops.
  Local Existing Instance ILFun_ILogic.
  Local Existing Instance BILFun_Ops.

  Local Transparent ILFun_Ops.

  Definition IBILFunLogic
  : @IBILogic ((fun x y => x -> y) T A) (@ILFun_Ops T A _) (@BILFun_Ops T A _).
  Proof.
(* Goal: @IBILogic ((fun x y : Type => forall _ : x, y) T A) (@ILFun_Ops T A ILOps) (@BILFun_Ops T A BIOps) *)
    split.
(* Goal: @BILogic (forall _ : T, A) (@ILFun_Ops T A ILOps) (@BILFun_Ops T A BIOps) *)
(* Goal: @lentails (forall _ : T, A) (@ILFun_Ops T A ILOps) (@ltrue (forall _ : T, A) (@ILFun_Ops T A ILOps)) (@empSP (forall _ : T, A) (@BILFun_Ops T A BIOps)) *)
    apply BILFunLogic. apply BIL.
(* Goal: @ILogic A ILOps *)
(* Goal: @lentails (forall _ : T, A) (@ILFun_Ops T A ILOps) (@ltrue (forall _ : T, A) (@ILFun_Ops T A ILOps)) (@empSP (forall _ : T, A) (@BILFun_Ops T A BIOps)) *)
    apply _. intro x; simpl; apply emp_trueE.
  Qed.

End IBILogic_Fun.

Opaque SAIBIOps.
