Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.RelationClasses.
Require Import Logic.lib.Coqlib.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.ProofTheory.RewriteClass.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.DeMorgan.
Require Import Logic.PropositionalLogic.ProofTheory.GodelDummett.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.PropositionalLogic.ProofTheory.RewriteClass.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.ProofTheory.SeparationLogic.

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

Section RewriteClass.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {Gamma: ProofTheory L}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma}.

Instance sepcon_proper_impp: Proper ((fun x y => |-- impp x y) ==> (fun x y => |-- impp x y) ==> (fun x y => |-- impp x y)) sepcon.
Proof.
(* Goal: @Proper (forall (_ : @expr L) (_ : @expr L), @expr L) (@respectful (@expr L) (forall _ : @expr L, @expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)))) (@wand L sL) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@wand L sL x1) (@wand L sL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x1 y1) (@sepcon L sL x2 y2)) *)
  apply sepcon_mono; auto.
Qed.

Instance wand_proper_impp: Proper ((fun x y => |-- impp x y) --> (fun x y => |-- impp x y) ==> (fun x y => |-- impp x y)) wand.
Proof.
(* Goal: @Proper (forall (_ : @expr L) (_ : @expr L), @expr L) (@respectful (@expr L) (forall _ : @expr L, @expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)))) (@wand L sL) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@wand L sL x1) (@wand L sL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@impp L minL (@wand L sL x1 y1) (@wand L sL x2 y2)) *)
  unfold Basics.flip in H.
(* Goal: @provable L Gamma (@impp L minL (@wand L sL x1 y1) (@wand L sL x2 y2)) *)
  apply wand_mono; auto.
Qed.

Instance sepcon_proper_iffp: Proper ((fun x y => |-- iffp x y) ==> (fun x y => |-- iffp x y) ==> (fun x y => |-- iffp x y)) sepcon.
Proof.
(* Goal: @Proper (forall (_ : @expr L) (_ : @expr L), @expr L) (@respectful (@expr L) (forall _ : @expr L, @expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)))) (@wand L sL) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@wand L sL x1) (@wand L sL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@wand L sL x1 y1) (@wand L sL x2 y2)) *)
  apply solve_andp_intros.
  + apply sepcon_mono.
    - rewrite H; apply provable_impp_refl.
    - rewrite H0; apply provable_impp_refl.
  + apply sepcon_mono.
    - rewrite H; apply provable_impp_refl.
    - rewrite H0; apply provable_impp_refl.
Qed.

Instance wand_proper_iffp: Proper ((fun x y => |-- iffp x y) ==> (fun x y => |-- iffp x y) ==> (fun x y => |-- iffp x y)) wand.
Proof.
(* Goal: @Proper (forall (_ : @expr L) (_ : @expr L), @expr L) (@respectful (@expr L) (forall _ : @expr L, @expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)))) (@wand L sL) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@wand L sL x1) (@wand L sL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@wand L sL x1 y1) (@wand L sL x2 y2)) *)
  apply solve_andp_intros.
  + apply wand_mono.
    - rewrite H; apply provable_impp_refl.
    - rewrite H0; apply provable_impp_refl.
  + apply wand_mono.
    - rewrite H; apply provable_impp_refl.
    - rewrite H0; apply provable_impp_refl.
Qed.

End RewriteClass.

Existing Instances sepcon_proper_impp wand_proper_impp sepcon_proper_iffp wand_proper_iffp.
