Require Import Logic.lib.EnsemblesProperties.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Local Open Scope logic_base.

Section ContextProperty.

Context {L: Language}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}.

Lemma Included_derivable: forall (Phi: context),
  Included _ Phi (derivable Phi).
Proof.
(* Goal: forall Phi : @context L, Included (@expr L) Phi (@derivable L Gamma Phi) *)
  intros; hnf; intros.
(* Goal: @derivable L Gamma Phi x *)
  apply derivable_assum; auto.
Qed.

Lemma derivable_mono: forall (Phi Psi: context),
  Included _ Phi Psi ->
  Included _ (derivable Phi) (derivable Psi).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  hnf; intros.
(* Goal: @derivable L Gamma Psi x *)
  eapply deduction_weaken; eauto.
Qed.

Lemma derivable_derivable: forall (Phi: context),
  Included _ (derivable (derivable Phi)) (derivable Phi).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  hnf; unfold Ensembles.In; intros.
(* Goal: @derivable L Gamma Phi x *)
  eapply derivable_trans with (derivable Phi); auto.
Qed.

Lemma derivable_derivable_Same_set: forall (Phi: context),
  Same_set _ (derivable (derivable Phi)) (derivable Phi).
Proof.
(* Goal: forall Phi : @context L, Same_set (@expr L) (@derivable L Gamma (@derivable L Gamma Phi)) (@derivable L Gamma Phi) *)
  intros; split.
  + apply derivable_derivable.
  + apply Included_derivable.
Qed.

End ContextProperty.

Section CanonicalProperties.

Context {L: Language}
        {Gamma: ProofTheory L}.

Definition derivable_closed : context -> Prop :=
  fun Phi => forall x, derivable Phi x -> Phi x.

Definition derivable_superset_preserved (P: context -> Prop): Prop :=
  forall Phi Psi, Included _ (derivable Phi) (derivable Psi) -> P Phi -> P Psi.

Definition derivable_subset_preserved (P: context -> Prop): Prop :=
  forall Phi Psi, Included _ (derivable Phi) (derivable Psi) -> P Psi -> P Phi.

Lemma not_derivable_superset_preserved_derivable_subset_preserved: forall P,
  derivable_superset_preserved P ->
  derivable_subset_preserved (fun X => ~ P X).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  hnf; intros.
(* Goal: not (P Phi) *)
  intro; apply H1; clear H1.
(* Goal: P Psi *)
  eapply H; [| exact H2].
(* Goal: Included (@expr L) (@derivable L Gamma Phi) (@derivable L Gamma Psi) *)
  auto.
Qed.

Context {bSC: BasicSequentCalculus L Gamma}.

Lemma derivable_subset_preserved_subset_preserved: forall P,
  derivable_subset_preserved P ->
  subset_preserved P.
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: @superset_preserved (@expr L) P *)
  hnf in H |- *.
(* Goal: forall (Phi Psi : Ensemble (@expr L)) (_ : Included (@expr L) Phi Psi) (_ : P Phi), P Psi *)
  intros ? ? ?; apply H.
(* Goal: Included (@expr L) (@derivable L Gamma Phi) (@derivable L Gamma Psi) *)
  intros ? ?.
(* Goal: @derivable L Gamma Psi x *)
  eapply deduction_weaken; eauto.
Qed.

Lemma derivable_superset_preserved_superset_preserved: forall P,
  derivable_superset_preserved P ->
  superset_preserved P.
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: @superset_preserved (@expr L) P *)
  hnf in H |- *.
(* Goal: forall (Phi Psi : Ensemble (@expr L)) (_ : Included (@expr L) Phi Psi) (_ : P Phi), P Psi *)
  intros ? ? ?; apply H.
(* Goal: Included (@expr L) (@derivable L Gamma Phi) (@derivable L Gamma Psi) *)
  intros ? ?.
(* Goal: @derivable L Gamma Psi x *)
  eapply deduction_weaken; eauto.
Qed.

Lemma derivable_closed_element_derivable: forall (Phi: context),
  derivable_closed Phi ->
  (forall x: expr, Phi x <-> Phi |-- x).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: Included (@expr L) (@derivable L Gamma Phi) (@derivable L Gamma Psi) *)
  split; intros; auto.
(* Goal: @derivable L Gamma Phi x *)
  apply derivable_assum; auto.
Qed.

End CanonicalProperties.

Section ContextProperties.

Context {L: Language}
        {Gamma: ProofTheory L}.

Definition can_derive (x: expr): context -> Prop :=
  fun Phi => Phi |-- x.

Definition cannot_derive (x: expr): context -> Prop :=
  fun Phi => ~ Phi |-- x.

Lemma can_derive_derivable_superset_preserved: forall x,
  derivable_superset_preserved (can_derive x).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: @superset_preserved (@expr L) (can_derive x) *)
  unfold can_derive.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  hnf; intros.
(* Goal: Included (@expr L) (@derivable L Gamma Phi) (@derivable L Gamma Psi) *)
  apply H; auto.
Qed.

Lemma cannot_derive_derivable_subset_preserved: forall x,
  derivable_subset_preserved (cannot_derive x).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: @derivable_subset_preserved L Gamma (cannot_derive x) *)
  apply (not_derivable_superset_preserved_derivable_subset_preserved _ (can_derive_derivable_superset_preserved x)).
Qed.

Context {bSC: BasicSequentCalculus L Gamma}.

Lemma can_derive_superset_preserved: forall x,
  superset_preserved (can_derive x).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: @superset_preserved (@expr L) (can_derive x) *)
  unfold can_derive.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  hnf; intros.
(* Goal: @derivable L Gamma Psi x *)
  eapply deduction_weaken; eauto.
Qed.

Lemma cannot_derive_subset_preserved: forall x,
  subset_preserved (cannot_derive x).
Proof.
(* Goal: forall x : @expr L, @subset_preserved (@expr L) (cannot_derive x) *)
  intros.
(* Goal: @subset_preserved (@expr L) (cannot_derive x) *)
  apply (not_superset_preserved_subset_preserved _ (can_derive_superset_preserved x)).
Qed.

End ContextProperties.
