Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.RelationClasses.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.

Local Open Scope logic_base.

Section PropertiesOfSequentCalculus.

Context (L: Language)
        (Gamma: ProofTheory L).

Definition DerivableRefl: Prop :=
  forall x: expr, empty_context;; x |-- x.

Definition DeductionWeaken: Prop :=
  forall (Phi Psi: context) (x: expr), Included _ Phi Psi -> Phi |-- x -> Psi |-- x.

Definition DerivableAssu: Prop :=
  forall (Phi: context) (x: expr), Ensembles.In _ Phi x -> Phi |-- x.

Definition DeductionSubst1: Prop :=
  forall (Phi: context) (x y: expr), Phi |-- x -> Phi;; x |-- y -> Phi |-- y.

Definition DeductionSubst: Prop :=
  forall (Phi Psi: context) (y: expr), (forall x, Psi x -> Phi |-- x) -> Union _ Phi Psi |-- y -> Phi |-- y.

Definition DerivableFiniteWitnessed: Prop :=
  forall (Phi: context) (y: expr), Phi |-- y -> exists xs, Forall Phi xs /\ (fun x => In x xs) |-- y.

Definition ContextualDerivableFiniteWitnessed: Prop :=
  forall (Phi Psi: context) (y: expr), Union _ Phi Psi |-- y -> exists xs, Forall Psi xs /\ Union _ Phi (fun x => In x xs) |-- y.

End PropertiesOfSequentCalculus.

Section TheoryOfSequentCalculus.

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

Lemma DeductionWeaken_DerivableFiniteWitnessed_2_ContextualDerivableFiniteWitnessed:
  DeductionWeaken L Gamma ->
  DerivableFiniteWitnessed L Gamma ->
  ContextualDerivableFiniteWitnessed L Gamma.
Proof.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  intros.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  hnf; intros.
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) Phi xs) (@derivable L Gamma (fun x : @expr L => @In (@expr L) x xs) y)) *)
  apply H0 in H1; clear H0.
(* Goal: @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)) *)
  destruct H1 as [xs [? ?]].
(* Goal: @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)) *)
  assert (exists xs', (forall x, In x xs -> Phi x \/ In x xs') /\ forall x, In x xs' -> Psi x).
  + clear H1.
(* Goal: @ex (list (@expr L)) (fun xs' : list (@expr L) => and (forall (x : @expr L) (_ : @In (@expr L) x xs), or (Phi x) (@In (@expr L) x xs')) (forall (x : @expr L) (_ : @In (@expr L) x xs'), Psi x)) *)
    induction H0.
    - exists nil.
(* Goal: and (forall (x : @expr L) (_ : @In (@expr L) x (@nil (@expr L))), or (Phi x) (@In (@expr L) x (@nil (@expr L)))) (forall (x : @expr L) (_ : @In (@expr L) x (@nil (@expr L))), Psi x) *)
      split; simpl; intros; tauto.
    - destruct IHForall as [xs' [? ?]].
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
      rewrite Union_spec in H0; destruct H0; [exists xs' | exists (x :: xs')]; split; intros.
      * destruct H4; [subst; auto |].
(* Goal: or (Phi x0) (@In (@expr L) x0 xs') *)
        apply H2; auto.
      * apply H3; auto.
      * destruct H4; [simpl; auto |].
(* Goal: or (Phi x0) (@In (@expr L) x0 (@cons (@expr L) x xs')) *)
        apply H2 in H4.
(* Goal: or (Phi x0) (@In (@expr L) x0 (@cons (@expr L) x xs')) *)
        simpl; tauto.
      * destruct H4; [subst; auto |].
(* Goal: Psi x0 *)
        apply H3; auto.
  + destruct H2 as [xs' [? ?]].
(* Goal: @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)) *)
    exists xs'.
(* Goal: and (@Forall (@expr L) Psi xs') (@derivable L Gamma (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x xs')) y) *)
    split.
    - rewrite Forall_forall; auto.
    - eapply H; eauto.
(* Goal: Included (@expr L) (fun x : @expr L => @In (@expr L) x xs) (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x xs')) *)
      unfold Included, Ensembles.In; intro; rewrite Union_spec; auto.
Qed.

Lemma DeductionWeaken_ContextualDerivableFiniteWitnessed_2_DerivableFiniteWitnessed:
  DeductionWeaken L Gamma ->
  ContextualDerivableFiniteWitnessed L Gamma ->
  DerivableFiniteWitnessed L Gamma.
Proof.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  intros.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  hnf; intros.
  eapply H in H1; [| rewrite <- (Union_Empty_left Phi); apply Included_refl].
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) Phi xs) (@derivable L Gamma (fun x : @expr L => @In (@expr L) x xs) y)) *)
  apply H0 in H1; clear H0.
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) Phi xs) (@derivable L Gamma (fun x : @expr L => @In (@expr L) x xs) y)) *)
  destruct H1 as [xs [? ?]]; exists xs; split; auto.
(* Goal: @derivable L Gamma (fun x : @expr L => @In (@expr L) x xs) y *)
  eapply H in H1; [| rewrite Union_Empty_left; apply Included_refl].
(* Goal: @derivable L Gamma Phi x0 *)
  auto.
Qed.

Lemma DeductionSubst_2_DeductionSubst1:
  DeductionSubst L Gamma ->
  DeductionSubst1 L Gamma.
Proof.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  intros.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  hnf; intros.
(* Goal: @derivable L Gamma Phi x0 *)
  apply H with (Singleton _ x); auto.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  intros.
(* Goal: @derivable L Gamma Phi x0 *)
  inversion H2; subst.
(* Goal: @derivable L Gamma Phi x0 *)
  auto.
Qed.

Lemma DeductionWeaken_ContextualDerivableFiniteWitnessed_DeductionSubst1_2_DeductionSubst:
  DeductionWeaken L Gamma ->
  ContextualDerivableFiniteWitnessed L Gamma ->
  DeductionSubst1 L Gamma ->
  DeductionSubst L Gamma.
Proof.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  intros; hnf; intros.
(* Goal: @derivable L Gamma Phi y *)
  apply H0 in H3.
(* Goal: @derivable L Gamma Phi y *)
  destruct H3 as [xs [? ?]].
(* Goal: @derivable L Gamma Phi y *)
  eapply Forall_impl in H3; [| exact H2]; clear H2.
(* Goal: @derivable L Gamma Phi y *)
  induction H3.
  + eapply H; eauto.
(* Goal: or (Phi x0) (@In (@expr L) x0 (@cons (@expr L) x xs')) *)
    unfold Included, Ensembles.In; intro; rewrite Union_spec; simpl; tauto.
  + apply IHForall.
(* Goal: @derivable L Gamma (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x l)) y *)
    apply H1 with x.
    - eapply H; eauto.
(* Goal: or (Phi x0) (@In (@expr L) x0 (@cons (@expr L) x xs')) *)
      unfold Included, Ensembles.In; intro; rewrite Union_spec; simpl; tauto.
    - eapply H; eauto.
(* Goal: Included (@expr L) (Union (@expr L) Phi (fun x0 : @expr L => @In (@expr L) x0 (@cons (@expr L) x l))) (Union (@expr L) (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x l)) (Singleton (@expr L) x)) *)
      unfold Included, Ensembles.In; intro; rewrite !Union_spec; simpl.
(* Goal: @derivable L Gamma Phi x0 *)
      intros [? | [? | ?]]; auto.
(* Goal: or (or (Phi x0) (@In (@expr L) x0 l)) (Singleton (@expr L) x x0) *)
      right; subst; constructor.
Qed.

Lemma DerivableRefl_DeductionWeaken_2_DerivableAssu:
  DerivableRefl L Gamma ->
  DeductionWeaken L Gamma ->
  DerivableAssu L Gamma.
Proof.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  intros.
(* Goal: DerivableAssu L Gamma *)
  intros ? ? ?.
(* Goal: @derivable L Gamma Phi x *)
  eapply H0; [| apply H].
(* Goal: Included (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) x)) Phi *)
  intros ? ?.
(* Goal: Ensembles.In (@expr L) Phi x0 *)
  destruct H2.
  + destruct H2.
  + destruct H2; auto.
Qed.

Lemma DerivableAssu_2_DerivableRefl:
  DerivableAssu L Gamma ->
  DerivableRefl L Gamma.
Proof.
(* Goal: forall _ : DerivableAssu L Gamma, DerivableRefl L Gamma *)
  intros.
(* Goal: DerivableRefl L Gamma *)
  intros ?.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) x)) x *)
  apply H.
(* Goal: Ensembles.In (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) x)) x *)
  right.
(* Goal: Ensembles.In (@expr L) (Singleton (@expr L) x) x *)
  constructor.
Qed.

End TheoryOfSequentCalculus.
