Require Import List Permutation Arith.

From Undecidability.Shared.Libs.DLW
  Require Import utils pos vec.

From Undecidability.ILL Require Import ILL EILL ill.

Set Implicit Arguments.

Local Infix "~p" := (@Permutation _) (at level 70).


Notation "⦑ c ⦒" := (eill_cmd_map c) (at level 0).

Notation "Σ ; Γ ⊦ u" := (G_eill Σ Γ u) (at level 70, no associativity).

Theorem g_eill_mono_Si Σ Σ' Γ u : incl Σ Σ' -> Σ; Γ ⊦ u -> Σ'; Γ ⊦ u.
Proof.
  revert Σ Σ' Γ; intros Si Si' Ga.
  intros H H1; revert H1 Si' H.
  induction 1 as [ u
                 | Ga De p H1 H2 IH2
                 | Ga a p q H1 H2 IH2
                 | Ga De p q r H1 H2 IH2 H3 IH3
                 | Ga p q r H1 H2 IH2 H3 IH3
                 ]; intros Si' HSi.
  + apply in_geill_ax.
  + apply in_geill_perm with (1 := H1); auto.
  + apply in_geill_inc with (1 := HSi _ H1); auto.
  + apply in_geill_dec with (1 := HSi _ H1); auto.
  + apply in_geill_fork with (1 := HSi _ H1); auto.
Qed.


Notation "Γ ⊢ A" := (S_ill_restr Γ A) (at level 70, no associativity).

Theorem G_eill_sound Σ Γ p : Σ; Γ ⊦ p -> map (fun c => !⦑c⦒) Σ ++ map £ Γ ⊢ £ p.
Proof.
  revert Σ; intros Si.
  induction 1 as [ u
                 | Ga De p H1 H2 IH2
                 | Ga a p q H1 H2 IH2
                 | Ga De p q r H1 H2 IH2 H3 IH3
                 | Ga p q r H1 H2 IH2 H3 IH3
                 ].
  + rewrite <- map_map; apply S_ill_restr_weak; apply in_ill1_ax.
  + revert IH2; apply in_ill1_perm.
    apply Permutation_app; auto.
    apply Permutation_map; auto.
  + rewrite <- map_map; apply S_ill_restr_weak_cntr with (1 := in_map _ _ _ H1); simpl.
    rewrite map_map.
    apply in_ill1_bang_l.
    apply in_ill1_perm with (((£ a ⊸ £ p) ⊸ £ q) :: ((map (fun c => !⦑c⦒) Si ++ map £ Ga) ++ nil)).
    * rewrite <- app_nil_end; auto.
    * apply in_ill1_limp_l.
      2: apply in_ill1_ax.
      apply in_ill1_limp_r.
      revert IH2; apply in_ill1_perm.
      simpl; apply Permutation_sym, Permutation_cons_app; auto.
  + rewrite <- map_map.
    apply S_ill_restr_cntr.
    rewrite map_map.
    rewrite <- map_map; apply S_ill_restr_weak_cntr with (1 := in_map _ _ _ H1); simpl; rewrite map_map.
    apply in_ill1_bang_l.
    rewrite map_app.
    apply in_ill1_perm with (£ p ⊸ £ q ⊸ £ r :: (map (fun c => !⦑c⦒) Si ++ map £ Ga)
                                             ++ (map (fun c => !⦑c⦒) Si ++ map £ De)).
    * apply Permutation_cons; auto.
      rewrite app_ass; apply Permutation_app; auto.
      do 2 rewrite <- app_ass; apply Permutation_app; auto.
      apply Permutation_app_comm.
    * apply in_ill1_limp_l; auto.
      apply in_ill1_perm with (£ q ⊸ £ r :: ((map (fun c => !⦑c⦒) Si ++ map £ De) ++ nil)).
      - rewrite <- app_nil_end; auto.
      - apply in_ill1_limp_l; auto.
        apply in_ill1_ax.
  + rewrite <- map_map; apply S_ill_restr_weak_cntr with (1 := in_map _ _ _ H1); simpl.
    rewrite map_map.
    apply in_ill1_bang_l.
    apply in_ill1_perm with (£ p & £ q ⊸ £ r :: ((map (fun c => !⦑c⦒) Si ++ map £ Ga) ++ nil)).
    * rewrite <- app_nil_end; auto.
    * apply in_ill1_limp_l.
      - apply in_ill1_with_r; auto.
      - apply in_ill1_ax.
Qed.

Section TPS.

  Variables (n : nat) (s : ill_vars -> vec nat n -> Prop) (rx : pos n -> ill_vars).

  Fact ill_tps_vec_map_list_mono :
       (forall (p : pos n), s (rx p) (vec_one p))
     -> forall v, ill_tps_list s (map £ (vec_map_list v rx)) v.
  Proof.
    intros H v; rewrite map_vec_map_list.
    induction v as [ | p | v w Hv Hw ] using (@vec_nat_induction n).
    + rewrite vec_map_list_zero; simpl; tauto.
    + rewrite vec_map_list_one; simpl.
      exists (vec_one p), vec_zero; rew vec; repeat split; auto.
    + apply ill_tps_perm with (1 := Permutation_sym (vec_map_list_plus _ _ _)).
      apply ill_tps_app.
      exists v, w; repeat split; auto.
  Qed.

  Fact ill_tps_vec_map_list :
       (forall (p : pos n) (v : vec nat n), s (rx p) v <-> v = vec_one p)
     -> forall v w, ill_tps_list s (map £ (vec_map_list v rx)) w <-> v = w.
  Proof.
    intros H v; rewrite map_vec_map_list.
    induction v as [ | p | v w Hv Hw ] using (@vec_nat_induction n); intros z.
    + rewrite vec_map_list_zero; simpl; tauto.
    + rewrite vec_map_list_one; simpl.
      split.
      * intros (a & b & H1 & H2 & H3).
        apply H in H2; subst; rew vec.
      * intros [].
        exists (vec_one p), vec_zero; rew vec; repeat split; auto.
        apply H; auto.
    + split.
      * intros Hz.
        apply ill_tps_perm with (1 := vec_map_list_plus _ _ _) in Hz.
        apply ill_tps_app in Hz.
        destruct Hz as (a & b & H1 & H2 & H3).
        apply Hv in H2.
        apply Hw in H3.
        subst; auto.
      * intros [].
        apply ill_tps_perm with (1 := Permutation_sym (vec_map_list_plus _ _ _)).
        apply ill_tps_app.
        exists v, w; repeat split; auto.
        - apply Hv; auto.
        - apply Hw; auto.
  Qed.

End TPS.

Section g_eill_complete_bound.

  Variable (Σ : list eill_cmd) (Γ : list eill_vars) (n : nat).

  Notation vars := (flat_map eill_cmd_vars Σ ++ Γ).


  Hypothesis (w : vec eill_vars n)
             (w_surj : forall u, In u vars -> exists p, u = vec_pos w p).

  Let rx p := vec_pos w p.

  Let Hrx l : incl l (flat_map eill_cmd_vars Σ ++ Γ) -> exists v, l ~p vec_map_list v rx.
  Proof.
    induction l as [ | x l IHl ]; intros H.
    + exists vec_zero; rewrite vec_map_list_zero; auto.
    + destruct IHl as (v & Hv).
      { intros ? ?; apply H; right; auto. }
      assert (In x vars) as Hx.
      { apply H; left; auto. }
      destruct w_surj with (u := x)
        as (p & ?); subst; auto.
      exists (vec_plus (vec_one p) v).
      apply Permutation_sym.
      apply Permutation_trans with (1 := vec_map_list_plus _ _ _).
      rewrite vec_map_list_one.
      apply perm_skip, Permutation_sym; auto.
  Qed.

  Let s x v := Σ; vec_map_list v rx ⊦ x.

  Notation "⟦ A ⟧" := (ill_tps s A) (at level 65).
  Notation "'[<' Γ '|-' A '>]'" := (ill_sequent_tps s Γ A) (at level 65).

  Theorem G_eill_complete_bound x :
            [< map (fun c => !⦑c⦒) Σ ++ map £ Γ |- £ x >] vec_zero
         -> Σ; Γ ⊦ x.
  Proof.
    intros H.
    do 2 red in H.
    destruct (@Hrx Γ) as (v & Hv).
    1: { intros ? ?; apply in_or_app; right; auto. }
    apply in_geill_perm with (1 := Permutation_sym Hv).
    fold (s x v).
    rewrite <- (vec_zero_plus v), vec_plus_comm.
    apply H.
    rewrite ill_tps_app.
    exists vec_zero, v.
    repeat split; auto; try (rew vec; fail).
    2:{ apply ill_tps_perm with (map £ (vec_map_list v (fun p => rx p))).
        apply Permutation_map, Permutation_sym; auto.
        apply ill_tps_vec_map_list_mono; auto.
        intros p.
        red.
        rewrite vec_map_list_one.
        apply in_geill_ax. }

    rewrite <- map_map.
    apply ill_tps_list_bang_zero.
    intros A HA.
    apply in_map_iff in HA.
    destruct HA as (c & H1 & H2); subst.
    destruct c as [ a p q | a p q | p q r ]; simpl.


    + intros y Hy; rew vec; unfold s.
      apply in_geill_inc with a p; auto.
      destruct (@Hrx (a::nil)) as (z & Hz).
      intros ? [ [] | [] ]; apply in_or_app; left.
      * apply in_flat_map; exists (LL_INC a p q); simpl; auto.
      * apply in_geill_perm with (vec_map_list (vec_plus z y) rx).
        - apply Permutation_trans with (1 := vec_map_list_plus _ _ _).
          change (a::vec_map_list y rx) with ((a::nil)++vec_map_list y rx).
          apply Permutation_app; auto.
          apply Permutation_sym; auto.
        - apply Hy; red.
          apply in_geill_perm with (1 := Hz), in_geill_ax.


    + intros u Hu y Hy.
      rew vec.
      rewrite vec_plus_comm.
      apply in_geill_perm with (1 := Permutation_sym (vec_map_list_plus _ _ _)).
      apply in_geill_dec with a p; auto.


    + intros u (H3 & H4).
      rew vec.
      apply in_geill_fork with p q; auto.
  Qed.

End g_eill_complete_bound.

Section g_eill_complete.

  Variable (Σ : list eill_cmd) (Γ : list eill_vars).

  Notation vars := (flat_map eill_cmd_vars Σ ++ Γ).

  Let vv := nat_sort vars.

  Let Hvv1 : list_injective vv.
  Proof. apply nat_sorted_injective, nat_sort_sorted. Qed.

  Let Hvv2 : incl vv (flat_map eill_cmd_vars Σ ++ Γ)
          /\ incl (flat_map eill_cmd_vars Σ ++ Γ) vv.
  Proof. apply nat_sort_eq. Qed.

  Let n := length vv.
  Let w : vec eill_vars n := proj1_sig (list_vec_full vv).
  Let Hw : vec_list w = vv.
  Proof. apply (proj2_sig (list_vec_full vv)). Qed.

  Let w_surj : forall u, In u vars -> exists p, u = vec_pos w p.
  Proof.
    intros u Hu.
    apply Hvv2 in Hu; rewrite <- Hw in Hu.
    revert Hu; apply vec_list_inv.
  Qed.

  Variables (x : eill_vars)
            (Hvalid : forall n s, @ill_sequent_tps n s (map (fun c => !⦑c⦒) Σ ++ map £ Γ) (£ x) vec_zero).

  Theorem G_eill_complete : Σ; Γ ⊦ x.
  Proof.
    apply G_eill_complete_bound with (1 := w_surj), Hvalid.
  Qed.

End g_eill_complete.

From Undecidability.ILL Require Import CLL ill_cll schellinx.

Fact eill_no_bot c : ~ ill_has_bot ⦑ c ⦒.
Proof. induction c; simpl; tauto. Qed.


Section correctness_results_for_the_reduction.

  Variables (Σ : list eill_cmd) (Γ : list eill_vars) (u : nat).

  Notation Σi := (map (fun c => ill_ban ⦑c⦒) Σ).
  Notation Γi := (map ill_var Γ).
  Notation ui := (ill_var u).

  Notation Σc := (map (fun c => cll_una cll_bang [⦑c⦒]) Σ).
  Notation Γc := (map cll_var Γ).
  Notation uc := (cll_var u).

  Theorem G_eill_correct : (Σ; Γ ⊦ u -> S_ill_restr (Σi++Γi) ui)
                        /\ (S_ill_restr (Σi++Γi) ui -> S_ill_restr_wc (Σi++Γi) ui)
                        /\ (S_ill_restr (Σi++Γi) ui -> S_ill (Σi++Γi) ui)
                        /\ (S_ill_restr_wc (Σi++Γi) ui -> S_ill_wc (Σi++Γi) ui)
                        /\ (S_ill (Σi++Γi) ui -> S_ill_wc (Σi++Γi) ui)
                        /\ (S_ill_wc (Σi++Γi) ui -> Σ; Γ ⊦ u).
  Proof.
    msplit 5.
    + apply G_eill_sound.
    + apply S_ill_restr_restr_wc.
    + apply S_ill_restr_full.
    + apply S_ill_restr_full_wc.
    + apply S_ill_full_wc.
    + intro; apply G_eill_complete.
      intros; now apply ill_tps_sound.
  Qed.

  Tactic Notation "solve" "with" int(i) int(j) :=
    let H := fresh in split; [ intro; now do i apply G_eill_correct
                             | intros H; now do j apply G_eill_correct in H ].


  Corollary G_eill_S_ill_restr : Σ; Γ ⊦ u <-> S_ill_restr (Σi++Γi) ui.
  Proof. solve with 1 3. Qed.


  Corollary G_eill_S_ill_restr_wc : Σ; Γ ⊦ u <-> S_ill_restr_wc (Σi++Γi) ui.
  Proof. solve with 2 2. Qed.


  Corollary G_eill_S_ill : Σ; Γ ⊦ u <-> S_ill (Σi++Γi) ui.
  Proof. solve with 2 2. Qed.


  Corollary G_eill_S_ill_wc : Σ; Γ ⊦ u <-> S_ill_wc (Σi++Γi) ui.
  Proof. solve with 3 1. Qed.

  Let not_bot f : In f (ui :: Σi ++ Γi) -> ~ ill_has_bot f.
  Proof.
    simpl; rewrite in_app_iff, !in_map_iff.
    intros [ <- | [ (? & <- & ?) | (? & <- & ?) ] ];
      simpl; auto; apply eill_no_bot.
  Qed.

  Theorem G_eill_S_cll : Σ; Γ ⊦ u <-> S_cll (Σc++Γc) (uc::nil).
  Proof.
    split.
    + rewrite G_eill_S_ill.
      intros H.
      rewrite ill_cll_equiv in H; auto.
      eq goal H; f_equal.
      now rewrite map_app, !map_map.
    + intros H.
      apply G_eill_S_ill, ill_cll_equiv; auto.
      eq goal H; f_equal.
      now rewrite map_app, !map_map.
  Qed.

End correctness_results_for_the_reduction.