Require Import Logic.lib.Coqlib.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.TheoryOfSequentCalculus.

Local Open Scope logic_base.

Class NormalSequentCalculus (L: Language) (Gamma: ProofTheory L): Type := {
  provable_derivable: forall x, provable x <-> derivable empty_context x
}.

Class BasicSequentCalculus (L: Language) (Gamma: ProofTheory L) := {
  deduction_weaken: forall Phi Psi x, Included _ Phi Psi -> Phi |-- x -> Psi |-- x;
  derivable_assum: forall Phi x, Ensembles.In _ Phi x -> Phi |-- x;
  deduction_subst: forall (Phi Psi: context) y, (forall x, Psi x -> Phi |-- x) -> Union _ Phi Psi |-- y -> Phi |-- y
}.

Class FiniteWitnessedSequentCalculus (L: Language) (Gamma: ProofTheory L) := {
  derivable_finite_witnessed: forall (Phi: context) (y: expr), Phi |-- y -> exists xs, Forall Phi xs /\ (fun x => In x xs) |-- y
}.

Section DerivableRulesFromSequentCalculus.

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

Lemma deduction_subst1: forall Phi x y, Phi |-- x -> Phi;; x |-- y -> Phi |-- y.
Proof.
(* Goal: forall (Phi : @context L) (y : @expr L) (_ : @provable L Gamma y), @derivable L Gamma Phi y *)
  intros.
(* Goal: @derivable L Gamma Phi y *)
  apply deduction_subst with (Singleton _ x); auto.
(* Goal: forall (Phi : @context L) (y : @expr L) (_ : @provable L Gamma y), @derivable L Gamma Phi y *)
  intros.
(* Goal: @derivable L Gamma Phi x0 *)
  inversion H1; subst.
(* Goal: @derivable L Gamma Phi x0 *)
  auto.
Qed.

Lemma derivable_trans: forall (Phi Psi: context) y, (forall x, Psi x -> Phi |-- x) -> Psi |-- y -> Phi |-- y.
Proof.
(* Goal: forall (Phi : @context L) (y : @expr L) (_ : @provable L Gamma y), @derivable L Gamma Phi y *)
  intros.
(* Goal: @derivable L Gamma Phi x0 *)
  eapply deduction_subst; eauto.
(* Goal: @derivable L Gamma Phi x0 *)
  eapply deduction_weaken; eauto.
(* Goal: Included (@expr L) Psi (Union (@expr L) Phi Psi) *)
  apply right_Included_Union.
Qed.

Lemma deduction_weaken1: forall Phi x y,
  Phi |-- y ->
  Phi;; x |-- y.
Proof.
(* Goal: forall (Phi : @context L) (y : @expr L) (_ : @provable L Gamma y), @derivable L Gamma Phi y *)
  intros.
(* Goal: @derivable L Gamma Phi x0 *)
  eapply deduction_weaken; eauto.
(* Goal: @derivable L Gamma Phi x0 *)
  intros ? ?; left; auto.
Qed.

Lemma derivable_assum1: forall (Phi: context) (x: expr), Phi;; x |-- x.
Proof.
(* Goal: forall (Phi : @context L) (y : @expr L) (_ : @provable L Gamma y), @derivable L Gamma Phi y *)
  intros.
(* Goal: @derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) x *)
  apply derivable_assum.
(* Goal: Ensembles.In (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) x *)
  right; constructor.
Qed.

Lemma contextual_derivable_finite_witnessed {fwSC: FiniteWitnessedSequentCalculus L Gamma}: forall (Phi Psi: context) (y: expr), Union _ Phi Psi |-- y -> exists xs, Forall Psi xs /\ Union _ Phi (fun x => In x xs) |-- y.
Proof.
(* Goal: forall (Phi Psi : @context L) (y : @expr L) (_ : @derivable L Gamma (Union (@expr L) Phi Psi) y), @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) Psi xs) (@derivable L Gamma (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x xs)) y)) *)
  apply DeductionWeaken_DerivableFiniteWitnessed_2_ContextualDerivableFiniteWitnessed.
(* Goal: @derivable L Gamma Phi x0 *)
  + hnf; intros; eapply deduction_weaken; eauto.
(* Goal: @derivable L Gamma Phi x0 *)
  + hnf; intros; eapply derivable_finite_witnessed; eauto.
Qed.

Lemma deduction_weaken0 {SC: NormalSequentCalculus L Gamma}: forall Phi y,
  |-- y ->
  Phi |-- y.
Proof.
(* Goal: forall (Phi : @context L) (y : @expr L) (_ : @provable L Gamma y), @derivable L Gamma Phi y *)
  intros.
(* Goal: @derivable L Gamma Phi y *)
  rewrite provable_derivable in H.
(* Goal: @derivable L Gamma Phi x0 *)
  eapply deduction_weaken; eauto.
(* Goal: Included (@expr L) (@empty_context L) Phi *)
  intros ? [].
Qed.

End DerivableRulesFromSequentCalculus.

Ltac solve_assum :=
  (first [apply derivable_assum1 | assumption | apply deduction_weaken1; solve_assum] || fail 1000 "Cannot find the conclusion in assumption").

