(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Permutation Arith Omega.

Require Import utils pos vec.

Set Implicit Arguments.

(** * Intuionistic Linear Logic *)

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

Definition ll_vars := nat.

(** We only consider the fragment of ILL which
   contains !, -o and & ... 
 
   ILL can be faithfully embedded into that fragment 
   but this does not matter for undecidability 
*)

Inductive ll_conn := ll_with | ll_limp | ll_times | ll_plus.
Inductive ll_cst := ll_one | ll_bot | ll_top.

Inductive ll_form : Set :=
  | ll_var  : ll_vars -> ll_form
  | ll_zero : ll_cst  -> ll_form
  | ll_ban  : ll_form -> ll_form
  | ll_bin  : ll_conn -> ll_form -> ll_form -> ll_form.

(* Symbols for cut&paste ⟙   ⟘   𝝐  ﹠ ⊗  ⊕  ⊸  ❗   ‼  ∅  ⊢ *)

Notation "⟙" := (ll_zero ll_top).
Notation "⟘" := (ll_zero ll_bot).
Notation 𝝐 := (ll_zero ll_one).

Infix "&" := (ll_bin ll_with) (at level 50, only parsing).
Infix "﹠" := (ll_bin ll_with) (at level 50).
Infix "⊗" := (ll_bin ll_times) (at level 50).
Infix "⊕" := (ll_bin ll_plus) (at level 50).
Infix "-o" := (ll_bin ll_limp) (at level 51, only parsing, right associativity).
Infix "⊸" := (ll_bin ll_limp) (at level 51, right associativity).

Notation "'!' x" := (ll_ban x) (at level 52, only parsing).
Notation "❗ x" := (ll_ban x) (at level 52).

Notation "£" := ll_var.

Definition ll_lbang := map (fun x => !x).

Notation "'!l' x" := (ll_lbang x) (at level 60, only parsing).
Notation "‼ x" := (ll_lbang x) (at level 60).

Notation "∅" := nil (only parsing).

Reserved Notation "l '⊢' x" (at level 70, no associativity).

Inductive S_ill : list ll_form -> ll_form -> Prop :=

  (* These are the SILL rules in the paper *)

  | in_llp_ax     : forall A,                         A::∅ ⊢ A

  | in_llp_perm   : forall Γ Δ A,              Γ ~p Δ     ->   Γ ⊢ A 
                                           (*-----------------------------*)
                                      ->                 Δ ⊢ A

  | in_llp_limp_l : forall Γ Δ A B C,          Γ ⊢ A      ->   B::Δ ⊢ C
                                           (*-----------------------------*)    
                                      ->           A ⊸ B::Γ++Δ ⊢ C

  | in_llp_limp_r : forall Γ A B,                    A::Γ ⊢ B
                                           (*-----------------------------*)
                                      ->            Γ ⊢ A ⊸ B

  | in_llp_with_l1 : forall Γ A B C,                  A::Γ ⊢ C 
                                           (*-----------------------------*)
                                      ->           A﹠B::Γ ⊢ C

  | in_llp_with_l2 : forall Γ A B C,                  B::Γ ⊢ C 
                                           (*-----------------------------*)
                                      ->           A﹠B::Γ ⊢ C
 
  | in_llp_with_r : forall Γ A B,               Γ ⊢ A     ->   Γ ⊢ B
                                           (*-----------------------------*)
                                      ->              Γ ⊢ A﹠B

  | in_llp_bang_l : forall Γ A B,                    A::Γ ⊢ B
                                           (*-----------------------------*)
                                      ->            ❗ A::Γ ⊢ B

  | in_llp_bang_r : forall Γ A,                       ‼Γ ⊢ A
                                           (*-----------------------------*)
                                      ->              ‼Γ ⊢ ❗ A

  | in_llp_weak : forall Γ A B,                        Γ ⊢ B
                                           (*-----------------------------*)
                                      ->           ❗ A::Γ ⊢ B

  | in_llp_cntr : forall Γ A B,                    ❗ A::❗ A::Γ ⊢ B
                                           (*-----------------------------*)
                                      ->             ❗ A::Γ ⊢ B

  (* These are the other rule for a complete sequent calculus for the whole ILL *)

  | in_llp_cut : forall Γ Δ A B,                 Γ ⊢ A    ->   A::Δ ⊢ B
                                           (*-----------------------------*)    
                                      ->              Γ++Δ ⊢ B

  | in_llp_times_l : forall Γ A B C,               A::B::Γ ⊢ C 
                                           (*-----------------------------*)
                                      ->            A⊗B::Γ ⊢ C
 
  | in_llp_times_r : forall Γ Δ A B,             Γ ⊢ A    ->   Δ ⊢ B
                                           (*-----------------------------*)
                                      ->              Γ++Δ ⊢ A⊗B

  | in_llp_plus_l :  forall Γ A B C,            A::Γ ⊢ C  ->  B::Γ ⊢ C 
                                           (*-----------------------------*)
                                      ->            A⊕B::Γ ⊢ C

  | in_llp_plus_r1 : forall Γ A B,                    Γ ⊢ A  
                                           (*-----------------------------*)
                                      ->              Γ ⊢ A⊕B

  | in_llp_plus_r2 : forall Γ A B,                    Γ ⊢ B  
                                           (*-----------------------------*)
                                      ->              Γ ⊢ A⊕B

  | in_llp_bot_l : forall Γ A,                     ⟘::Γ ⊢ A

  | in_llp_top_r : forall Γ,                          Γ ⊢ ⟙

  | in_llp_unit_l : forall Γ A,                       Γ ⊢ A  
                                           (*-----------------------------*)
                                      ->           𝝐 ::Γ ⊢ A

  | in_llp_unit_r :                                   ∅ ⊢ 𝝐

where "l ⊢ x" := (S_ill l x).

Definition ILL_PROVABILITY (c : (list ll_form) * ll_form) := let (Ga,A) := c in Ga ⊢ A. 

Fact S_ill_weak Γ Δ B : Δ ⊢ B -> ‼Γ++Δ ⊢ B.
(* Goal: forall _ : S_ill Δ B, S_ill (@app ll_form (ll_lbang Γ) Δ) B *)
Proof. intro; induction Γ; simpl; auto; apply in_llp_weak; auto. Qed.

Fact S_ill_cntr Γ Δ B : ‼Γ++‼Γ++Δ ⊢ B -> ‼Γ++ Δ ⊢ B.
Proof.
(* Goal: forall _ : S_ill (@app ll_form (ll_lbang Γ) (@app ll_form (ll_lbang Γ) Δ)) B, S_ill (@app ll_form (ll_lbang Γ) Δ) B *)
  revert Γ Δ; intros Ga.
(* Goal: forall (Δ : list ll_form) (_ : S_ill (@app ll_form (ll_lbang Ga) (@app ll_form (ll_lbang Ga) Δ)) B), S_ill (@app ll_form (ll_lbang Ga) Δ) B *)
  induction Ga as [ | A Ga IH ]; simpl; auto; intros De.
(* Goal: forall _ : forall (A0 : ll_form) (_ : @In ll_form A0 (@cons ll_form A Ga)), ll_tps A0 (@vec_zero n), ll_tps_list (ll_lbang (@cons ll_form A Ga)) (@vec_zero n) *)
  intros H.
(* Goal: S_ill (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De)) B *)
  apply in_llp_cntr.
(* Goal: S_ill (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De))) B *)
  apply in_llp_perm with (map ll_ban Ga ++ (!A::!A::De)).
  + apply Permutation_sym.
(* Goal: @Permutation ll_form (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De))) (@app ll_form (@map ll_form ll_form ll_ban Ga) (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) De))) *)
    do 2 apply Permutation_cons_app; auto.
  + apply IH.
(* Goal: S_ill (@app ll_form (ll_lbang Ga) (@app ll_form (ll_lbang Ga) (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) De)))) B *)
    revert H; apply in_llp_perm.
(* Goal: @Permutation ll_form (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De)))) (@app ll_form (ll_lbang Ga) (@app ll_form (ll_lbang Ga) (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) De)))) *)
    rewrite app_assoc.
(* Goal: @Permutation ll_form (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De)))) (@app ll_form (@app ll_form (ll_lbang Ga) (ll_lbang Ga)) (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) De))) *)
    apply Permutation_cons_app.
(* Goal: @Permutation ll_form (@app ll_form (ll_lbang Ga) (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De))) (@app ll_form (@app ll_form (ll_lbang Ga) (ll_lbang Ga)) (@cons ll_form (ll_ban A) De)) *)
    rewrite <- app_assoc.
(* Goal: @Permutation ll_form (@app ll_form (ll_lbang Si) Ga) (@app ll_form (ll_lbang (@cons ll_form A Si')) Ga) *)
    apply Permutation_app; auto.
(* Goal: @Permutation ll_form (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De)) (@app ll_form (ll_lbang Ga) (@cons ll_form (ll_ban A) De)) *)
    apply Permutation_cons_app; auto.
Qed.

Theorem S_ill_weak_cntr Σ Γ A B : In A Σ -> ‼Σ++Γ ⊢ B <-> ❗ A::‼Σ++Γ ⊢ B.
Proof.
(* Goal: forall _ : @In ll_form A Σ, iff (S_ill (@app ll_form (ll_lbang Σ) Γ) B) (S_ill (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Σ) Γ)) B) *)
  revert Σ Γ; intros Si Ga.
(* Goal: forall _ : forall (A0 : ll_form) (_ : @In ll_form A0 (@cons ll_form A Ga)), ll_tps A0 (@vec_zero n), ll_tps_list (ll_lbang (@cons ll_form A Ga)) (@vec_zero n) *)
  intros H.
(* Goal: iff (S_ill (@app ll_form (ll_lbang Si) Ga) B) (S_ill (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Si) Ga)) B) *)
  apply In_perm in H.
(* Goal: iff (S_ill (@app ll_form (ll_lbang Si) Ga) B) (S_ill (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Si) Ga)) B) *)
  destruct H as (Si' & H).
(* Goal: iff (ll_sequent_tps Γ A (@vec_zero n)) (forall (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps A x) *)
  split.
  + apply in_llp_weak.
  + intros H1.
    apply in_llp_perm with (‼(A :: Si') ++ Ga).
(* Goal: @Permutation ll_form (@app ll_form (ll_lbang Si) Ga) (@app ll_form (ll_lbang (@cons ll_form A Si')) Ga) *)
    * apply Permutation_app; auto.
(* Goal: @Permutation ll_form (ll_lbang (@cons ll_form A Si')) (ll_lbang Si) *)
      apply Permutation_map; auto.
(* Goal: S_ill (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Ga) De)) B *)
    * simpl; apply in_llp_cntr.
(* Goal: S_ill (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Si') Ga))) B *)
      revert H1; apply in_llp_perm.
(* Goal: @Permutation ll_form (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Si) Ga)) (@cons ll_form (ll_ban A) (@cons ll_form (ll_ban A) (@app ll_form (ll_lbang Si') Ga))) *)
      simpl; apply Permutation_cons; auto.
      change (❗ A::‼Si'++Ga) with (‼(A::Si')++Ga).
(* Goal: @Permutation ll_form (@app ll_form (ll_lbang Si) Ga) (@app ll_form (ll_lbang (@cons ll_form A Si')) Ga) *)
      apply Permutation_app; auto.
(* Goal: @Permutation ll_form (ll_lbang Si) (ll_lbang (@cons ll_form A Si')) *)
      apply Permutation_map, Permutation_sym; auto.
Qed.

Section trivial_phase_semantics.

  Variables (n : nat) (s : ll_vars -> vec nat n -> Prop).

  Reserved Notation "'⟦' A '⟧'" (at level 65).

  Definition ll_tps_imp (X Y : _ -> Prop) (v : vec _ n) := forall x, X x -> Y (vec_plus x v).
  Definition ll_tps_mult (X Y : _ -> Prop) (x : vec _ n) := exists a b, x = vec_plus a b /\ X a /\ Y b. 
  
  Infix "**" := (ll_tps_mult) (at level 65, right associativity).
  Infix "-*" := (ll_tps_imp) (at level 65, right associativity).

  Fact ll_tps_mult_mono (X1 X2 Y1 Y2 : _ -> Prop) : 
             (forall x, X1 x -> X2 x)
          -> (forall x, Y1 x -> Y2 x)
          -> (forall x, (X1**Y1) x -> (X2**Y2) x).
  Proof.
(* Goal: forall (_ : forall (x : vec nat n) (_ : X1 x), X2 x) (_ : forall (x : vec nat n) (_ : Y1 x), Y2 x) (x : vec nat n) (_ : ll_tps_mult X1 Y1 x), ll_tps_mult X2 Y2 x *)
    intros H1 H2 x (a & b & H3 & H4 & H5); subst.
(* Goal: ll_tps_mult X2 Y2 (@vec_plus n a b) *)
    exists a, b; auto.
  Qed.

  (* Symbols for cut&paste ⟙   ⟘   𝝐  ﹠ ⊗  ⊕  ⊸  ❗   ‼  ∅  ⊢ ⟦ ⟧ Γ Δ Σ*)

  Fixpoint ll_tps A x : Prop :=
    match A with
      | £ X     => s X x
      | A ﹠ B  => ⟦A⟧ x /\ ⟦B⟧ x
      | ❗ A     => ⟦A⟧ x /\ x = vec_zero
      | A ⊸ B  => (⟦A⟧ -* ⟦B⟧) x
      | A ⊗ B  => (⟦A⟧ ** ⟦B⟧) x
      | A ⊕ B  => ⟦A⟧ x \/ ⟦B⟧ x
      | ⟘             => False
      | ⟙             => True
      | 𝝐              => x = vec_zero
    end
  where "⟦ A ⟧" := (ll_tps A).

  Reserved Notation "'[[' Γ ']]'" (at level 0).

  Fixpoint ll_tps_list Γ :=
    match Γ with
      | ∅    => eq vec_zero
      | A::Γ => ⟦A⟧ ** [[Γ]]
    end
  where "[[ Γ ]]" := (ll_tps_list Γ).

  Fact ll_tps_app Γ Δ x : [[Γ++Δ]] x <-> ([[Γ]]**[[Δ]]) x.
  Proof.
(* Goal: iff (ll_tps_list (@app ll_form Γ Δ) x) (ll_tps_mult (ll_tps_list Γ) (ll_tps_list Δ) x) *)
    revert Γ Δ x; intros Ga De.
(* Goal: forall x : vec nat n, iff (ll_tps_list (@app ll_form Ga De) x) (ll_tps_mult (ll_tps_list Ga) (ll_tps_list De) x) *)
    induction Ga as [ | A Ga IH ]; intros x; simpl; split; intros Hx.
    + exists vec_zero, x; simpl; rew vec.
    + destruct Hx as (a & b & H1 & H2 & H3); subst; auto; rewrite vec_zero_plus; auto.
    + destruct Hx as (a & b & H1 & H2 & H3).
(* Goal: ll_tps_mult (ll_tps_mult (ll_tps A) (ll_tps_list Ga)) (ll_tps_list De) x *)
      apply IH in H3.
(* Goal: ll_tps_mult (ll_tps_mult (ll_tps A) (ll_tps_list Ga)) (ll_tps_list De) x *)
      destruct H3 as (c & d & H4 & H5 & H6).
(* Goal: iff (ll_sequent_tps Γ A (@vec_zero n)) (forall (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps A x) *)
      exists (vec_plus a c), d; split.
      * subst; apply vec_plus_assoc.
      * split; auto.
(* Goal: ll_tps_mult (ll_tps A) (ll_tps_list Ga) (@vec_plus n a c) *)
        exists a, c; auto.
    + destruct Hx as (y & d & H1 & H2 & H3).
(* Goal: ll_tps_mult (ll_tps A) (ll_tps_list (@app ll_form Ga De)) x *)
      destruct H2 as (a & g & H2 & H4 & H5).
(* Goal: iff (ll_sequent_tps Γ A (@vec_zero n)) (forall (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps A x) *)
      exists a, (vec_plus g d); split.
      * subst; symmetry; apply vec_plus_assoc.
      * split; auto.
(* Goal: ll_tps_list (@app ll_form Ga De) (@vec_plus n g d) *)
        apply IH.
(* Goal: ll_tps_mult (ll_tps_list Ga) (ll_tps_list De) (@vec_plus n g d) *)
        exists g, d; auto.
  Qed.

  Fact ll_tps_lbang Γ x : [[‼Γ]] x <-> [[Γ]] x /\ x = vec_zero.
  Proof.
(* Goal: iff (ll_tps_list (ll_lbang Γ) x) (and (ll_tps_list Γ x) (@eq (vec nat n) x (@vec_zero n))) *)
    revert Γ x; intros Ga.
(* Goal: forall x : vec nat n, iff (ll_tps_list (ll_lbang Ga) x) (and (ll_tps_list Ga x) (@eq (vec nat n) x (@vec_zero n))) *)
    induction Ga as [ | A Ga IH ]; intros x.
    + simpl; split; auto; tauto.
    + split.
      * intros (a & g & H1 & H2 & H3).
(* Goal: iff (ll_sequent_tps Γ A (@vec_zero n)) (forall (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps A x) *)
        split.
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
        - exists a, g; repeat split; auto.
          ** apply H2.
          ** apply IH; auto.
        - apply IH, proj2 in H3.
(* Goal: @eq (vec nat n) x (@vec_zero n) *)
          apply proj2 in H2; subst; auto.
(* Goal: @eq (vec nat n) (@vec_plus n (@vec_zero n) (@vec_zero n)) (@vec_zero n) *)
          apply vec_zero_plus.
      * intros ((a & g & H1 & H2 & H3) & H4).
(* Goal: ll_tps_list (ll_lbang (@cons ll_form A Ga)) x *)
        exists x, x.
(* Goal: and (@eq (vec nat n) x (@vec_plus n x x)) (and (ll_tps (ll_ban A) x) (ll_tps_list (ll_lbang Ga) x)) *)
        assert (a = vec_zero /\ g = vec_zero) as E.
(* Goal: and (@eq (vec nat n) a (@vec_zero n)) (@eq (vec nat n) g (@vec_zero n)) *)
(* Goal: and (@eq (vec nat n) x (@vec_plus n x x)) (and (ll_tps (ll_ban A) x) (ll_tps_list (ll_lbang Ga) x)) *)
        { apply vec_plus_is_zero; subst; auto. }
(* Goal: and (@eq (vec nat n) x (@vec_plus n x x)) (and (ll_tps (ll_ban A) x) (ll_tps_list (ll_lbang Ga) x)) *)
        destruct E; subst; repeat split; auto; rew vec.
(* Goal: ll_tps_list (ll_lbang Ga) (@vec_zero n) *)
        apply IH; auto.
  Qed.

  Fact ll_tps_list_bang_zero Γ : [[‼Γ]] vec_zero <-> forall A, In A Γ -> ⟦A⟧ vec_zero.
  Proof.
(* Goal: iff (ll_tps_list (ll_lbang Γ) (@vec_zero n)) (forall (A : ll_form) (_ : @In ll_form A Γ), ll_tps A (@vec_zero n)) *)
    induction Γ as [ | A Ga IH ].
    + split.
      * simpl; tauto.
      * intros _; simpl; auto.
    + split.
      * intros (u & v & H1 & H2 & H3).
(* Goal: forall (A0 : ll_form) (_ : @In ll_form A0 (@cons ll_form A Ga)), ll_tps A0 (@vec_zero n) *)
        destruct H2 as [ H2 H4 ]; subst; auto.
(* Goal: forall (A0 : ll_form) (_ : @In ll_form A0 (@cons ll_form A Ga)), ll_tps A0 (@vec_zero n) *)
        rewrite vec_zero_plus in H1; subst.
(* Goal: forall (A0 : ll_form) (_ : @In ll_form A0 (@cons ll_form A Ga)), ll_tps A0 (@vec_zero n) *)
        rewrite IH in H3.
(* Goal: forall (A0 : ll_form) (_ : @In ll_form A0 (@cons ll_form A Ga)), ll_tps A0 (@vec_zero n) *)
        intros B [ E | HB ]; subst; auto.
(* Goal: forall _ : forall (A0 : ll_form) (_ : @In ll_form A0 (@cons ll_form A Ga)), ll_tps A0 (@vec_zero n), ll_tps_list (ll_lbang (@cons ll_form A Ga)) (@vec_zero n) *)
      * intros H.
(* Goal: ll_tps_list (ll_lbang (@cons ll_form A Ga)) (@vec_zero n) *)
        exists vec_zero, vec_zero.
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
        rewrite vec_zero_plus; repeat split; auto.
        - apply H; left; auto.
        - rewrite IH.
(* Goal: forall (A : ll_form) (_ : @In ll_form A Ga), ll_tps A (@vec_zero n) *)
          intros; apply H; right; auto.
  Qed.

  (* Symbols for cut&paste ⟙   ⟘   𝝐  ﹠ ⊗  ⊕  ⊸  ❗   ‼  ∅  ⊢ ⟦ ⟧ Γ Δ Σ*)
 
  Fact ll_tps_perm Γ Δ : Γ ~p Δ -> forall x, [[Γ]] x -> [[Δ]] x.
  Proof.
(* Goal: forall (_ : @Permutation ll_form Γ Δ) (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps_list Δ x *)
    induction 1 as [ | A Ga De H IH | A B Ga | ]; simpl; auto.
    + intros x (a & b & H1 & H2 & H3).
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
      exists a, b; repeat split; auto.
    + intros x (a & b & H1 & H2 & c & d & H3 & H4 & H5).
(* Goal: iff (ll_sequent_tps Γ A (@vec_zero n)) (forall (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps A x) *)
      exists c, (vec_plus a d); split.
      * subst; rewrite (vec_plus_comm c), vec_plus_assoc, (vec_plus_comm c); auto.
      * split; auto.
(* Goal: ll_tps_mult (ll_tps B) (ll_tps_list Ga) (@vec_plus n a d) *)
        exists a, d; auto.
  Qed.
  
  Definition ll_sequent_tps Γ A := [[Γ]] -* ⟦A⟧.

  Notation "'[<' Γ '|-' A '>]'" := (ll_sequent_tps Γ A).

  Fact ll_sequent_tps_mono Γ A B :
     (forall x, ⟦A⟧ x -> ⟦B⟧ x) -> forall x, [< Γ |- A >] x -> [< Γ |- B >] x.
  Proof.
(* Goal: forall (_ : forall (x : vec nat n) (_ : ll_tps A x), ll_tps B x) (x : vec nat n) (_ : ll_sequent_tps Γ A x), ll_sequent_tps Γ B x *)
    intros H x; simpl; unfold ll_sequent_tps.
(* Goal: forall _ : ll_tps_imp (ll_tps_list Γ) (ll_tps A) x, ll_tps_imp (ll_tps_list Γ) (ll_tps B) x *)
    intros H1 a H2.
(* Goal: ll_tps B (@vec_plus n a x) *)
    apply H, H1; auto.
  Qed.

  Fact ll_perm_tps Γ Δ : Γ ~p Δ -> forall x A, [< Γ |- A >] x -> [< Δ |- A >] x.
  Proof.
(* Goal: forall (_ : @Permutation ll_form Γ Δ) (x : vec nat n) (A : ll_form) (_ : ll_sequent_tps Γ A x), ll_sequent_tps Δ A x *)
    intros H1 x B; unfold ll_sequent_tps.
(* Goal: forall _ : ll_tps_imp (ll_tps_list Γ) (ll_tps B) x, ll_tps_imp (ll_tps_list Δ) (ll_tps B) x *)
    intros H2 a H3.
(* Goal: ll_tps B (@vec_plus n a x) *)
    apply H2; revert H3. 
(* Goal: forall _ : ll_tps_list Δ a, ll_tps_list Γ a *)
    apply ll_tps_perm, Permutation_sym; auto.
  Qed.

  Fact ll_sequent_tps_eq  Γ A : [< Γ |- A >] vec_zero <-> forall x, [[Γ]] x -> ⟦A⟧ x.
  Proof.
(* Goal: iff (ll_sequent_tps Γ A (@vec_zero n)) (forall (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps A x) *)
    split.
    * intros H x Hx.
      rewrite <- vec_zero_plus, vec_plus_comm.
(* Goal: ll_tps A (@vec_plus n x (@vec_zero n)) *)
      apply (H x); trivial.
    * intros H x Hx.
(* Goal: @eq (vec nat n) (@vec_plus n (@vec_plus n a b) (@vec_zero n)) (@vec_plus n a b) *)
      rewrite vec_plus_comm, vec_zero_plus; auto.
  Qed.

  Theorem ll_tps_sound Γ A : Γ ⊢ A -> [< Γ |- A >] vec_zero.
  Proof.
    induction 1 as [ A 
                   | Ga De A H1 H2 IH2
                   | Ga De A B C H1 IH1 H2 IH2
                   | Ga A B H1 IH1
                   | Ga A B C H1 IH1
                   | Ga A B C H1 IH1
                   | Ga A B H1 IH1 H2 IH2
                   | Ga A B H1 IH1 
                   | Ga A H1 IH1
                   | Ga A B H1 IH1
                   | Ga A B H1 IH1

                   | Ga De A B H1 IH1 H2 IH2
                   | Ga A B C H1 IH1
                   | Ga De A B H1 IH1 H2 IH2
                   | Ga A B C H1 IH1 H2 IH2
                   | Ga A B H1 IH1
                   | Ga A B H1 IH1
                   | Ga A
                   | Ga
                   | Ga A H1 IH1
                   |
                   ]; unfold ll_sequent_tps in * |- *.

    + intros x; simpl; intros (a & b & H1 & H2 & H3); subst; eq goal H2.
(* Goal: @eq (vec nat n) (@vec_plus n (@vec_plus n a b) (@vec_zero n)) (@vec_plus n a b) *)
      f_equal; do 2 rewrite vec_plus_comm, vec_zero_plus; auto.

    + revert IH2; apply ll_perm_tps; auto.

    + intros x (y & z & H3 & H4 & H5); simpl.
(* Goal: ll_tps B (@vec_plus n x (@vec_zero n)) *)
      apply IH2.
(* Goal: ll_tps_list (@cons ll_form B De) x *)
      apply ll_tps_app in H5.
(* Goal: ll_tps_list (@cons ll_form B De) x *)
      destruct H5 as (g & d & H5 & H6 & H7).
(* Goal: ll_tps_list (@cons ll_form B De) x *)
      simpl in H4.
(* Goal: ll_tps_list (@cons ll_form B De) x *)
      apply IH1, H4 in H6.
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
      exists (vec_plus y g), d; repeat split; auto.
      * subst; apply vec_plus_assoc.
      * eq goal H6; f_equal; rew vec.

    + simpl; intros y Hy a Ha.
(* Goal: ll_tps B (@vec_plus n a (@vec_plus n y (@vec_zero n))) *)
      rewrite vec_plus_assoc.
(* Goal: ll_tps C (@vec_plus n x (@vec_zero n)) *)
      apply IH1.
(* Goal: ll_tps_list (@cons ll_form A Ga) (@vec_plus n a y) *)
      exists a, y; repeat split; auto; omega.

    + intros x (a & b & H2 & H3 & H4); apply IH1.
(* Goal: ll_tps_list (@cons ll_form B Ga) x *)
      exists a, b; repeat split; auto; apply H3.

    + intros x (a & b & H2 & H3 & H4); apply IH1.
(* Goal: ll_tps_list (@cons ll_form B Ga) x *)
      exists a, b; repeat split; auto; apply H3.

    + intros x Hx; split.
      * apply IH1; auto.
      * apply IH2; auto.
   
    + intros x (a & g & H2 & H3 & H4).
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
      apply IH1; exists a, g; repeat split; auto.
(* Goal: ll_tps A a *)
      apply H3.

    + intros x Hx; split.
(* Goal: ll_tps A (@vec_plus n g (@vec_zero n)) *)
      apply IH1; auto.
(* Goal: @eq (vec nat n) (@vec_plus n x (@vec_zero n)) (@vec_zero n) *)
      rew vec.
(* Goal: @eq (vec nat n) x (@vec_zero n) *)
      apply ll_tps_lbang in Hx; tauto.

    + intros x (a & g & H2 & H3 & H4).
(* Goal: ll_tps C (@vec_plus n x (@vec_zero n)) *)
      apply IH1.
(* Goal: ll_tps_list Ga x *)
      apply proj2 in H3; subst; auto.
(* Goal: ll_tps_list Ga (@vec_plus n (@vec_zero n) g) *)
      rew vec; auto.
  
    + intros x (a & g & H2 & H3 & H4).
(* Goal: ll_tps C (@vec_plus n x (@vec_zero n)) *)
      apply IH1.
(* Goal: ll_tps_list (@cons ll_form (ll_ban A) Ga) g *)
      exists a, g.
(* Goal: and (@eq (vec nat n) g (@vec_plus n a g)) (and (ll_tps (ll_ban A) a) (ll_tps_list Ga g)) *)
      repeat (split; auto).
(* Goal: ll_tps_list (@cons ll_form (ll_ban A) Ga) g *)
      exists a, g.
(* Goal: and (@eq (vec nat n) g (@vec_plus n a g)) (and (ll_tps (ll_ban A) a) (ll_tps_list Ga g)) *)
      repeat (split; auto).
(* Goal: @eq (vec nat n) g (@vec_plus n a g) *)
      apply proj2 in H3.
(* Goal: ll_tps_list Ga (@vec_plus n (@vec_zero n) g) *)
      subst; rew vec; auto.

    (* Cut Rule *)
 
    + intros x Hx.
(* Goal: ll_tps B (@vec_plus n x (@vec_zero n)) *)
      rewrite ll_tps_app in Hx.
(* Goal: ll_tps B (@vec_plus n x (@vec_zero n)) *)
      apply IH2.
(* Goal: ll_tps_list (@cons ll_form A De) x *)
      destruct Hx as (a & b & G1 & G2 & G3); subst.
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
      exists a, b; split; auto.
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
      split; auto.
      rewrite <- vec_zero_plus, vec_plus_comm.
(* Goal: ll_tps A (@vec_plus n g (@vec_zero n)) *)
      apply IH1; auto.

    (* ⊗ left *)

    + intros x Hx.
(* Goal: ll_tps C (@vec_plus n x (@vec_zero n)) *)
      apply IH1.
(* Goal: ll_tps_list (@cons ll_form A (@cons ll_form B Ga)) x *)
      destruct Hx as (c & g & ? & (a & b & ? & H2 & H3) & H4); subst.
(* Goal: and (ll_tps A a) (ll_tps_list De b) *)
      exists a, (vec_plus b g); split; auto.
      * rewrite vec_plus_assoc; trivial.
      * split; auto; exists b, g; auto.

    (* ⊗ right *)

    + intros x Hx.
(* Goal: ll_tps (ll_bin ll_times A B) (@vec_plus n x (@vec_zero n)) *)
      apply ll_tps_app in Hx.
(* Goal: ll_tps (ll_bin ll_times A B) (@vec_plus n x (@vec_zero n)) *)
      destruct Hx as (a & b & ? & H3 & H4); subst.
(* Goal: iff (ll_sequent_tps Γ A (@vec_zero n)) (forall (x : vec nat n) (_ : ll_tps_list Γ x), ll_tps A x) *)
      exists a, b; split.
      * rewrite vec_plus_comm, vec_zero_plus; auto.
      * split; rewrite <- vec_zero_plus, vec_plus_comm.
        - apply IH1; auto.
        - apply IH2; auto.

    (* ⊕ left & ⊕ right 1 & 2 *)

    + intros x Hx.
(* Goal: ll_tps C (@vec_plus n x (@vec_zero n)) *)
      destruct Hx as (u & g & ? & [ G1 | G1 ] & G2); subst.
      * apply IH1; exists u, g; auto.
      * apply IH2; exists u, g; auto.
    + intros x Hx; left; apply IH1; auto.
    + intros x Hx; right; apply IH1; auto.

    (* ⟘ left, ⟙ right *)

    + intros ? (? & _ & _ & [] & _).    
    + intros x _; red; trivial.

    (* 𝝐 unit left & right *)

    + intros x (i & g & ? & H2 & H3); subst.
(* Goal: ll_tps A (@vec_plus n (@vec_plus n i g) (@vec_zero n)) *)
      red in H2; subst.
(* Goal: ll_tps A (@vec_plus n (@vec_plus n (@vec_zero n) g) (@vec_zero n)) *)
      rewrite vec_zero_plus.
(* Goal: ll_tps A (@vec_plus n g (@vec_zero n)) *)
      apply IH1; auto.
    + intros x Hx; red in Hx; subst.
(* Goal: ll_tps (ll_zero ll_one) (@vec_plus n (@vec_zero n) (@vec_zero n)) *)
      rewrite vec_zero_plus; red; trivial.
  Qed.

  (* This semantics is NOT complete for ILL 
     or even the (!,&,-o) fragment but it is
     complete for the EILL fragment *)
  
End trivial_phase_semantics.
