Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.RelationClasses.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.ProofTheory.RewriteClass.
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.ProofTheory.SeparationLogic.
Require Import Logic.SeparationLogic.ProofTheory.DerivedRules.
Require Import Logic.SeparationLogic.ProofTheory.RewriteClass.
Require Import Logic.Extensions.ProofTheory.Stable.

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

Class Corable (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} := {
  corable: expr -> Prop;
  corable_pstable: PropositionalStable L Gamma corable;
  corable_sstable: SeparationStable L Gamma corable;
  corable_sabs: SeparationAbsorbStable L Gamma corable
}.

Section Corable.

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}
        {CosGamma: Corable L Gamma}.

Lemma corable_andp: forall x y, corable x -> corable y -> corable (x && y).
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
Proof. intros. apply (@andp_stable L _ _ Gamma corable corable_pstable); auto. Qed.

Lemma corable_orp: forall x y, corable x -> corable y -> corable (x || y).
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
Proof. intros. apply (@orp_stable L _ _ Gamma corable corable_pstable); auto. Qed.

Lemma corable_impp: forall x y, corable x -> corable y -> corable (x --> y).
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
Proof. intros. apply (@impp_stable L _ _ Gamma corable corable_pstable); auto. Qed.

Lemma corable_iffp: forall x y, corable x -> corable y -> corable (x <--> y).
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
Proof. intros. apply (@iffp_stable L _ _ Gamma corable corable_pstable); auto. Qed.

Lemma corable_falsep: corable FF.
Proof. apply (@falsep_stable L _ _ Gamma corable corable_pstable); auto. Qed.

Lemma corable_truep: corable TT.
Proof. apply (@truep_stable L _ _ Gamma corable corable_pstable); auto. Qed.

Lemma corable_sepcon: forall x y, corable x -> corable y -> corable (x * y).
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
Proof. intros. apply (@sepcon_stable L _ _ Gamma corable corable_sstable); auto. Qed.

Lemma corable_wand: forall x y, corable x -> corable y -> corable (x -* y).
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
Proof. intros. apply (@wand_stable L _ _ Gamma corable corable_sstable); auto. Qed.

Instance corable_proper_iff: Proper ((fun x y => |-- x <--> y) ==> iff) corable.
Proof. apply (@stable_proper_iffp L _ _ Gamma corable corable_pstable); auto. Qed.

Lemma corable_andp_sepcon1: forall x y z, corable x -> |-- (x && y) * z <--> x && (y * z).
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
Proof. intros. apply (@stable_andp_sepcon1 L _ _ _ Gamma corable corable_sabs); auto. Qed.

Lemma corable_andp_sepcon2: forall x y z, corable y -> |-- (x && y) * z <--> y && (x * z).
Proof.
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@andp L pL y z)) (@andp L pL z (@sepcon L sL x y))) *)
  rewrite andp_comm.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL (@andp L pL y z) x) (@andp L pL y (@sepcon L sL z x))) *)
  apply corable_andp_sepcon1; auto.
Qed.

Lemma corable_sepcon_andp1: forall x y z, corable y -> |-- x * (y && z) <--> y && (x * z).
Proof.
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@andp L pL y z)) (@andp L pL y (@sepcon L sL x z))) *)
  rewrite sepcon_comm.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL (@andp L pL y z) x) (@andp L pL y (@sepcon L sL x z))) *)
  rewrite (sepcon_comm x z).
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL (@andp L pL y z) x) (@andp L pL y (@sepcon L sL z x))) *)
  apply corable_andp_sepcon1; auto.
Qed.

Lemma corable_sepcon_andp2: forall x y z, corable z -> |-- x * (y && z) <--> z && (x * y).
Proof.
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@andp L pL y z)) (@andp L pL z (@sepcon L sL x y))) *)
  rewrite andp_comm.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@andp L pL z y)) (@andp L pL z (@sepcon L sL x y))) *)
  apply corable_sepcon_andp1; auto.
Qed.

Lemma corable_sepcon_imply_andp: forall x y, corable x -> corable y -> |-- x * y --> x && y.
Proof.
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  rewrite <- (andp_truep y) at 1.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@andp L pL y (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite corable_sepcon_andp1 by auto.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL y (@sepcon L sL x (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite <- (andp_truep x) at 1.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL y (@sepcon L sL (@andp L pL x (@truep L minL pL)) (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite corable_andp_sepcon1 by auto.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL y (@andp L pL x (@sepcon L sL (@truep L minL pL) (@truep L minL pL)))) (@andp L pL x y)) *)
  rewrite <- andp_assoc.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@andp L pL y x) (@sepcon L sL (@truep L minL pL) (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite (andp_comm x y).
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@andp L pL y x) (@sepcon L sL (@truep L minL pL) (@truep L minL pL))) (@andp L pL y x)) *)
  apply andp_elim1.
Qed.

Lemma corable_sepcon_is_andp {ExtsGamma: ExtSeparationLogic L Gamma}: forall x y, corable x -> corable y -> |-- x * y <--> x && y.
Proof.
(* Goal: forall (x y : @expr L) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma x) (_ : @corable L minL pL sL Gamma minAX ipGamma sGamma CosGamma y), @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  rewrite <- (andp_truep y) at 1.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@andp L pL y (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite corable_sepcon_andp1 by auto.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL y (@sepcon L sL x (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite <- (andp_truep x) at 1.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL y (@sepcon L sL (@andp L pL x (@truep L minL pL)) (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite corable_andp_sepcon1 by auto.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL y (@andp L pL x (@sepcon L sL (@truep L minL pL) (@truep L minL pL)))) (@andp L pL x y)) *)
  rewrite <- andp_assoc.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@andp L pL y x) (@sepcon L sL (@truep L minL pL) (@truep L minL pL))) (@andp L pL x y)) *)
  rewrite (andp_comm x y).
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@andp L pL y x) (@sepcon L sL (@truep L minL pL) (@truep L minL pL))) (@andp L pL y x)) *)
  rewrite provable_truep_sepcon_truep.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@andp L pL y x) (@truep L minL pL)) (@andp L pL y x)) *)
  rewrite andp_truep.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL y x) (@andp L pL y x)) *)
  apply provable_iffp_refl.
Qed.

End Corable.

Existing Instance corable_proper_iff.
