Require Import Environments Sequents SequentProps Cut DecisionProcedure.
From Stdlib Require Import Program.Equality.

Definition Lindenbaum_Tarski_preorder φ ψ :=
  ∅ • φ ⊢ ∅ • ψ.

Declare Scope provability.
Open Scope provability.

Notation "φ ≼ ψ" := (Lindenbaum_Tarski_preorder φ ψ) (at level 150) : provability.

(* Particular case of `additive_cut` easier to use *)
Corollary weak_cut φ ψ θ:
  (φ ≼ ψ) -> (ψ ≼ θ) ->
  φ ≼ θ.
Proof.
intros H1 H2.
eapply additive_cut.
- apply H1.
- exchl 0. now apply weakeningl.
Qed.

(* Decides whether one formula entails the other or not ; in the latter case return Eq.
   It uses the decision procedure defined at `DecisionProcedure.v`
*)
Definition obviously_smaller (φ ψ : form) :=
  if [φ] ⊢? [ψ] then Lt
  else if [ψ] ⊢? [φ] then Gt
  else Eq.

Definition choose_conj φ ψ :=
match obviously_smaller φ ψ with
  | Lt => φ
  | Gt => ψ
  | Eq => φ ∧ ψ
 end.

Lemma occurs_in_choose_conj v φ ψ :
  occurs_in v (choose_conj φ ψ) -> occurs_in v φ \/ occurs_in v ψ.
Proof. unfold choose_conj; destruct obviously_smaller; simpl; intros; tauto. Qed.

Definition make_conj φ ψ :=
match ψ with
  | ψ1 ∧ ψ2 =>
      match obviously_smaller φ ψ1 with
      | Lt => φ ∧ ψ2
      | Gt => ψ
      | Eq => φ ∧ ψ
      end
  | ψ1 → ψ2 =>
      if decide (obviously_smaller φ ψ1 = Lt)
      then choose_conj φ ψ2
      else choose_conj φ ψ
  | _ =>
      match φ with
      | φ1 → φ2 =>
          if decide (obviously_smaller ψ φ1 = Lt)
          then choose_conj φ2 ψ
          else choose_conj φ ψ
      | _ => choose_conj φ ψ
       end
end.

Infix "⊼" := make_conj (at level 60).

Lemma occurs_in_make_conj v (φ ψ : form) :
  occurs_in v (φ ⊼ ψ) -> occurs_in v φ \/ occurs_in v ψ.
Proof.
generalize ψ.
induction φ; intro ψ0; dependent destruction ψ0;
intro H; unfold make_conj in H; unfold choose_conj in H;
repeat match goal with
    | H: occurs_in _ (if ?cond then _ else _) |- _ => case decide in H
    | H: occurs_in _ (match ?x with _ => _ end) |- _ => destruct x
    | |- _ => simpl; simpl in H; tauto
end.
Qed.

Definition choose_disj φ ψ :=
match obviously_smaller φ ψ with
  | Lt => ψ
  | Gt => φ
  | Eq => φ ∨ ψ
 end.

Definition make_disj φ ψ : form :=
match ψ with
  | ψ1 ∨ ψ2 =>
      match obviously_smaller φ ψ1 with
      | Lt => ψ
      | Gt => φ ∨ ψ2
      | Eq => φ ∨ ψ
      end
  | ψ1 ∧ ψ2 =>
      if decide ((obviously_smaller φ ψ1) = Gt) then φ
      else if decide ((obviously_smaller φ ψ2) = Gt) then φ
      else choose_disj φ ψ
  |_ => choose_disj φ ψ
end.

Global Infix "⊻" := make_disj (at level 65).

Lemma occurs_in_choose_disj v φ ψ :
  occurs_in v (choose_disj φ ψ) -> occurs_in v φ \/ occurs_in v ψ.
Proof. unfold choose_disj; destruct obviously_smaller; simpl; intros; tauto. Qed.

Lemma occurs_in_make_disj v φ ψ :
  occurs_in v (φ ⊻ ψ) -> occurs_in v φ ∨ occurs_in v ψ.
Proof.
generalize ψ.
induction φ; intro ψ0; dependent destruction ψ0;
intro H; unfold make_disj in H; unfold choose_disj in H;
repeat match goal with
    | H: occurs_in _ (if ?cond then _ else _) |- _ => case decide in H
    | H: occurs_in _ (match ?x with _ => _ end) |- _ => destruct x
    | |- _ => simpl; simpl in H; tauto
end.
Qed.

(* "lazy" implication, which produces a potentially simpler, equivalent formula *)

Definition choose_impl (φ ψ : form) : form :=
     if decide (obviously_smaller φ ψ = Lt) then ⊤
     else if decide (obviously_smaller φ ⊥ = Lt) then ⊤
     else if decide (obviously_smaller ⊤ ψ = Lt) then ⊤
     else if decide (obviously_smaller ⊤ φ = Lt) then ψ
     else if decide (obviously_smaller ψ ⊥ = Lt) then ¬φ
     else if decide (is_negation φ ψ) then ¬φ
     else if decide (is_negation ψ φ) then ψ
    else φ → ψ.

Fixpoint make_impl φ ψ :=
match ψ with
  |(ψ1 → ψ2) => make_impl (make_conj φ ψ1) ψ2
  |_ => choose_impl φ ψ
end.

Infix "⇢" := make_impl (at level 66).

Lemma occurs_in_choose_impl v x y : occurs_in v (choose_impl x y) -> occurs_in v x ∨ occurs_in v y.
Proof.
intro H; unfold choose_impl in H; fold make_impl in H;
repeat match goal with
    | H: occurs_in _ (if ?cond then _ else _) |- _ => case decide in H
    | H: occurs_in _ (match ?x with _ => _ end) |- _ => destruct x
    | |- _ => simpl; simpl in H; tauto
end.
Qed.

Lemma occurs_in_make_impl v x y :
  occurs_in v (x ⇢ y) -> occurs_in v x ∨ occurs_in v y.
Proof.
revert x.
induction y; intro ψ0;
intro H; unfold make_impl in H; try apply occurs_in_choose_impl in H; try tauto.
apply IHy2 in H.
- destruct H as [H|H]; [ apply occurs_in_make_conj in H|]; simpl; tauto.
Qed.

Lemma occurs_in_make_impl2 v x y z:
  occurs_in v (x ⇢ (y ⇢ z)) -> occurs_in v x ∨ occurs_in v y ∨ occurs_in v z.
Proof.
intro H. apply occurs_in_make_impl in H. destruct H as [H|H]; try tauto.
apply occurs_in_make_impl in H. tauto.
Qed.

Definition conjunction l := foldl make_conj (⊥→ ⊥) (nodup form_eq_dec l).
Notation "⋀" := conjunction.

Definition disjunction l := foldl make_disj ⊥ (nodup form_eq_dec l).
Notation "⋁" := disjunction.

Lemma variables_conjunction x l : occurs_in x (⋀ l) -> exists φ, φ ∈ l /\ occurs_in x φ.
Proof.
unfold conjunction.
assert (Hcut : forall ψ, occurs_in x (foldl make_conj ψ (nodup form_eq_dec l))
  -> occurs_in x ψ \/ (∃ φ, (φ ∈ l ∧ occurs_in x φ)%type)).
{
induction l; simpl.
- tauto.
- intros ψ Hocc.
  case in_dec in Hocc; apply IHl in Hocc; simpl in Hocc;
  destruct Hocc as [Hx|(φ&Hin&Hx)]; try tauto.
  + right. exists φ. split; auto with *.
  + apply occurs_in_make_conj in Hx; destruct Hx as [Hx|Hx]; auto with *.
      right. exists a. auto with *.
  + right. exists φ. split; auto with *.
}
intro Hocc. apply Hcut in Hocc. simpl in Hocc. tauto.
Qed.

Lemma variables_disjunction x l :
  occurs_in x (⋁ l) -> exists φ, φ ∈ l /\ occurs_in x φ.
Proof.
unfold disjunction.
assert (Hcut : forall ψ, occurs_in x (foldl make_disj ψ (nodup form_eq_dec l))
  -> occurs_in x ψ \/ (∃ φ, (φ ∈ l ∧ occurs_in x φ)%type)).
{
induction l; simpl.
- tauto.
- intros ψ Hocc.
  case in_dec in Hocc; apply IHl in Hocc; simpl in Hocc;
  destruct Hocc as [Hx|(φ&Hin&Hx)]; try tauto.
  + right. exists φ. split; auto with *.
  + apply occurs_in_make_disj in Hx; destruct Hx as [Hx|Hx]; auto with *.
      right. exists a. auto with *.
  + right. exists φ. split; auto with *.
}
intro Hocc. apply Hcut in Hocc. simpl in Hocc. tauto.
Qed.

Lemma double_negation_obviously_smaller φ ψ:
 is_double_negation φ ψ -> ψ ≼ φ.
Proof.
intro H; rewrite H. apply ImpR; auto with proof.
- apply ImpL; auto with proof.
- box_tac. exchl 0. apply open_box_L; exchl 0. apply ImpL; auto with proof.
Qed.

Lemma is_implication_obviously_smaller φ ψ:
 is_implication φ ψ -> ψ ≼ φ.
Proof.
unfold is_implication. intro H.
destruct φ; try (contradict H; intros [θ Hθ]; discriminate).
case (decide (φ2 = ψ)).
- intro; subst. apply ImpR.
  + apply weakeningl, generalised_axiom.
  + box_tac; apply weakeningl, open_box_L, generalised_axiom.
- intro Hneq. contradict H; intros [θ Hθ]. dependent destruction Hθ. tauto.
Qed.

Lemma obviously_smaller_compatible_LT φ ψ :
  (obviously_smaller φ ψ = Lt -> φ ≼ ψ) *
  ((φ ≼ ψ) -> obviously_smaller φ ψ = Lt ).
Proof.
unfold obviously_smaller, Lindenbaum_Tarski_preorder.
case ([φ] ⊢? [ψ]); intros Hp.
- apply Provable_dec_of_Prop in Hp. split; intro. peapply Hp. trivial.
- split; intro Hf.
  + contradict Hf. case ([ψ] ⊢? [φ]); discriminate.
  + tauto.
Qed.

Lemma obviously_smaller_compatible_GT φ ψ :
  (obviously_smaller φ ψ = Gt -> ψ ≼ φ) *
  (((φ ≼ ψ) -> False) -> (ψ ≼ φ) -> obviously_smaller φ ψ = Gt ).
Proof.
unfold obviously_smaller, Lindenbaum_Tarski_preorder.
case ([ψ] ⊢? [φ]); intro Hp; case ([φ] ⊢? [ψ]); intro Hp'; split; try discriminate; trivial.
- intros Hf _. destruct Hp'. contradict Hf. tauto.
- intros. apply Provable_dec_of_Prop in Hp. peapply Hp.
- intros _ Hf. destruct Hp'. contradict Hf. tauto.
- intros _ Hf. destruct Hp'. contradict Hf. tauto.
Qed.

Lemma and_congruence φ ψ φ' ψ':
  (φ ≼ φ') -> (ψ ≼ ψ') -> (φ ∧ ψ) ≼ φ' ∧ ψ'.
Proof.
intros Hφ Hψ.
apply AndL.
apply AndR.
- now apply weakeningl.
- exchl 0. now apply weakeningl.
Qed.

Lemma choose_conj_topL φ : (choose_conj φ ⊤ = φ).
Proof.
unfold choose_conj.
rewrite (obviously_smaller_compatible_LT _ _).2. trivial.
apply ImpR; apply ExFalso.
Qed.

Lemma choose_conj_sound_L Δ Δ0 φ ψ:
  (Δ ⊢ Δ0 • φ) -> (Δ ⊢ Δ0 • ψ) -> Δ ⊢ Δ0 • choose_conj φ ψ.
Proof.
intros Hφ Hψ.
unfold choose_conj. case obviously_smaller; auto with proof.
Qed.

Corollary choose_conj_equiv_L φ ψ φ' ψ':
  (φ ≼ φ') -> (ψ ≼ ψ') -> (φ ∧ ψ) ≼ choose_conj φ' ψ'.
Proof.
intros H1 H2. apply choose_conj_sound_L; apply AndL; auto with proof.
exchl 0. apply weakeningl, H2.
Qed.

Lemma choose_conj_equiv_R φ ψ φ' ψ':
  (φ' ≼ φ) -> (ψ' ≼ ψ) -> choose_conj φ' ψ' ≼ φ ∧ ψ.
Proof.
intros Hφ Hψ.
unfold choose_conj.
case_eq (obviously_smaller φ' ψ'); intro Heq.
- now apply and_congruence.
- apply AndR.
  + assumption.
  + eapply weak_cut.
    * apply obviously_smaller_compatible_LT, Heq.
    * assumption.
- apply AndR.
  + eapply weak_cut.
    * apply obviously_smaller_compatible_GT, Heq.
    * assumption.
  + assumption.
Qed.

Hint Unfold Lindenbaum_Tarski_preorder : proof.

Lemma make_conj_equiv_L φ ψ φ' ψ' :
  (φ ≼ φ') -> (ψ ≼ ψ') -> (φ ∧ ψ) ≼ φ' ⊼ ψ'.
Proof.
intros Hφ Hψ.
unfold make_conj.
destruct ψ'.
- destruct φ'; try (exact (choose_conj_equiv_L _ _ _ _ Hφ Hψ)).
  case decide; intro; try (apply choose_conj_equiv_L; assumption).
  apply obviously_smaller_compatible_LT in e.
  apply weak_cut with ((φ ∧ φ'1) ∧ ψ).
  + apply AndL; apply AndR; [apply AndR|]; auto with proof.
    exchl 0. apply weakeningl; apply weak_cut with n; assumption.
  + apply choose_conj_equiv_L; auto with proof.
    apply AndL, ImpR_revl, Hφ.
- apply exfalso, AndL. exchl 0. apply weakeningl, Hψ.
- case_eq (obviously_smaller φ' ψ'1); intro Heq.
  + apply and_congruence; assumption.
  + apply and_congruence.
    * assumption.
    * apply AndR_rev in Hψ; apply Hψ.
  + apply AndL. exchl 0. apply weakeningl. assumption.
- destruct φ'; try (exact (choose_conj_equiv_L _ _ _ _ Hφ Hψ)).
  case decide; intro; try (apply choose_conj_equiv_L; assumption).
  apply obviously_smaller_compatible_LT in e.
  apply weak_cut with ((φ ∧ φ'1) ∧ ψ).
  + apply AndL; apply AndR; [apply AndR|]. auto with proof.
      * exchl 0. apply weakeningl; apply weak_cut with (ψ'1 ∨ ψ'2); assumption.
      * apply generalised_axiom.
  + apply choose_conj_equiv_L; auto with proof.
    apply AndL, ImpR_revl, Hφ.
- case (decide (obviously_smaller φ' ψ'1 = Lt)); intro.
  + apply weak_cut with (φ ∧ (φ ∧ ψ)).
     * apply AndR; auto with proof.
     * apply choose_conj_equiv_L. assumption.
        apply obviously_smaller_compatible_LT in e.
        apply contractionl, ImpR_revl. apply weak_cut with ψ'1.
        -- apply weak_cut with φ'; auto with proof.
        -- apply ImpR.
          ++ exchl 0. apply ImpR_revl, AndL. exchl 0. apply weakeningl, Hψ.
          ++ box_tac. exchl 0. apply open_box_L, ImpR_revl, AndL. exchl 0.
             apply weakeningl, Hψ.
  + apply choose_conj_equiv_L; assumption.
- dependent destruction φ'; try (exact (choose_conj_equiv_L _ _ _ _ Hφ Hψ)).
  case decide; intro; try (apply choose_conj_equiv_L; assumption).
  apply weak_cut with (ψ ∧ (φ ∧ φ'1)).
  + apply AndL, AndR. auto with proof. apply AndR. auto with proof.
    exchl 0. apply weakeningl. apply weak_cut with (□ ψ'). auto with proof.
    now apply obviously_smaller_compatible_LT.
  + apply weak_cut with ((φ ∧ φ'1) ∧ ψ).
     * apply AndR; auto with proof.
     * apply choose_conj_equiv_L; auto with proof.
       apply AndL, ImpR_revl, Hφ.
Qed.

Lemma make_conj_equiv_R φ ψ φ' ψ' :
  (φ' ≼ φ) -> (ψ' ≼ ψ) -> φ' ⊼ ψ' ≼ φ ∧ ψ.
Proof.
intros Hφ Hψ.
unfold make_conj.
destruct ψ'.
- destruct φ'; try case decide; intros; apply choose_conj_equiv_R; try assumption.
  eapply imp_cut; eassumption.
- destruct φ'; try case decide; intros; apply choose_conj_equiv_R; try assumption.
   eapply imp_cut; eassumption.
- case_eq (obviously_smaller φ' ψ'1); intro Heq.
  + now apply and_congruence.
  + apply AndR.
    * apply AndL. now apply weakeningl.
    * apply (weak_cut _ ( ψ'1 ∧ ψ'2) _).
      -- apply and_congruence;
         [now apply obviously_smaller_compatible_LT | apply generalised_axiom].
      -- assumption.
  + apply AndR.
    * apply AndL. apply weakeningl. eapply weak_cut.
      -- apply obviously_smaller_compatible_GT; apply Heq.
      -- assumption.
    * assumption.
- destruct φ'; try case decide; intros; apply choose_conj_equiv_R; try assumption.
   eapply imp_cut; eassumption.
- case decide; intro Heq.
  + apply choose_conj_equiv_R. assumption. eapply weak_cut; [|exact Hψ].
    apply ImpR.
    * apply weakeningl, generalised_axiom.
    * box_tac. apply weakeningl, open_box_L, generalised_axiom.
  + apply choose_conj_equiv_R; assumption.
- dependent destruction φ'; try case decide; intros; apply choose_conj_equiv_R; try assumption.
  eapply imp_cut; eassumption.
Qed.

Lemma specialised_weakening Γ Δ (φ ψ : form) : (φ ≼ ψ) -> (Γ• φ) ⊢ (Δ • ψ).
Proof.
intro H. apply generalised_weakeninglL,generalised_weakeningrL.
erewrite proper_Provable; [exact H| |]; ms.
Qed.

Lemma make_conj_sound_L Γ φ ψ θ : Γ•φ ∧ψ ⊢ θ -> Γ• φ ⊼ ψ ⊢ θ.
Proof.
intro H.
eapply additive_cut.
- apply specialised_weakening.
  apply make_conj_equiv_R; apply generalised_axiom.
- exchl 0. now apply weakeningl.
Qed.

Global Hint Resolve make_conj_sound_L : proof.

Lemma make_conj_complete_L Γ φ ψ θ : Γ• φ ⊼ ψ ⊢ θ -> Γ•φ ∧ψ ⊢ θ.
Proof.
intro H.
eapply additive_cut.
- apply specialised_weakening.
  apply make_conj_equiv_L; apply generalised_axiom.
- exchl 0. now apply weakeningl.
Qed.

Lemma make_conj_sound_R Γ Δ φ ψ : Γ ⊢ Δ • (φ ∧ ψ) -> Γ ⊢ Δ • (φ ⊼ ψ).
Proof.
intro H.
eapply symmetric_cut.
- exchr 0. apply weakeningr, H.
- apply make_conj_complete_L, generalised_axiom.
Qed.

Global Hint Resolve make_conj_sound_R : proof.

Lemma make_conj_complete_R Γ Δ φ ψ : Γ ⊢ Δ • (φ ⊼ ψ) -> Γ ⊢ Δ • (φ ∧ ψ).
Proof.
intro H.
eapply symmetric_cut.
- exchr 0. apply weakeningr, H.
- apply make_conj_sound_L, generalised_axiom.
Qed.

Lemma or_congruence φ ψ φ' ψ':
  (φ ≼ φ') -> (ψ ≼ ψ') -> (φ ∨ ψ) ≼ φ' ∨ ψ'.
Proof. intros Hφ Hψ. apply OrR, OrL; [|exchr 0]; auto with proof. Qed.

Lemma choose_disj_sound_L1 Δ Δ0 φ ψ:
  (Δ ⊢ Δ0 • φ) -> Δ ⊢ Δ0 • choose_disj φ ψ.
Proof.
intros Hφ.
unfold choose_disj. case_eq (obviously_smaller φ ψ); auto with proof.
intro Hs. apply obviously_smaller_compatible_LT in Hs.
apply symmetric_cut with φ.
- exchr 0. auto with *.
- now apply specialised_weakening.
Qed.

Lemma choose_disj_sound_L2 Δ Δ0 φ ψ:
  (Δ ⊢ Δ0 • ψ) -> Δ ⊢ Δ0 • choose_disj φ ψ.
Proof.
intros Hφ.
unfold choose_disj. case_eq (obviously_smaller φ ψ); auto with proof.
- intro Hs. apply OrR. exchr 0. auto with proof.
- intro Hs. apply obviously_smaller_compatible_GT in Hs.
  apply symmetric_cut with ψ.
  + exchr 0. auto with *.
  + now apply specialised_weakening.
Qed.

Lemma choose_disj_equiv_L φ ψ φ' ψ':
  (φ ≼ φ') -> (ψ ≼ ψ') -> (φ ∨ ψ) ≼ choose_disj φ' ψ'.
Proof.
intros Hφ Hψ.
unfold choose_disj.
case_eq (obviously_smaller φ' ψ'); intro Heq.
- case_eq (obviously_smaller ψ' φ'); intro Heq'.
  + apply or_congruence; assumption.
  + apply OrR, OrL; [|exchr 0]; auto with proof.
  + apply OrR, OrL; [|exchr 0]; auto with proof.
- apply OrL.
  + eapply weak_cut.
    * apply Hφ.
    * apply obviously_smaller_compatible_LT; assumption.
  + assumption.
- apply OrL.
  + assumption.
  + eapply weak_cut.
    * eapply weak_cut.
      -- apply Hψ.
      -- apply obviously_smaller_compatible_GT. apply Heq.
    * apply generalised_axiom.
Qed.

Lemma choose_disj_equiv_R φ ψ φ' ψ' :
  (φ' ≼ φ) -> (ψ' ≼ ψ) -> choose_disj φ' ψ' ≼ φ ∨ ψ.
Proof.
intros Hφ Hψ.
unfold choose_disj. apply OrR.
case_eq (obviously_smaller φ' ψ'); intro Heq.
- apply OrL; [|exchr 0]; auto with proof.
- exchr 0. auto with proof.
- auto with proof.
Qed.

Lemma make_disj_equiv_L φ ψ φ' ψ' :
  (φ ≼ φ') -> (ψ ≼ ψ') -> (φ ∨ ψ) ≼ φ' ⊻ ψ'.
Proof.
intros Hφ Hψ.
unfold make_disj.
destruct ψ'; try (exact (choose_disj_equiv_L _ _ _ _ Hφ Hψ)).
- repeat case decide; intros.
  + apply OrL.
    * assumption.
    * eapply weak_cut.
      -- apply Hψ.
      -- apply AndL; apply weakeningl; now apply obviously_smaller_compatible_GT.
  + apply OrL.
    * assumption.
    * eapply weak_cut.
      -- apply Hψ.
      -- apply AndL; exchl 0. apply weakeningl; now apply obviously_smaller_compatible_GT.
  + now apply choose_disj_equiv_L.
- case_eq (obviously_smaller φ' ψ'1); intro Heq.
  + now apply or_congruence.
  + apply OrL.
    * eapply weak_cut.
      -- apply Hφ.
      -- apply OrR, weakeningr. now apply obviously_smaller_compatible_LT.
    * assumption.
  + apply OrL.
    * apply OrR, weakeningr; auto with *.
    * eapply weak_cut.
      -- apply Hψ.
      -- apply or_congruence; [apply obviously_smaller_compatible_GT; assumption| apply generalised_axiom].
Qed.

Lemma make_disj_equiv_R φ ψ φ' ψ' :
  (φ' ≼ φ) -> (ψ' ≼ ψ) -> φ' ⊻ ψ' ≼ φ ∨ ψ.
Proof.
intros Hφ Hψ.
unfold make_disj.
destruct ψ'.
- now apply choose_disj_equiv_R.
- now apply choose_disj_equiv_R.
- repeat case decide; intros.
  + apply OrR. auto with *.
  + apply OrR. auto with *.
  + now apply choose_disj_equiv_R.
- case_eq (obviously_smaller φ' ψ'1); intro Heq.
 + now apply or_congruence.
 + apply OrR. exchr 0. auto with *.
 + apply OrL.
   * apply OrR. auto with *.
   * apply OrL_rev in Hψ.
     apply OrR. exchr 0. apply weakeningr, Hψ.
- now apply choose_disj_equiv_R.
- now apply choose_disj_equiv_R.
Qed.

Lemma make_disj_sound_L Γ φ ψ θ :
  Γ•φ ∨ψ ⊢ θ -> Γ•make_disj φ ψ ⊢ θ.
Proof.
intro H.
eapply additive_cut.
- apply specialised_weakening.
  apply make_disj_equiv_R; apply generalised_axiom.
- exchl 0. now apply weakeningl.
Qed.

Global Hint Resolve make_disj_sound_L : proof.

Lemma make_disj_complete_L Γ φ ψ θ :
  Γ • make_disj φ ψ ⊢ θ -> Γ • φ ∨ψ ⊢ θ.
Proof.
intro H.
eapply additive_cut.
- apply specialised_weakening.
  apply make_disj_equiv_L; apply generalised_axiom.
- exchl 0. now apply weakeningl.
Qed.

Lemma make_disj_sound_R Γ Δ φ ψ : Γ ⊢ Δ • (φ ∨ ψ) -> Γ ⊢ Δ • make_disj φ ψ.
Proof.
intro H.
eapply symmetric_cut.
- exchr 0. apply weakeningr. apply H.
- apply make_disj_complete_L, generalised_axiom.
Qed.

Global Hint Resolve make_disj_sound_R : proof.

Lemma make_disj_complete_R Γ Δ φ ψ : Γ ⊢ Δ • make_disj φ ψ -> Γ ⊢ Δ • (φ ∨ ψ).
Proof.
intro H.
eapply symmetric_cut.
- exchr 0. apply weakeningr. apply H.
- apply make_disj_sound_L, generalised_axiom.
Qed.

Lemma tautology_cut {Γ} {φ ψ θ} :
  Γ • (φ → ψ) ⊢ θ -> (φ ≼ ψ) -> Γ ⊢ θ.
Proof.
intros Hp H.
apply additive_cut with (φ → ψ).
  + apply ImpR; apply generalised_weakeninglL; peapply H.
  + apply Hp.
Qed.

Lemma Lindenbaum_Tarski_preorder_Bot φ : ⊥ ≼ φ.
Proof. apply ExFalso. Qed.

Local Hint Resolve Lindenbaum_Tarski_preorder_Bot : proof.

Lemma choose_impl_sound_L Γ φ ψ θ: Γ•(φ → ψ) ⊢ θ -> Γ•(choose_impl φ ψ) ⊢ θ.
Proof.
intro HP.
unfold choose_impl; repeat case decide; intros;
repeat match goal with
| H : obviously_smaller _ _ = Lt |- _ => apply obviously_smaller_compatible_LT in H
| H : obviously_smaller _ _ = Gt |- _ => apply obviously_smaller_compatible_GT in H
| H : is_negation _ _ |- _ => eapply symmetric_cut; [| exchl 0; apply weakeningl, HP]; apply ImpR, exfalso; exchl 0; auto with proof
end; trivial; try (solve [eapply imp_cut; eauto]);
try solve[apply weakeningl, (tautology_cut HP); trivial; try apply weak_cut with ⊥; auto with proof].
- apply weakeningl, (tautology_cut HP); trivial. apply additive_cut with (φ := ⊤); auto with proof.
  exchl 0. auto with proof.
- eapply additive_cut with (φ := (φ → ψ)).
  + apply ImpR; try box_tac; exchl 0; apply ImpL; auto with proof.
  + exchl 0. auto with proof.
- unfold is_negation in *. subst. eapply additive_cut with (φ := (¬ ψ → ψ)).
  + apply ImpR.
    * exchl 0. apply ImpL ; auto with proof.
    * rewrite open_boxes_add. exchl 0 ; apply ImpL ; auto with proof.
  + exchl 0 ; apply weakeningl ; auto.
Qed.

Lemma make_impl_sound_L Γ Δ φ ψ: Γ•(φ → ψ) ⊢ Δ -> Γ•(φ ⇢ ψ) ⊢ Δ.
Proof.
revert φ. induction ψ; intros φ HP; simpl; repeat case decide; intros.
1-4, 6: now apply choose_impl_sound_L.
apply IHψ2.
apply ImpLAnd in HP.
apply symmetric_cut with (φ ∧ ψ1 → ψ2).
- apply ImpR ; try apply HP ; apply make_conj_complete_L ;
  try box_tac ; try apply MP.
- exchl 0 ; apply weakeningl ; auto.
Qed.

Global Hint Resolve make_impl_sound_L : proof.

Lemma choose_impl_sound_R Γ Δ φ ψ: Γ ⊢ Δ • (φ → ψ) -> Γ ⊢ Δ • (choose_impl φ ψ).
Proof.
unfold choose_impl.
repeat case decide; intros ;
repeat match goal with
| |- _ ⊢ _ • ⊤ => apply ImpR, ExFalso
| H : obviously_smaller _ _ = Lt |- _ => apply obviously_smaller_compatible_LT in H
| H : obviously_smaller _ _ = Gt |- _ => apply obviously_smaller_compatible_GT in H
| H : is_negation _ _ |- _ => rewrite H in *; apply ImpR ; eapply additive_cut; [apply ImpR_rev, HP| exchl 0; auto with *]
end; trivial; auto with proof.
try (solve[peapply (cut ∅ Γ φ); auto with proof; eapply TopL_rev; eauto]).
- apply symmetric_cut with (φ:= ⊤ → ψ) ; [ | apply ImpL ; auto with proof].
  + exchr 0 ; apply weakeningr. apply symmetric_cut with (φ:= φ → ψ).
    * exchr 0 ; apply weakeningr ; auto with proof.
    * apply ImpR.
      -- exchl 0 ; apply ImpL ; auto with proof. apply specialised_weakening ; auto.
      -- box_tac. exchl 0 ; apply ImpL ; auto with proof. apply specialised_weakening ; auto.
- apply symmetric_cut with (φ:= φ → ψ) ; [ exchr 0 ; apply weakeningr ; auto | ].
  apply ImpR.
  + exchl 0. apply ImpL ; auto with proof. apply specialised_weakening ; auto.
  + box_tac. exchl 0 ; apply ImpL ; auto with proof. apply specialised_weakening ; auto.
- unfold is_negation in *. subst. apply symmetric_cut with (φ:= ¬ ψ → ψ) ; [ exchr 0 ; apply weakeningr ; auto | ].
  apply ImpR.
  + do 2 (exchl 0 ; apply ImpL ; auto with proof).
  + box_tac. do 2 (exchl 0 ; apply ImpL ; auto with proof).
- unfold is_negation in *. subst. apply symmetric_cut with (φ:= φ → ¬ φ) ; [ exchr 0 ; apply weakeningr ; auto | ].
  apply ImpR.
  + exchl 0 ; apply ImpL ; auto with proof. apply ImpL ; auto with proof.
  + box_tac. exchl 0 ; apply ImpL ; auto with proof. apply ImpL ; auto with proof.
Qed.

Lemma make_impl_sound_R Γ Δ φ ψ: Γ ⊢ Δ • (φ → ψ) -> Γ ⊢ Δ • φ ⇢ ψ.
Proof.
revert φ. induction ψ; intros φ HP; simpl.
1-4, 6: now apply choose_impl_sound_R.
apply IHψ2. apply symmetric_cut with (φ:= (φ → ψ1 → ψ2)) ; [ exchr 0 ; apply weakeningr ; auto | ].
apply ImpR.
- apply make_conj_sound_L, AndL. exchl 1 ; exchl 0. do 2 (apply ImpL ; auto with proof).
- box_tac. apply make_conj_sound_L, AndL. exchl 1 ; exchl 0. do 2 (apply ImpL ; auto with proof).
Qed.

Global Hint Resolve make_impl_sound_R : proof.

Lemma make_impl_sound_L2 Γ φ1 φ2 ψ θ:
  Γ•(φ1 → (φ2 → ψ)) ⊢ θ -> Γ•(φ1 ⇢ (φ2 ⇢ ψ)) ⊢ θ.
Proof.
intro HP. apply make_impl_sound_L in HP.
apply symmetric_cut with (φ1 ⇢ (φ2 → ψ)).
- apply make_impl_sound_L, make_impl_sound_R.
  apply ImpR.
  + exchl 0. apply ImpL ; auto with proof.
  + box_tac. exchl 0. apply ImpL ; auto with proof.
- exchl 0. apply weakeningl, HP.
Qed.

Global Hint Resolve make_impl_sound_L2: proof.

Lemma make_impl_sound_L2' Γ φ1 φ2 ψ θ:
  Γ•((φ1 → φ2) → ψ) ⊢ θ -> Γ•((φ1 ⇢ φ2) ⇢ ψ) ⊢ θ.
Proof.
intro HP. apply make_impl_sound_L.
apply symmetric_cut with ((φ1 → φ2) → ψ); [|exchl 0; apply weakeningl, HP].
apply ImpR.
- exchl 0. apply ImpL ; auto with proof.
- box_tac ; exchl 0. apply ImpL ; auto with proof.
Qed.

Lemma make_impl_complete_L Γ φ ψ θ:
  Γ•(φ ⇢ ψ) ⊢ θ -> Γ•(φ → ψ) ⊢ θ.
Proof.
intro HP.
apply additive_cut with (φ ⇢ ψ); [|exchl 0; apply weakeningl, HP].
apply make_impl_sound_R, generalised_axiom.
Qed.

Lemma make_impl_complete_L2 Γ φ1 φ2 ψ θ:
  Γ•(φ1 ⇢ (φ2 ⇢ ψ)) ⊢ θ -> Γ•(φ1 → (φ2 → ψ)) ⊢ θ.
Proof.
intro HP. apply make_impl_complete_L in HP.
apply additive_cut with (φ1 → φ2 ⇢ ψ); [|exchl 0; apply weakeningl, HP].
apply ImpR.
- exchl 0. apply ImpL ; auto with proof.
- box_tac ; exchl 0. apply ImpL ; auto with proof.
Qed.

Lemma make_impl_complete_R Γ φ ψ:
  Γ ⊢ ∅ • (φ ⇢ ψ) -> Γ ⊢ ∅ • (φ → ψ).
Proof.
intro HP.
apply additive_cut with (φ ⇢ ψ); [apply HP| apply make_impl_sound_L, generalised_axiom ].
Qed.

Lemma disjunction_L Γ Δ θ :
  ((forall φ, φ ∈ Δ -> (Γ•φ ⊢ θ)) -> (Γ•⋁ Δ ⊢ θ)) *
  ((Γ•⋁ Δ ⊢ θ) -> (forall φ, φ ∈ Δ -> (Γ•φ ⊢ θ))).
Proof.
unfold disjunction.
assert(Hcut :
  (forall ψ, (Γ•ψ ⊢ θ) -> (forall φ, φ ∈ Δ -> (Γ•φ ⊢ θ)) ->
    (Γ•foldl make_disj ψ (nodup form_eq_dec Δ) ⊢ θ)) *
  (forall ψ,((Γ•foldl make_disj ψ (nodup form_eq_dec Δ)) ⊢ θ ->
    (Γ•ψ ⊢ θ) * (∀ φ : form, φ ∈ Δ → (Γ•φ) ⊢ θ)))).
{
  induction Δ; simpl; split; intros ψ Hψ.
  - intro. apply Hψ.
  - split; trivial. intros φ Hin. contradict Hin. auto with *.
  - intro Hall. case in_dec; intro; apply (fst IHΔ).
    + exact Hψ.
    + auto with *.
    + simpl. apply make_disj_sound_L, OrL; auto with *.
    + auto with *.
  - case in_dec in Hψ; apply IHΔ in Hψ;
    destruct Hψ as [Hψ Hind].
    + split; trivial; intros φ Hin; destruct (decide (φ = a)); auto 2 with *.
        subst. apply Hind. now apply elem_of_list_In.
    + apply make_disj_complete_L in Hψ.
        apply OrL_rev in Hψ as [Hψ Ha].
        split; trivial; intros φ Hin; destruct (decide (φ = a)); auto with *.
}
split; apply Hcut. constructor 2.
Qed.

Lemma disjunction_R (Γ Δ : env) (φ : form) : (φ ∈ Δ) -> (Γ ⊢ ∅ • φ) -> (Γ ⊢ Δ).
Proof.
induction Δ as [|θ Δ] using gmultiset_rec.
- intro Hin. exfalso. inversion Hin.
- intros Hin Hp. case (decide (φ = θ)).
  + intro; subst. apply generalised_weakeningrR. rpeapply Hp.
  + intro. apply generalised_weakeningrL, IHΔ, Hp. ms.
Qed.

Lemma op_disjunction_R Γ Δ φ Π : φ ∈ Δ -> (Γ ⊢ Π • φ) -> (Γ ⊢ Π • ⋁ Δ).
Proof.
intros Hin Hprov. unfold disjunction. revert Hin.
assert(Hcut : forall ψ, ((φ ∈ Δ) + (Γ ⊢ Π • ψ)) -> (Γ ⊢ Π • foldl make_disj ψ (nodup form_eq_dec Δ))).
{
  induction Δ; simpl; intros ψ [Hin | Hψ].
  - contradict Hin; auto with *.
  - trivial.
  - case in_dec; intro; apply IHΔ; destruct (decide (φ = a)).
    + subst. left. now apply elem_of_list_In.
    + left. auto with *.
    + subst. right. apply make_disj_sound_R, OrR; exchr 0. auto with proof.
    + left. auto with *.
  - case in_dec; intro; apply IHΔ; right; trivial.
     apply make_disj_sound_R. auto with proof.
}
intro Hin. apply Hcut. now left.
Qed.

Lemma conjunction_R1 Γ Δ Π : (forall φ, φ ∈ Δ -> Γ ⊢ Π • φ) -> (Γ ⊢ Π • ⋀ Δ).
Proof.
intro Hprov. unfold conjunction.
assert(Hcut : forall θ, Γ ⊢ Π • θ -> Γ ⊢ Π • foldl make_conj θ (nodup form_eq_dec Δ)).
{
  induction Δ; intros θ Hθ; simpl; trivial.
  case in_dec; intro; auto with *.
  apply IHΔ.
  - intros; apply Hprov. now right.
  - apply make_conj_sound_R, AndR; trivial. apply Hprov. now left.
}
apply Hcut. apply ImpR ; apply ExFalso.
Qed.

Lemma conjunction_R2 Γ Δ Π : (Γ ⊢ Π • ⋀ Δ) -> (forall φ, φ ∈ Δ -> Γ ⊢ Π • φ).
Proof.
 unfold conjunction.
assert(Hcut : forall θ, Γ ⊢ Π • foldl make_conj θ (nodup form_eq_dec Δ) -> (Γ ⊢ Π • θ) * (forall φ, φ ∈ Δ -> Γ ⊢ Π • φ)).
{
  induction Δ; simpl; intros θ Hθ.
  - split; trivial. intros φ Hin; contradict Hin. auto with *.
  - case in_dec in Hθ ; destruct (IHΔ _ Hθ) as (Hθ' & Hi).
    + split ; auto. intros φ Hin. apply elem_of_cons in Hin; destruct (decide (φ = a)); subst; trivial ;
      apply Hi ; rewrite elem_of_list_In ; [auto | destruct Hin ; subst ; [contradiction | rewrite <- elem_of_list_In ; tauto]].
    + split.
      * apply make_conj_complete_R in Hθ'; destruct (AndR_rev _ _ Hθ') ; auto.
      * intros φ Hin; apply elem_of_cons in Hin; destruct (decide (φ = a)); subst; trivial.
       -- apply make_conj_complete_R in Hθ'; destruct (AndR_rev _ _ Hθ') ; auto.
       -- apply Hi. destruct Hin ; subst ; [contradiction | auto].
}
apply Hcut.
Qed.

Lemma conjunction_L Γ Δ φ Π: (φ ∈ Δ) -> (Γ•φ ⊢ Π) -> (Γ•⋀ Δ ⊢ Π).
Proof.
intros Hin Hprov. unfold conjunction. revert Hin.
assert(Hcut : forall ψ, ((φ ∈ Δ) + (Γ•ψ ⊢ Π)) -> (Γ•foldl make_conj ψ (nodup form_eq_dec Δ) ⊢ Π)).
{
  induction Δ; simpl; intros ψ [Hin | Hψ].
  - contradict Hin; auto with *.
  - trivial.
  - case in_dec; intro; apply IHΔ; destruct (decide (φ = a)).
    + subst. left. now apply elem_of_list_In.
    + left. auto with *.
    + subst. right. apply make_conj_sound_L, AndL; exchl 0. auto with proof.
    + left. auto with *.
  - case in_dec; intro; apply IHΔ; right; trivial.
     apply make_conj_sound_L. auto with proof.
}
intro Hin. apply Hcut. now left.
Qed.

Lemma conjunction_L' Γ Δ Δ0: (Γ ⊎ {[⋀ Δ]} ⊢ Δ0) -> Γ ⊎ list_to_set_disj Δ ⊢ Δ0.
Proof.
revert Δ0. unfold conjunction.
assert( Hstrong: ∀ θ Δ0, Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ Δ0
  → (Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ Δ0).
{
  induction Δ as [|δ Δ]; intros θ Δ0; simpl.
  - intro Hp. peapply Hp.
  - case in_dec; intros Hin Hp.
    + peapply (weakeningl δ). apply IHΔ, Hp. ms.
    + simpl in Hp. apply IHΔ in Hp.
      peapply (AndL_rev (Γ ⊎ list_to_set_disj Δ) θ δ).
      apply make_conj_complete_L, Hp.
}
  intros; apply additive_cut with (φ := ⊤); eauto with proof.
Qed.

Lemma disjunction_L' Γ Δ Δ0: (Γ ⊎ {[⋀ Δ]} ⊢ Δ0) -> Γ ⊎ list_to_set_disj Δ ⊢ Δ0.
Proof.
revert Δ0. unfold conjunction.
assert( Hstrong: ∀ θ Δ0, Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ Δ0
  → (Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ Δ0).
{
  induction Δ as [|δ Δ]; intros θ Δ0; simpl.
  - intro Hp. peapply Hp.
  - case in_dec; intros Hin Hp.
    + peapply (weakeningl δ). apply IHΔ, Hp. ms.
    + simpl in Hp. apply IHΔ in Hp.
      peapply (AndL_rev (Γ ⊎ list_to_set_disj Δ) θ δ).
      apply make_conj_complete_L, Hp.
}
  intros; apply additive_cut with (φ := ⊤); eauto with proof.
Qed.

Lemma conjunction_R Δ: list_to_set_disj Δ ⊢ ∅ • ⋀ Δ.
Proof.
apply conjunction_R1. intros φ Hφ. apply elem_of_list_to_set_disj in Hφ.
exhibit Hφ 0. apply generalised_axiom.
Qed.

Lemma conjunction_L'' Γ Δ Δ0:
  Γ ⊎ list_to_set_disj Δ ⊢ Δ0 -> (Γ ⊎ {[⋀ Δ]} ⊢ Δ0).
Proof.
revert Δ0. unfold conjunction.
assert( Hstrong: ∀ θ Δ1, (Γ ⊎ list_to_set_disj Δ) ⊎ {[θ]} ⊢ Δ1 ->
          Γ ⊎ {[foldl make_conj θ (nodup form_eq_dec Δ)]} ⊢ Δ1).
{
  induction Δ as [|δ Δ]; intros θ ϕ; simpl.
  - intro Hp. peapply Hp.
  - case in_dec; intros Hin Hp.
    + apply IHΔ.
      assert(Hin' : δ ∈ (Γ ⊎ list_to_set_disj Δ)).
      { apply gmultiset_elem_of_disj_union; right.
        apply elem_of_list_to_set_disj, elem_of_list_In, Hin. }
        exhibit Hin' 1.
        rewrite (proper_Provable _ _ (env_add_comm _ _ _) _ _ (env_refl _)).
        apply contractionl. exchl 1. exchl 0.
        rwl difference_singleton. peapply Hp.
    + simpl. apply IHΔ. apply make_conj_sound_L, AndL. peapply Hp.
}
intros. apply Hstrong, weakeningl. assumption.
Qed.

Lemma disjunction_L'' Γ Δ: (Γ ⊎ {[⋁ Δ]} ⊢ list_to_set_disj Δ).
Proof.
unfold disjunction.
assert(Hstrong : forall θ,
  Γ ⊎ {[foldl make_disj θ (nodup form_eq_dec Δ)]} ⊢KM list_to_set_disj Δ • θ). {
  induction Δ as [|δ Δ]; intros θ; simpl.
  - auto with proof.
  - replace ({[+ δ +]} ⊎ list_to_set_disj Δ • θ)
         with ((list_to_set_disj Δ) • θ • δ : env) by ms.
    case in_dec; intros Hin.
    + apply weakeningr, IHΔ; trivial.
    + simpl. apply OrR_rev, make_disj_complete_R, IHΔ.
  }
intros. apply symmetric_cut with ⊥.
- apply Hstrong.
- apply ExFalso.
Qed.

Lemma disjunction_R'' Γ Δ Δ0:
  Γ ⊢ Δ0 ⊎ list_to_set_disj Δ-> (Γ ⊢ Δ0 • ⋁ Δ).
Proof.
revert Δ0. unfold disjunction.
assert( Hstrong: ∀ θ Δ1, Γ ⊢ (Δ1 ⊎ list_to_set_disj Δ) ⊎ {[θ]} ->
          Γ ⊢ Δ1 • foldl make_disj θ (nodup form_eq_dec Δ)).
{
  induction Δ as [|δ Δ]; intros θ Δ1; simpl.
  - intro Hp. rpeapply Hp.
  - case in_dec; intros Hin Hp.
    + apply IHΔ.
         assert(Hin' : δ ∈ (Δ1 ⊎ list_to_set_disj Δ)).
         { apply gmultiset_elem_of_disj_union; right.
           apply elem_of_list_to_set_disj, elem_of_list_In, Hin. }
           exhibit Hin' 1.
          rewrite (proper_Provable _ _ (env_refl _) _ _ (env_add_comm _ _ _)).
           apply contractionr. exchr 1. exchr 0.
           rwr difference_singleton. rpeapply Hp.
    + simpl. apply IHΔ. apply make_disj_sound_R, OrR. rpeapply Hp.
}
intros. apply Hstrong, weakeningr. assumption.
Qed.