Require Import syntax syntax_facts Sequents Order.
Require Import SequentProps.
From Stdlib Require Import Program.Equality.

Local Hint Rewrite @elements_env_add : order.

Lemma env_weight_0_empty (Δ : env) : env_weight (elements Δ) = 0 -> Δ = ∅.
Proof.
intro Hw. destruct Δ as [|x Δ] using gmultiset_ind; trivial.
contradict Hw. unfold env_weight.
setoid_rewrite gmultiset_elements_disj_union.
setoid_rewrite gmultiset_elements_singleton.
rewrite map_app, list_sum_app. simpl.
pose(weight_pos x).
destruct (Nat.pow_gt_1 9 (weight x)); lia.
Qed.

Theorem symmetric_cut (φ : form) (Γ Δ : env) :
  Γ ⊢ Δ • φ -> Γ • φ ⊢ Δ ->
  Γ ⊢ Δ.
Proof.
remember (weight φ) as w. assert(Hw : weight φ ≤ w) by lia. clear Heqw.
revert φ Hw Δ Γ.
induction w; intros φ Hw; [pose (weight_pos φ); lia|].
intros Δ Γ.
remember (Γ, Δ) as pe.
replace Γ with pe.1 by now subst.
replace Δ with pe.2 by now subst.
clear Heqpe Γ Δ. revert pe.
refine (@well_founded_induction _ _ wf_env_pair_ms_order _ _).
intros (Γ &Δ). simpl. intro IHW'. assert (IHW := fun Γ0 => fun Δ0 => IHW' (Γ0, Δ0)).
simpl in IHW. clear IHW'. intros HPφ HPΔ.
Ltac eqtac := try match goal with | x : (?Δ0 • ?a) = (?Δ • ?phi) |- _ =>
  let Heq := fresh "Heq" in rename x into Heq;
  assert(Hin : a ∈ (Δ • phi)) by(rewrite <- Heq; ms);
  assert(Hin' : phi ∈ (Δ0 • a)) by(rewrite Heq; ms);
  try assert(a ∈ (Δ • phi)) by ms;
  apply symmetry, env_equiv_eq, env_add_inv' in Heq; try rwr Heq end.
Ltac otac Heq := subst; repeat rewrite env_replace in Heq by trivial;
repeat rewrite env_add_remove by trivial; order_tac; rewrite Heq; repeat order_tac.
dependent destruction HPφ; eqtac; simpl in Hw.
- case (decide (φ = #p)); intro; subst.
  + apply contractionl. rpeapply HPΔ.
  + eqtac. forwardr. apply Atom.
- apply ExFalso.
- case (decide(φ = (φ0 ∧ ψ))); intro; subst.
  + rewrite env_add_remove in *. simpl in Hw. apply AndL_rev in HPΔ.
    do 2 (apply IHw in HPΔ; trivial; try lia).
    * rpeapply HPΔ.
    * rpeapply HPφ1.
    * apply weakeningl. rpeapply HPφ2.
    * apply weakeningl. rpeapply HPφ2.
  + forwardr. apply AndR; backwardr.
    * apply IHW; trivial; try lia.
      -- otac Heq.
      -- backwardr. rewrite env_add_remove. apply HPφ1.
      -- forwardr. apply AndR_rev with(φ2 := ψ). backwardr. rpeapply HPΔ.
    * apply IHW; trivial; try lia.
      -- otac Heq.
      -- backwardr. rewrite env_add_remove. apply HPφ2.
      -- forwardr. apply AndR_rev with(φ1 := φ0). backwardr. rpeapply HPΔ.
- apply AndL. apply IHW; trivial.
  + order_tac.
  + exchl 0. exchl 1. apply AndL_rev. peapply HPΔ.
- case (decide(φ = (φ0 ∨ ψ))); intro; subst.
  + rewrite env_add_remove in *. simpl in Hw.
    apply OrL_rev in HPΔ. apply (IHw φ0); [lia| |rpeapply HPΔ ]; try tauto.
    apply (IHw ψ); [lia| |]; try tauto.
    apply weakeningr. rpeapply HPΔ.
  + forwardr. apply OrR. do 2 backwardr. apply IHW.
    * otac Heq.
    * backwardr. rewrite env_add_remove. now exchr 0.
    * do 2 forwardr. apply OrR_rev. backwardr. rpeapply HPΔ.
- apply OrL; apply IHW; trivial; try order_tac; exchl 0.
  + apply OrL_rev with (ψ := ψ). now exchl 0.
  + apply OrL_rev with (φ := φ0). now exchl 0.
- (* ImpR *)
 (* (V) *) (* hard:  *)
(* START *)
  case (decide(φ = (φ0 → ψ))); intro; subst.
  2 : {
    forwardr. apply ImpR; trivial.
    apply IHW. otac Heq.
    - backwardr. rewrite env_add_remove. exact HPφ1.
    - exchl 0. apply ImpR_revl. backwardr. rpeapply HPΔ.
  }
  rewrite env_add_remove in *. clear H Hin Hin'.
  rwr (symmetry Heq).
  assert(HPφ1' : Γ • φ0 ⊢KM Δ • ψ) by rpeapply HPφ1; clear HPφ1 Δ0 Heq.
  dependent destruction HPΔ; eqtac; try rwl Heq; simpl in Hw.
  + forwardl. auto with proof.
  + forwardl. auto with proof.
  + apply AndR.
     * apply IHW.
     -- order_tac.
     -- apply ImpR; trivial.
        exchr 0. apply AndR_rev with (φ2 := ψ0). now exchr 0.
     -- peapply HPΔ1.
     * apply IHW.
     -- order_tac.
     -- apply ImpR; trivial.
        exchr 0. apply AndR_rev with (φ1 := φ). now exchr 0.
     -- peapply HPΔ2.
  + forwardl. apply AndL. apply IHW.
     * otac Heq.
     * apply AndL_rev. backwardl. rwl (symmetry Heq). now apply ImpR; trivial.
     * backwardl. peapply HPΔ.
  + apply OrR, IHW.
    * order_tac.
    * apply ImpR; trivial. exchr 0. exchr 1. apply OrR_rev. exchr 0. apply HPφ1'.
    * peapply HPΔ.
  + forwardl.
     apply ImpR in HPφ1'; trivial.
     assert(HPφ' : (((Γ0 ∖ {[φ0→ ψ]}) • (φ ∨ ψ0) ⊢ Δ • (φ0 → ψ)))).
      by (backwardl; peapply HPφ1').
    apply OrL.
    * apply IHW.
      -- otac Heq.
      -- eapply (OrL_rev _ φ ψ0); eauto.
      -- backwardl. peapply HPΔ1.
    * apply IHW.
      -- otac Heq.
      -- eapply (OrL_rev _ φ ψ0); eauto.
      -- backwardl. peapply HPΔ2.
  + apply ImpR.
    * apply IHW.
      -- repeat order_tac.
      -- exchr 0. apply ImpR_revl. exchr 0. apply ImpR; trivial.
      -- exchl 0. trivial.
    * apply IHW.
      -- repeat order_tac.
      -- exchr 0. apply weakeningl, weakeningr. apply ImpR; trivial.
         apply open_boxes_R; trivial.
      -- exchl 0. peapply HPΔ2.
  + case (decide ((Var p → φ) = (φ0 → ψ))).
      * intro Heq'; dependent destruction Heq'.
         replace ((Γ0 • Var p • (p → ψ)) ∖ {[p → ψ]}) with (Γ0 • Var p) by ms.
         apply (IHw ψ).
        -- lia.
        -- apply contractionl. peapply HPφ1'.
        -- assumption.
      * intro Hneq. do 2 forwardl. exchl 0. apply ImpLVar, IHW.
        -- otac Heq.
        -- apply imp_cut with (φ := Var p). exchl 0. do 2 backwardl.
            rwl (symmetry Heq). apply ImpR; trivial.
        -- backwardl. rewrite env_add_remove. trivial.
  + case (decide (((φ1 ∧ φ2) → φ3)= (φ0 → ψ))).
    * intro Heq'; dependent destruction Heq'. rwl (symmetry Heq).
       apply (IHw (φ1 → φ2 → ψ)).
      -- simpl in *. lia.
      -- apply ImpR; apply ImpR; repeat box_tac.
        ++ apply AndL_rev, HPφ1'.
        ++ exchl 0. apply open_box_L. exchl 0. now apply AndL_rev.
        ++ now apply AndL_rev.
        ++ exchl 0. apply open_box_L. exchl 0. apply AndL_rev. now apply open_boxes_R.
      -- peapply HPΔ.
    * intro Hneq. forwardl. apply ImpLAnd, IHW.
      -- otac Heq.
      -- apply ImpLAnd_rev. backwardl. rwl (symmetry Heq). now apply ImpR.
      -- backwardl. rewrite env_add_remove. exact HPΔ.
  + case (decide (((φ1 ∨ φ2) → φ3)= (φ0 → ψ))).
      * intro Heq'; dependent destruction Heq'. rwl (symmetry Heq).
        apply OrL_rev in HPφ1'.
         apply (IHw (φ1 → ψ)).
        -- simpl in *. lia.
        -- apply (IHw (φ2 → ψ)).
           ++ simpl in *; lia.
           ++ apply ImpR.
            ** exchr 0. apply weakeningr, HPφ1'.
            ** eapply OrL_rev, HPφ2.
           ++ apply weakeningl, ImpR.
            ** apply HPφ1'.
            ** eapply OrL_rev with (ψ := φ2), HPφ2.
        -- apply (IHw (φ2 → ψ)).
           ++ simpl in *; lia.
           ++ apply weakeningl, ImpR.
            ** apply HPφ1'.
            ** eapply OrL_rev with (ψ := φ2), HPφ2.
           ++ peapply HPΔ.
      * intro Hneq. forwardl. apply ImpLOr, IHW.
        -- otac Heq.
        -- apply ImpLOr_rev. backwardl. rwl (symmetry Heq). now apply ImpR.
        -- backwardl. rewrite env_add_remove. exact HPΔ.
  + case (decide (((φ1 → φ2) → φ3) = (φ0 → ψ))).
     * intro Heq'. dependent destruction Heq'.
       rewrite env_add_remove in *.
       rwl (symmetry Heq). apply (IHw ψ).
      -- lia.
      -- apply (IHw(φ1 → φ2)).
        ++ lia.
        ++ apply (IHw (φ2 → ψ)).
          ** simpl in *. lia.
          ** apply ImpR.
            --- eapply imp_cut. apply weakeningr, generalised_axiom.
            --- eapply imp_cut, HPφ2.
          ** exchr 0. apply weakeningr. apply ImpR; repeat box_tac.
            --- peapply HPΔ1.
            --- peapply HPΔ2.
        ++ exact HPφ1'.
      -- peapply HPΔ3.
   * (* (V-d) *)
     intro Hneq. forwardl. apply ImpLImp.
     -- apply IHW.
      ++ otac Heq.
      ++ exchl 0. apply ImpLImp_prev'. backwardl. rwl (symmetry Heq).
         apply ImpR; trivial. exchr 0. apply weakeningr, HPφ1'.
      ++ backwardl. rewrite env_add_remove. exact HPΔ1.
     -- apply IHW.
      ++ otac Heq.
      ++ exchl 0. apply ImpLImp_prev'. box_tac. backwardl.
         exchr 0. apply weakeningr. apply ImpR; [|apply open_boxes_R];
         lazy_apply HPφ2; rewrite Heq, open_boxes_remove; ms.
      ++ box_tac. backwardl. rewrite env_add_remove. exact HPΔ2.
     -- apply IHW.
      ++ otac Heq.
      ++ apply (ImpLImp_prev _ φ1 φ2 φ3). backwardl. rwl (symmetry Heq).
         now apply ImpR.
      ++ backwardl. rewrite env_add_remove. exact HPΔ3.
  + case (decide ((□ φ1 → φ2) = (φ0 → ψ))).
     * intro Heq'. dependent destruction Heq'. rwl (symmetry Heq).
        assert(Γ = Γ0) by ms. subst Γ0. clear Hin.
        apply (IHw (□ φ1)).
      -- lia.
      -- apply BoxR, (IHw ψ).
        ++ lia.
        ++ exchr 0. apply weakeningr, HPφ2.
        ++ exact HPΔ1.
     -- apply (IHw ψ).
        ++ lia.
        ++ exact HPφ1'.
        ++ exchl 0. apply weakeningl, HPΔ2.
    * (* (V-f ) *)
       intro Hneq. forwardl. apply ImpLBox.
       -- apply IHW.
        ++ otac Heq.
        ++ apply ImpR.
          ** exchl 0. apply ImpLBox_prev with φ1. box_tac. backwardl. exchl 0.
             apply weakeningl. exchr 0. apply weakeningr.
             lazy_apply HPφ2. rewrite Heq. ms.
          ** apply open_boxes_R.
             exchl 0. apply ImpLBox_prev with φ1. box_tac. backwardl. exchl 0.
             apply weakeningl. lazy_apply HPφ2. rewrite Heq. ms.
        ++ box_tac. backwardl. rewrite env_add_remove. exact HPΔ1.
       -- apply IHW.
        ++ otac Heq.
        ++ apply ImpLBox_prev with φ1. backwardl. rwl (symmetry Heq).
           now apply ImpR.
        ++ backwardl. rewrite env_add_remove. exact HPΔ2.
  + rewrite open_boxes_add in HPΔ. simpl in HPΔ. apply BoxR, IHW.
    * repeat order_tac.
    * exchr 0. apply weakeningr, weakeningl, ImpR; trivial.
      apply open_boxes_R; trivial.
    * exchl 0. exact HPΔ.
- apply ImpLVar. eapply IHW; eauto.
  + otac Heq.
  + exchl 0. apply (imp_cut (Var p)). exchl 0; exact HPΔ.
- apply ImpLAnd. eapply IHW; eauto.
  + otac Heq.
  + exchl 0. apply ImpLAnd_rev. exchl 0. exact HPΔ.
- apply ImpLOr. eapply IHW; eauto.
  + otac Heq.
  + exchl 0. exchl 1. apply ImpLOr_rev. exchl 0. exact HPΔ.
- apply ImpLImp; [|assumption|].
  + apply IHW.
    * do 2 order_tac.
    * rpeapply HPφ1.
    * exchl 0. exchl 1. exchl 0. apply ImpLImp_prev'. exchl 0.
      apply weakeningr, HPΔ.
  + apply IHW; [order_tac|trivial|].
    exchl 0. eapply ImpLImp_prev; exchl 0; eassumption.
- apply ImpLBox; trivial. apply IHW; trivial.
  * otac Heq.
  * exchl 0. eapply ImpLBox_prev. exchl 0. exact HPΔ.
- (* BoxR *)
  case (decide (φ = □ φ0)); intro; subst; [|forwardr; now apply BoxR].
  rewrite env_add_remove in *.
(* (VIII) *)
  remember (Γ • □ φ0) as Γ' eqn:HH.
  rwr (symmetry Heq). clear Heq Δ0 Hin Hin'.
  assert (Heq: Γ ≡ Γ' ∖ {[ □ φ0 ]}) by ms.
  assert(Hin : (□ φ0) ∈ Γ')by ms.
  rwl Heq. dependent destruction HPΔ.
  + forwardl. auto with proof.
  + forwardl. auto with proof.
  + apply AndR.
     * apply IHW.
     -- otac H.
     -- rwl (symmetry Heq). now apply BoxR.
     -- peapply HPΔ1.
     * peapply (IHW Γ).
       -- otac Heq.
       -- apply BoxR. box_tac. peapply HPφ.
       -- peapply HPΔ2.
  + forwardl. apply AndL. apply IHW.
     * otac Heq.
     * apply AndL_rev. backwardl. rwl (symmetry Heq). apply BoxR, HPφ.
     * backwardl. peapply HPΔ.
  + apply OrR, IHW.
    * otac Heq.
    * rwl (symmetry Heq). apply BoxR, HPφ.
    * peapply HPΔ.
  + forwardl. apply BoxR with (Δ := Δ) in HPφ.
     assert(Hin'' : (φ ∨ ψ) ∈ ((Γ0 • φ ∨ ψ) ∖ {[□ φ0]}))
       by (apply in_difference; [discriminate|ms]).
     assert(HPφ' : (((Γ0 • φ ∨ ψ) ∖ {[□ φ0]}) ∖ {[φ ∨ ψ]} • φ ∨ ψ) ⊢ Δ • □ φ0).
     { rwl difference_singleton. rwl (symmetry Heq). exact HPφ. }
     assert (HP := (OrL_rev _ φ ψ _ HPφ')).
     apply OrL.
      * apply IHW.
        -- otac Heq.
        -- peapply HP.1.
        -- exchl 0. rwl difference_singleton. exact HPΔ1.
      * apply IHW.
        -- otac Heq.
        -- peapply HP.2.
        -- exchl 0. rwl difference_singleton. exact HPΔ2.
  + subst Γ0. rwl (symmetry Heq). apply ImpR.
    * apply IHW.
      -- otac Heq.
      -- apply weakeningl, BoxR, HPφ.
      -- exchl 0. peapply HPΔ1.
    * eapply IHW.
      -- otac Heq.
      -- apply weakeningl, BoxR, open_boxes_R, HPφ.
      -- apply IHw with φ0. (* inductive hypothesis on the smaller formula this time *)
        ++ simpl in Hw; lia.
        ++ exchl 0; exchr 0. apply weakeningr, weakeningl, HPφ.
        ++ exchl 0. exchl 1. apply weakeningl. peapply HPΔ2.
  + do 2 forwardl. exchl 0. apply ImpLVar, IHW.
    * otac Heq.
    * apply imp_cut with (φ := Var p). exchl 0. do 2 backwardl.
       rewrite HH. apply BoxR with (Δ := Δ) in HPφ. peapply HPφ.
    * backwardl. rewrite env_add_remove. exact HPΔ.
  + forwardl. apply ImpLAnd, IHW.
    * otac Heq.
    * apply BoxR with (Δ := Δ) in HPφ. apply ImpLAnd_rev. backwardl. rewrite HH. peapply HPφ.
    * backwardl. rewrite env_add_remove. exact HPΔ.
  + forwardl. apply ImpLOr, IHW.
    * otac Heq.
    * apply BoxR with (Δ := Δ) in HPφ. apply ImpLOr_rev. backwardl. rewrite HH. peapply HPφ.
    * backwardl. rewrite env_add_remove. exact HPΔ.
  + forwardl. apply ImpLImp.
    * apply IHW.
      -- otac Heq.
      -- exchl 0. apply ImpLImp_prev'. backwardl. rwl (symmetry Heq). apply BoxR, HPφ.
      -- exchl 0. exchl 0. backwardl. rewrite env_add_remove. exact HPΔ1.
    * apply IHW.
      -- otac Heq.
      -- box_tac. exchl 0. apply ImpLImp_prev'. apply BoxR. apply open_boxes_R.
         apply In_open_boxes in Hin0. simpl in Hin0.
         exchl 0. backwardl.
         lazy_apply HPφ. now rewrite Heq, open_boxes_remove, open_boxes_add by ms.
      -- assert(φ0 ∈ ⊗ Γ0) by now apply In_open_boxes in Hin0.
        apply IHw with φ0.
        ++ simpl in Hw; lia.
        ++ exchr 0. apply weakeningr. box_tac.
           exchl 0; exchl 1; exchl 0. apply ImpLImp_prev'.
           backwardl. lazy_apply HPφ.
           rewrite Heq, open_boxes_remove; ms.
        ++ box_tac. backwardl. rewrite env_add_remove. apply weakeningl, HPΔ2.
    * apply IHW.
      -- otac Heq.
      -- apply imp_cut with (φ1 → φ2). backwardl. rwl (symmetry Heq).
         apply BoxR, HPφ.
      -- backwardl. rewrite env_add_remove. exact HPΔ3.
  + (* (VIII-b) *)
      forwardl. apply ImpLBox.
     * (* π0 *)
        apply IHW.
      -- otac Heq.
      -- apply ImpLBox_prev with (φ1 := φ1).
          exchl 0. apply weakeningl.
          apply open_boxes_R. backwardl. rwl (symmetry Heq). apply BoxR, HPφ.
      -- (* π1 *)
          apply (IHw φ0).
          ++ simpl in Hw. lia.
          ++ exchl 1; exchl 0. apply weakeningl.
             exchl 0. apply ImpLBox_prev with (φ1 := φ1). exchl 0.
             replace (□ φ1 → φ2) with (⊙ (□ φ1 → φ2)) by trivial.
             rewrite <- (open_boxes_add (Γ0 ∖ {[□φ0]}) (□ φ1 → φ2)).
             assert(Heq0 : (Γ0 ∖ {[□ φ0]} • (□ φ1 → φ2)) ≡ Γ)
                by (rewrite Heq; now rewrite env_replace).
             rwl (proper_open_boxes _ _ Heq0). exchr 0. apply weakeningr. exact HPφ.
          ++ box_tac. exchl 0. apply weakeningl. exchl 0. exchl 1.
             assert(Hin1 : φ0 ∈ ⊗ Γ0) by(apply In_open_boxes in Hin0; now simpl).
             rwl difference_singleton. exact HPΔ1.
     * apply IHW.
      -- otac Heq.
      -- apply ImpLBox_prev with (φ1 := φ1). backwardl.
          rwl (symmetry Heq). apply BoxR, HPφ.
      -- backwardl. rewrite env_add_remove. exact HPΔ2.
  + (* (VIII-c) *)
      subst. rwl (symmetry Heq). rewrite open_boxes_add in HPΔ. simpl in HPΔ.
      apply BoxR. apply IHW.
    * otac Heq.
    * apply open_boxes_R, weakeningl, BoxR, HPφ.
    * apply (IHw φ0).
      -- simpl in Hw. lia.
      -- exchl 0. apply weakeningl. exchr 0. apply weakeningr, HPφ.
      -- exchl 0. apply weakeningl. exchl 0. exact HPΔ.
Qed.

Theorem additive_cut (φ : form) (Γ Δ : env) :
  Γ ⊢ ∅ • φ -> Γ • φ ⊢ Δ ->
  Γ ⊢ Δ.
Proof.
intros H1 H2. apply symmetric_cut with φ; trivial.
apply generalised_weakeningrL. rpeapply H1.
Qed.

(* Multiplicative cut rule *)
Theorem cut φ Γ Γ' Δ Δ' :
   Γ ⊢ Δ • φ -> Γ' • φ ⊢ Δ' ->
   Γ ⊎ Γ' ⊢ Δ ⊎ Δ'.
Proof.
intros H H'.
apply symmetric_cut with φ.
- apply generalised_weakeninglR.
  replace (Δ ⊎ Δ' • φ) with ((Δ • φ) ⊎ Δ') by ms.
  apply generalised_weakeningrR, H.
- replace (Γ ⊎ Γ' • φ) with ((Γ' • φ) ⊎ Γ) by ms.
  apply generalised_weakeninglR.
  apply generalised_weakeningrL, H'.
Qed.