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.
Require Import Logic.SeparationLogic.ProofTheory.RewriteClass.

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

Section DerivedRules.

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}.

Lemma provable_sepcon_andp_left: forall (x y z: expr),
  |-- (x && y) * z --> (x * z) && (y * z).
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@andp L pL x y)) *)
  apply solve_impp_andp.
  + apply sepcon_mono.
    - apply andp_elim1.
    - apply provable_impp_refl.
  + apply sepcon_mono.
    - apply andp_elim2.
    - apply provable_impp_refl.
Qed.

Lemma provable_sepcon_andp_right: forall (x y z: expr),
  |-- x * (y && z) --> (x * y) && (x * z).
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x (@andp L pL y z)) (@andp L pL (@sepcon L sL x y) (@sepcon L sL x z))) *)
  rewrite !(sepcon_comm x).
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL (@andp L pL y z) x) (@andp L pL (@sepcon L sL y x) (@sepcon L sL z x))) *)
  apply provable_sepcon_andp_left.
Qed.

Lemma provable_truep_sepcon_truep {ExtsGamma: ExtSeparationLogic L Gamma}:
  |-- TT * TT <--> TT.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  apply solve_andp_intros.
  + apply solve_impp_elim_left.
(* Goal: @provable L Gamma (@truep L minL pL) *)
    apply provable_impp_refl.
  + apply sepcon_ext.
Qed.

Lemma derivable_emp {s'L: SeparationEmpLanguage L} {eGamma: EmpSeparationLogic L Gamma} {gcsGamma: GarbageCollectSeparationLogic L Gamma}: forall (x y: expr),
  |-- emp.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
  rewrite <- (sepcon_elim2 TT emp).
(* Goal: @provable L Gamma (@sepcon L sL (@truep L minL pL) (@emp L sL s'L)) *)
  rewrite sepcon_emp.
(* Goal: @provable L Gamma (@truep L minL pL) *)
  apply provable_impp_refl.
Qed.

Lemma GC_Ext_Classical_collapse_aux {cpGamma: ClassicalPropositionalLogic L Gamma} {gcsGamma: GarbageCollectSeparationLogic L Gamma} {ExtsGamma: ExtSeparationLogic L Gamma}: forall (x: expr),
  |-- x --> x * x.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x (@sepcon L sL x x)) *)
  rewrite (sepcon_ext x) at 1.
  assert (|-- TT --> x || ~~ x) by (apply solve_impp_elim_left, excluded_middle).
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x (@truep L minL pL)) (@sepcon L sL x x)) *)
  rewrite H; clear H.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x (@orp L pL x (@negp L minL pL x))) (@sepcon L sL x x)) *)
  rewrite sepcon_orp_distr_r.
(* Goal: @provable L Gamma (@impp L minL (@orp L pL (@sepcon L sL x x) (@sepcon L sL x (@negp L minL pL x))) (@sepcon L sL x x)) *)
  apply solve_orp_impp; [apply provable_impp_refl |].
  rewrite <- (andp_dup (x * ~~ x)).
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x (@negp L minL pL x)) (@sepcon L sL x (@negp L minL pL x))) (@sepcon L sL x x)) *)
  rewrite sepcon_elim1 at 1.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL x (@sepcon L sL x (@negp L minL pL x))) (@sepcon L sL x x)) *)
  rewrite sepcon_elim2 at 1.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL x (@negp L minL pL x)) (@sepcon L sL x x)) *)
  clear sGamma gcsGamma ExtsGamma.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL x (@negp L minL pL x)) (@sepcon L sL x x)) *)
  AddSequentCalculus Gamma.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL x (@negp L minL pL x)) (@sepcon L sL x x)) *)
  rewrite provable_derivable.
  rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x (@negp L minL pL x)))) (@sepcon L sL x x) *)
  apply deduction_falsep_elim.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x (@negp L minL pL x)))) (@falsep L pL) *)
  apply deduction_modus_ponens with x.
  + apply deduction_andp_elim1 with (~~x).
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x (@negp L minL pL x)))) (@andp L pL x (@impp L minL x (@falsep L pL))) *)
    solve_assum.
  + apply deduction_andp_elim2 with x.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x (@negp L minL pL x)))) (@andp L pL x (@impp L minL x (@falsep L pL))) *)
    solve_assum.
Qed.

Theorem GC_Ext_Classical_collapse {cpGamma: ClassicalPropositionalLogic L Gamma} {gcsGamma: GarbageCollectSeparationLogic L Gamma} {ExtsGamma: ExtSeparationLogic L Gamma}: forall (x y: expr),
  |-- x * y <--> x && y.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  intros.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@andp L pL x y)) *)
  apply solve_andp_intros.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@andp L pL x y)) *)
  + apply solve_impp_andp.
    - apply sepcon_elim1.
    - apply sepcon_elim2.
  + rewrite (GC_Ext_Classical_collapse_aux (x && y)).
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL (@andp L pL x y) (@andp L pL x y)) (@sepcon L sL x y)) *)
    apply sepcon_mono.
    - apply andp_elim1.
    - apply andp_elim2.
Qed.

End DerivedRules.
