(***********************************************************)
(*  This file is distributed under the terms of the        *)
(*    GNU Lesser General Public License version 3          *)
(*                                                         *)
(*        Copyright 2009-2010: Damien Pous.                *)
(*                                                         *)
(***********************************************************)

(** * Untyping theorems for:
   - #<a href="##mll"># cyclic MLL#</a>#, 
   - #<a href="##imll"># non commutative IMLL (residuated monoids)#</a>#.
   *)
(** The corresponding .v file (with proofs) is #<a href="mll.v">here</a>#;
   see module #<a href="utas.html">utas</a># for monoids, semirings, Kleene algebras, and allegories;
   and module #<a href="mall.html">mall</a># for cyclic MALL (or involutive residuated lattices) and residuated lattices (without additive constants).
*)

Require Import Relations List.
Require Import Program.
Require Import Setoid Morphisms.

Set Implicit Arguments.
Unset Printing Implicit Defensive.
Unset Strict Implicit.

(* inversion tactics *)
Ltac inversion' H := inversion H; subst; clear H.

(* useful lemma to exploit hypotheses *)
Definition apply A a B (f: A -> B) := f a.
Notation refl := (refl_equal _).


(** ** preliminary lemmas for working with cyclic permutations  *)
Section perm.

  Variable A: Set.

  Lemma app_app: forall (h k h' k': list A), h++k = h'++k' ->
    exists l', h=h'++l' /\ k'=l'++k \/ h'=h++l' /\ k=l'++k'.
  Proof.
    induction h; intros; destruct h'; simpl in *; dependent destruction H; eauto.
    specialize (IHh _ _ _ x). intuition; subst; auto.
    destruct IHh; intuition; subst; eauto.
  Qed.

  Lemma nil_app: forall (h k: list A), [] = h++k -> []=h /\ []=k.
  Proof.
    intros. destruct h; destruct k; auto; discriminate.
  Qed.

  Lemma consnil_app: forall u (h k: list A), [u] = h++k -> [u]=h /\ []=k \/ []=h /\ [u]=k.
  Proof.
    intros. destruct h; dependent destruction H; auto.
    apply nil_app in x. intuition; subst. auto.
  Qed.

  Lemma cons_app: forall u (l h k: list A), u::l = h++k -> []=h /\ u::l=k \/ exists h', h=u::h' /\ l=h'++k.
  Proof.
    intros. destruct h; dependent destruction H; eauto.
  Qed.

  Lemma split_select: forall (h k h' k': list A), h++k = h'++k' ->
    exists l', h=h'++l' /\ k'=l'++k \/ h'=h++l' /\ k=l'++k'.
  Proof.
    induction h; intros; destruct h'; simpl in *; dependent destruction H; eauto.
    specialize (IHh _ _ _ x). intuition; subst; auto.
    destruct IHh; intuition; subst; eauto.
  Qed.

  Inductive perm: relation (list A) :=
  | perm_app: forall h k, perm (h++k) (k++h).

  Global Instance perm_equivalence: Equivalence perm.
  Proof.
    constructor; red; intros.
     rewrite app_nil_end. apply (perm_app [] x).
     inversion' H. constructor.
     inversion' H. inversion' H0. apply app_app in H1 as [l ?]. intuition; subst.
      rewrite <- app_ass. rewrite app_ass at 1. constructor.
      rewrite app_ass. rewrite <- app_ass. constructor.
  Qed.

  Infix " (=) " := perm (at level 80).

  Lemma permut_cons: forall u l k, l++[u] (=) k -> u::l (=) k.
  Proof. intros. rewrite perm_app in H. assumption. Qed.

  Lemma permut_app: forall h l k, l++h (=) k -> h++l (=) k.
  Proof. intros. rewrite perm_app. assumption. Qed.

  Lemma pmor1: forall P: list A -> Prop, (forall a l, P (l++[a]) -> P (a::l)) -> Proper (perm ==> iff) P.
  Proof.
   intros P HP.
   assert (forall k h, P (h++k) -> P (k++h)).
    induction k; intros.
     rewrite <- app_nil_end in H. assumption.
     simpl; apply HP. rewrite app_ass. apply IHk. rewrite app_ass. assumption.
   repeat intro. inversion' H0. split; auto. 
  Qed.

End perm.

(** equality of lists, modulo cyclic permutations *)
Infix " (=) " := perm (at level 80).
Hint Extern 0 (_ (=) _) => reflexivity.

(* tactic to solve cyclic permutations automatically *)
Hint Rewrite app_ass : permut_norm.
(* normalise concatenations (associativity), in goal and hypotheses *)
Ltac permut_norm := repeat (simpl in *; autorewrite with permut_norm in *).
(* rotate the left-hand side until reflexivity or until an assumption is obtained *)
Ltac solve_perm_aux :=
  permut_norm; solve [ auto | apply permut_cons; solve_perm_aux | apply permut_app; solve_perm_aux ].
(* final tactic: clear useless hypotheses *)
Ltac solve_perm :=
  repeat match goal with H: _ (=) _ |- _ => fail | H: _ |- _ => clear H end; solve_perm_aux.



(** [X] is the set of variables, it could be kept abstract *)
Definition X := nat. 

(** trivial typing environment *)
Definition ttt (x: X) := tt.


(** ** Untyping theorem for cyclic MLL #<a name=mll></a># *)
Module MLL.
  
  (** terms (formulae) *)
  Inductive T: Set :=
  | dot: T -> T -> T
  | par: T -> T -> T
  | one: T
  | bot: T
  | var: X -> T
  | rav: X -> T.
  
  (* is some term a ``constructed'' one, i.e., not a Coq variable; 
     this is useful to define some tactics below *)
  Ltac is_constr x := 
    match x with 
      | dot _ _ => idtac
      | par _ _ => idtac
      | var _ => idtac
      | rav _ => idtac
      | one => idtac
      | bot => idtac
      | [] => idtac
      | _::_ => idtac
    end.

  (** printing $ #<img alt="$" src="parr.png"/># *)
  (** notations *) (* $ means \parr *)
  Delimit Scope U_scope with U.
  Open Scope U_scope.
  Notation "x $ y"   := (par x y) (at level 50, left associativity): U_scope. 
  Notation "x ⨂ y"   := (dot x y) (at level 40, left associativity): U_scope. 
  Notation "1"       := (one): U_scope. 
  Notation "⊥"       := (bot): U_scope. 
  
  (** linear negation, note that it reverses arguments of tensors and pars *)
  Fixpoint dual u := 
    match u with
      | a ⨂ b => dual b $ dual a
      | a $ b => dual b ⨂ dual a
      | 1 => ⊥
      | ⊥ => 1
      | var i => rav i
      | rav i => var i
    end.
  
  (** linear negation is involutive, and hence, injective *)
  Lemma dual_invol: forall u, dual (dual u) = u.
  Proof.
    induction u; simpl; congruence.
  Qed.  

  Lemma dual_inj: forall u v, dual u = dual v -> u = v.
  Proof.
    intros.
    rewrite <- (dual_invol u), <- (dual_invol v). rewrite H. reflexivity.
  Qed.

  (** extension of linear negation to lists, note that it reverses lists *)
  Fixpoint ldual l := 
    match l with 
      | [] => []
      | a::l => ldual l ++ [dual a]
    end.
   
  (** input and output formulae (Danos-Regnier polarities) *)
  Inductive input: T -> Prop :=
  | i_rav: forall i, input (rav i)
  | i_par: forall a b, input a -> input b -> input (a $ b)
  | i_bot: input ⊥
  | i_dot_l: forall a b, input a -> output b -> input (a ⨂ b)
  | i_dot_r: forall a b, output a -> input b -> input (a ⨂ b)
  with output: T -> Prop := 
  | o_var: forall i, output (var i)
  | o_dot: forall a b, output a -> output b -> output (a ⨂ b)
  | o_one: output 1
  | o_par_l: forall a b, output a -> input b -> output (a $ b)
  | o_par_r: forall a b, input a -> output b -> output (a $ b)
  .
  Hint Constructors input output.

  (** input lists *)
  Inductive linput: list T -> Prop :=
  | i_nil: linput nil
  | i_cons: forall i l, input i -> linput l -> linput (i::l).
  Hint Constructors linput.

  (** linear negation goes from input to output formulae, and vice-versa *)
  Lemma dual_input: forall u, input u -> output (dual u)
  with dual_output: forall u, output u -> input (dual u).
  Proof.
    induction 1; intros; simpl; auto.  
    induction 1; intros; simpl; auto.
  Qed.

  (** lemmas about input lists *)
  Lemma i_app_inv: forall h k, linput (h++k) -> linput h /\ linput k.
  Proof.
    induction h; intros. auto.  inversion' H. apply IHh in H3. intuition; auto. 
  Qed.

  (* inversion of input/output hypotheses *)
  Ltac inverse_io :=
    repeat match goal with 
             | H: linput (_++_) |- _ => apply i_app_inv in H as [? ?]
             | H: linput ?u |- _ => is_constr u; inversion' H
             | H: input ?u |- _ => is_constr u; inversion' H
             | H: output ?u |- _ => is_constr u; inversion' H
           end.
  
  Lemma i_app: forall h k, linput h -> linput k -> linput (h++k).
  Proof.
    induction h; intros; inverse_io; simpl; auto.
  Qed.
  Hint Resolve i_app.

  (** a formula cannot be both input and output (not used in the sequel) *)
  Lemma not_i_and_o: forall u, input u -> output u -> False.
  Proof. induction u; intros; inverse_io; auto. Qed.

  (* inversion of list equalities, to do case analysis with cyclic permutation hypotheses *)
  Ltac inverse_app := 
    repeat match goal with 
             | H: [] = _++_ |- _ => apply nil_app in H; destruct H; subst
             | H: [_] = _++_ |- _ => apply consnil_app in H; destruct H as [[? ?]|[? ?]]; subst
             | H: _::_ = _++_ |- _ => apply cons_app in H; destruct H as [[? ?]|[? [? ?]]]; subst
             | H: [_] = [_] |- _ => dependent destruction H
             | H: _ :: _ = _ :: _ |- _ => dependent destruction H
           end.

  Section types.
  
    (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target)  *)
    Variable I: Set.
    Variables s t: X -> I.
  
    (** MLL typing judgement, for formulae, and lists *)
    Inductive typed: I -> I -> T -> Prop :=
    | t_var: forall x, typed (s x) (t x) (var x)
    | t_rav: forall x, typed (t x) (s x) (rav x)
    | t_one: forall n, typed n n 1
    | t_bot: forall n, typed n n ⊥
    | t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u ⨂ v)
    | t_par: forall n m o u v, typed n m u -> typed m o v -> typed n o (u $ v).

    Inductive ltyped: I -> I -> list T -> Prop :=
    | t_nil: forall n, ltyped n n []
    | t_cons: forall n m p l u, typed n m u -> ltyped m p l -> ltyped n p (u::l).

    Hint Constructors typed ltyped.
  
    Lemma t_app: forall l l' n m p, ltyped n m l -> ltyped m p l' -> ltyped n p (l++l').
    Proof. 
      intros.  induction H; simpl; eauto.
    Qed.
    Hint Resolve t_app.

    Lemma t_app_inv: forall l l' n p, ltyped n p (l++l') -> exists2 m, ltyped n m l & ltyped m p l'.
    Proof.
      induction l; intros.
       eauto.
       inversion' H. destruct (IHl _ _ _ H5). eauto.
    Qed.
    
    (** linear negation mirrors types  *)
    Lemma t_dual: forall u n m, typed n m u -> typed m n (dual u).
    Proof.
      induction 1; simpl; eauto.
    Qed.
    Hint Resolve t_dual.

    Lemma t_ldual: forall l n m, ltyped n m l -> ltyped m n (ldual l).
    Proof.
      induction 1; simpl; eauto.
    Qed.
    Hint Resolve t_ldual.

    (* inversion of typing derivations *)
    Ltac inverse_types := 
      repeat match goal with
               | H: typed _ _ ?x |- _ => is_constr x; inversion' H
               | H: ltyped _ _ ?x |- _ => is_constr x; inversion' H
               | H: ltyped _ _ (_++_) |- _ => destruct (t_app_inv H); clear H
             end.

    (** injectivity property of typing derivations *)
    Lemma typed_inj: forall u n m, typed n m u -> forall n' m', typed n' m' u -> n=n' /\ m=m' \/ n=m /\ n'=m'.
    Proof.
      induction 1; intros; inverse_types; intuition (subst; auto).
      eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto).
      eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto).
    Qed.

    Lemma ltyped_inj: forall l n m, ltyped n m l -> forall n' m', ltyped n' m' l -> n=n' /\ m=m' \/ n=m /\ n'=m'.
    Proof.
      induction 1; intros; inverse_types; intuition (subst; auto).
      destruct (typed_inj H H6); intuition (subst; auto).
      apply IHltyped in H0. apply IHltyped in H7. intuition (subst; auto).
    Qed.

    (* unification of pre-types by the injectivity property (with case analysis) *)
    Ltac injective_types :=
      repeat match goal with
               | H1: typed _ _ ?u,  H2: typed _ _ ?u |- _ => 
                 destruct (typed_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2
               | H1: ltyped _ _ ?u,  H2: ltyped _ _ ?u |- _ => 
                 destruct (ltyped_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2 
            end.

    (** typed sequent system for cyclic MLL  *)
    Inductive seq: I -> list T -> Prop :=
    | seq_ax: forall i, seq (t i) [rav i; var i]
    | seq_one:  forall n, seq n [1]
    | seq_bot: forall l n, seq n l -> seq n (⊥::l)
    | seq_dot: forall a b h l n, seq n (l++[a]) -> seq n (b::h) -> seq n (l++a ⨂ b::h)
    | seq_par: forall a b l n, seq n (a::b::l) -> seq n (a $ b::l)
    | seq_rot: forall a l n m, typed n m a -> seq m (l++[a]) -> seq n (a::l).

    Hint Constructors seq.

    (** sanity check: derivable sequents have square types *)
    Lemma seq_typed: forall l n, seq n l -> ltyped n n l.
    Proof.
      induction 1; intuition (inverse_types; injective_types; eauto).
    Qed.

    (* apply a rotation to the current goal *)
    Ltac rot := eapply seq_rot; eauto; simpl.

    (** admissible variant of rule [seq_rot]: rotate the sequent to an arbitrary position *)
    Lemma seq_rot': forall h l n m, ltyped m n h -> seq n (l++h) -> seq m (h++l).
    Proof.
      intros h l n m ltyp. revert l.
      induction ltyp; simpl; intros; inverse_types.
       rewrite <- app_nil_end in H. assumption.
       rot. rewrite app_ass. apply IHltyp. rewrite app_ass. assumption.
    Qed.

    (** admissible variant of rule [seq_dot] *)
    Lemma seq_dot': forall a b h l n m, typed n m a -> seq n (a::l) -> seq m (b::h) -> seq n (a ⨂ b::h++l).
    Proof.
      intros. eapply (seq_rot' (h:=a ⨂ b::h)). 
       apply seq_typed in H0. apply seq_typed in H1. inverse_types; injective_types; eauto.
       apply seq_dot; trivial. eapply seq_rot'; eauto. 
       apply seq_typed in H0. inverse_types; injective_types; eauto.
    Qed.

    (** the sequent system is "reflexive" *)
    Lemma seq_refl: forall u n m, typed n m u -> seq m [dual u; u].
    Proof.
      induction 1; simpl; eauto.
       rot. trivial. 
       rot. eauto.
       apply seq_par. rot. refine (seq_dot (l:=[dual u]) _ _); eauto.
       rot. apply seq_par. rot. refine (seq_dot (l:=[v]) _ _); simpl; eauto.
    Qed.

    (** input sequents cannot be proved *)
    Lemma linput_not_seq: forall l n, seq n l -> linput l -> False.
    Proof.
      induction 1; intros; inverse_io; auto.
    Qed.

    (** cut admissibility (not proved here, not used in the sequel)  *)
    Lemma seq_trans: forall n u l h, seq n (l++[u]) -> seq n (dual u::h) -> seq n (l++h).
    Proof.
    Abort.


  End types.

  (** [untyped] means typed in the trivial environment ;
      [useq] mean derivable in the untyped setting ;  
    *)
  Notation untyped u := (typed ttt ttt _ _ u).
  Notation useq := (seq ttt ttt tt).

  Hint Constructors seq typed ltyped.
  Hint Resolve t_app.

  (** terms and lists are always untyped  *)
  Lemma always_untyped: forall u, typed ttt ttt tt tt u.
  Proof. 
    induction u; eauto.
    generalize (t_var ttt ttt x); destruct (ttt x); auto. 
    generalize (t_rav ttt ttt x); destruct (ttt x); auto.
  Qed.

  Lemma always_luntyped: forall l, ltyped ttt ttt tt tt l.
  Proof. 
    induction l; eauto using always_untyped.
  Qed.


  (* inversion of typing derivations *)
  Ltac inverse_types := 
    repeat match goal with
             | H: typed _ _ _ _ ?x |- _ => is_constr x; inversion' H
             | H: ltyped _ _ _ _ ?x |- _ => is_constr x; inversion' H
             | H: ltyped _ _ _ _ (_++_) |- _ => destruct (t_app_inv H); clear H
           end.
  
  (* clearing useless hypotheses *)
  Ltac clean_untyped :=
    repeat match goal with 
             | t: unit |- _ => destruct t
             | H: untyped _ |- _ => clear H
           end.

  Section erase.

    Variable I: Set.
    Variables s t: X -> I.
  
    Notation ltyped := (ltyped s t).
    Notation typed := (typed s t).
    Notation seq := (seq s t).

    (** key lemma: types of derivable sequents are squares *)
    Lemma useq_mono: forall l, useq l -> forall n m, ltyped n m l -> n=m.
    Proof.
      (* generalisation: types of cyclic permutations of derivable sequents are squares *)
      assert (G: forall l, useq l -> forall h k n m, l=h++k -> ltyped n m (k++h) -> n=m).
        induction 1; intros; inverse_app; inverse_types; auto; clean_untyped.
         apply (IHseq nil l); trivial. rewrite <-app_nil_end. assumption.
         eauto.
         apply split_select in H1 as [h' ?]; intuition; subst; inverse_app; inverse_types.
          specialize (IHseq2 nil (b::h) m1 x refl). apply apply in IHseq2. 2: eauto. subst.
           apply (IHseq1 h0 (h'++[a])). apply app_ass. eauto. 
          specialize (IHseq2 nil (b::h) m1 x refl). apply apply in IHseq2. 2: eauto. subst. eauto.   
          specialize (IHseq1 nil (l++[a]) x m1 refl). apply apply in IHseq1. 2: eauto. subst.
           apply (IHseq2 (b::x0) k _ _ refl). eauto. 
         apply (IHseq nil _ _ _ refl). rewrite <-app_nil_end. eauto. 
         apply (IHseq (a::b::x) _ _ _ refl). eauto. 
         eauto.
         apply (IHseq x (k++[a]) _ _). apply app_ass. eauto.

      intros l H n m Hnm. apply (G _ H nil _ _ _ refl). rewrite <- app_nil_end. assumption.
    Qed.
    
    (** untyping theorem for cyclic MLL  *)
    Theorem untype: forall l, useq l -> forall n, ltyped n n l -> seq n l.
    Proof.
      induction 1; intros; clean_untyped; inverse_types; eauto 6.
      assert (n0 = m0). eapply useq_mono in H0. 2: eauto. auto.
      subst. eauto 7.
    Qed.

    (** typed derivable sequents are untyped derivable  *)
    Lemma erase: forall l n, seq n l -> useq l.
    Proof.
      induction 1; eauto using always_untyped.
      generalize (seq_ax ttt ttt i); destruct (ttt i); auto.
    Qed.

 End erase.

End MLL.






(** ** Untyping theorem for non commutative IMLL, i.e., residuated monoids #<a name=imll></a># *)
Module IMLL.

  Import MLL.
  Hint Resolve t_dual t_ldual dual_input dual_output.

  (** terms *)
  Inductive T: Set :=
  | dot: T -> T -> T
  | ldv: T -> T -> T
  | rdv: T -> T -> T
  | one: T
  | var: X -> T.

  (* is some term a ``constructed'' one, i.e., not a Coq variable; 
     this is useful to define some tactics below *)
  Ltac is_constr x := 
    match x with 
      | dot _ _ => idtac
      | ldv _ _ => idtac
      | rdv _ _ => idtac
      | var _ => idtac
      | one => idtac
      | [] => idtac
      | _::_ => idtac
    end.

  (** notations  *)
  Delimit Scope V_scope with V.
  Open Scope V_scope.
  Notation "x * y"   := (dot x y) (at level 40, left associativity): V_scope. 
  Notation "x / y"   := (rdv x y) (at level 40, left associativity): V_scope.
  Notation "x \ y"   := (ldv x y) (at level 40, left associativity): V_scope.
  Notation "1"       := (one): V_scope. 

  
  (** encoding of IMLL formulae into MLL formulae *)
  Fixpoint to_MLL (u: T): MLL.T :=
    match u with
      | a * b => to_MLL a ⨂ to_MLL b
      | a \ b => dual (to_MLL a) $ to_MLL b
      | a / b => to_MLL a $ dual (to_MLL b)
      | 1 => MLL.one
      | var x => MLL.var x
    end.

  (** extension to lists of formulae (warning: this function already applies the linear negation) *)
  Fixpoint lto_MLL l :=
    match l with 
     | [] => []
     | a::q => lto_MLL q++[dual (to_MLL a)]
    end.

  (** encoding of a concatenation *)
  Lemma lto_MLL_app: forall h k, lto_MLL (h++k) = lto_MLL k ++ lto_MLL h.
  Proof.
    induction h; intro; simpl.
     rewrite <- app_nil_end. reflexivity.
     rewrite IHh, app_ass. reflexivity.
  Qed.

  (** the encoding produces output formulae  *)
  Lemma to_MLL_output: forall u, MLL.output (to_MLL u).
  Proof.
    induction u; simpl; auto using MLL.dual_input, MLL.dual_output.
  Qed.

  (** the encoding of list produces lists of input formulae  *)
  Lemma lto_MLL_linput: forall l, MLL.linput (lto_MLL l).
  Proof.
    induction l; simpl; auto. apply MLL.i_app; trivial. constructor; trivial. apply MLL.dual_output, to_MLL_output.
  Qed.

  (* inversion on list equalities, to reason by case analysis about cyclic permutations *)
  Ltac inverse_app := 
    repeat  (
      simpl in *;
        match goal with 
          | H: [] = _::_ |- _ => discriminate H
          | H: _::_ = [] |- _ => discriminate H
          | H: _ (=) _ |- _ => inversion' H
          | H: [_] = [_] |- _ => inversion' H
          | H: _ :: _ = _ :: _ |- _ => inversion' H
          | H: _++_ = _++_ |- _ => apply app_app in H; destruct H as [? [[? ?]|[? ?]]]; subst
          | H: [] = _++_ |- _ => apply nil_app in H; destruct H; subst
          | H: _ ++ _ = [] |- _ => symmetry in H; apply nil_app in H; destruct H; subst
          | H: [_] = _++_ |- _ => apply consnil_app in H; destruct H as [[? ?]|[? ?]]; subst
          | H: _++_ = [_] |- _ => symmetry in H; apply consnil_app in H; destruct H as [[? ?]|[? ?]]; subst
          | H: _::_ = _++_ |- _ => apply cons_app in H; destruct H as [[? ?]|[? [? ?]]]; subst
          | H: _++_ = _::_ |- _ => symmetry in H; apply cons_app in H; destruct H as [[? ?]|[? [? ?]]]; subst
          | H: context[ _++[] ] |- _ => rewrite <- app_nil_end in H
        end).    

  (** inversion lemmas, to reason about cyclic permutations *)
  Lemma lto_MLL_app_inv: forall q l h, 
    l++h = lto_MLL q -> exists l', exists h', q=h'++l' /\ lto_MLL l' = l /\ lto_MLL h' = h.
  Proof.
    induction q; simpl; intros.
     inverse_app. exists (@nil T). exists (@nil T). auto.
     inverse_app. 
     exists (a::q). exists (@nil T). auto. 
     exists q. exists [a]. intuition; auto.
     symmetry in H. apply IHq in H as (?&?&?&?&?). exists x0. exists (a::x1). simpl. rewrite H, H0, H1. auto. 
  Qed.

  Lemma lto_MLL_cons_inv: forall q u h,
    u::h = lto_MLL q -> exists u', exists h', q=h'++[u'] /\ to_MLL u' = MLL.dual u /\ lto_MLL h' = h.
  Proof.
    induction q; simpl; intros.
     inverse_app. 
     inverse_app.
      destruct q; inverse_app. exists (a). exists (@nil T). simpl. rewrite MLL.dual_invol. auto. 
      symmetry in H. apply IHq in H as (?&?&?&?&?). subst. exists x0. exists (a::x1). simpl. auto. 
  Qed.

  (** inversion of the encoding *)
  Ltac inverse_conv :=
    repeat
      match goal with 
        | H: dual _ = dual _ |- _ => apply dual_inj in H
        | H: dual _ = _ |- _ => rewrite <- dual_invol in H; apply dual_inj in H
        | H: to_MLL _ = _ |- _ => symmetry in H
        | H: lto_MLL _ = _ |- _ => symmetry in H
        | H: ?x = to_MLL ?w |- _ => MLL.is_constr x; destruct w; try discriminate H; simpl in H; inversion' H
        | H: ?x = dual (to_MLL ?w) |- _ => MLL.is_constr x; destruct w; try discriminate H; simpl in H; inversion' H
        | H: [] = lto_MLL ?w |- _ => destruct w; [clear H| inverse_app]
        | H: _::_ = lto_MLL ?w |- _ => apply lto_MLL_cons_inv in H as (?&?&->&?&?); simpl in *
        | H: _++_ = lto_MLL ?w |- _ => apply lto_MLL_app_inv in H as (?&?&->&?&?)
      end.
  
  (* systematic case analysis *)
  Ltac inverse := repeat progress (inverse_app; inverse_conv).

  Section types.
  
    (** [I] is the set of pretypes, [s] and [t] give the typing environment (source and target)  *)
    Variable I: Set.
    Variables s t: X -> I.

    (** IMLL typing judgements, for formulae and lists *)
    Inductive typed: I -> I -> T -> Prop :=
    | t_var: forall x, typed (s x) (t x) (var x)
    | t_one: forall n, typed n n 1
    | t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u * v)
    | t_ldv: forall n m o u v, typed m n u -> typed m o v -> typed n o (u \ v)
    | t_rdv: forall n m o u v, typed o m u -> typed n m v -> typed n o (v / u).

    Inductive ltyped: I -> I -> list T -> Prop :=
    | t_nil: forall n, ltyped n n []
    | t_cons: forall n m p l u, typed n m u -> ltyped m p l -> ltyped n p (u::l).

    Hint Constructors typed ltyped.
  
    Lemma t_app: forall l l' n m p, ltyped n m l -> ltyped m p l' -> ltyped n p (l++l').
    Proof. 
      intros. induction H; simpl; eauto.
    Qed.
    Hint Resolve t_app.

    Lemma t_app_inv: forall l l' n p, ltyped n p (l++l') -> exists2 m, ltyped n m l & ltyped m p l'.
    Proof.
      induction l; intros.
       eauto.
       inversion' H. destruct (IHl _ _ _ H5). eauto.
    Qed.

    (* inversion on typing derivations *)
    Ltac inverse_types := 
      repeat match goal with
               | H: typed _ _ ?x |- _ => is_constr x; inversion' H
               | H: ltyped _ _ ?x |- _ => is_constr x; inversion' H
               | H: ltyped _ _ (_++_) |- _ => destruct (t_app_inv H); clear H
             end.

    (** injectivity property of types *)
    Lemma typed_inj: forall u n m, typed n m u -> forall n' m', typed n' m' u -> n=n' /\ m=m' \/ n=m /\ n'=m'.
    Proof.
      induction 1; intros; inverse_types; intuition (subst; auto).
      eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto).
      eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto).
      eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto).
    Qed.

    Lemma ltyped_inj: forall l n m, ltyped n m l -> forall n' m', ltyped n' m' l -> n=n' /\ m=m' \/ n=m /\ n'=m'.
    Proof.
      induction 1; intros; inverse_types; intuition (subst; auto).
      destruct (typed_inj H H6); intuition (subst; auto).
      apply IHltyped in H0. apply IHltyped in H7. intuition (subst; auto).
    Qed.

    (* unification of pre-types by the injectivity property (with case analysis) *)
    Ltac injective_types :=
      repeat match goal with
               | H1: typed _ _ ?u,  H2: typed _ _ ?u |- _ => 
                 destruct (typed_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2
               | H1: ltyped _ _ ?u,  H2: ltyped _ _ ?u |- _ => 
                 destruct (ltyped_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2 
            end.

    (** the encoding preserve types *)
    Lemma typed_to_MLL: forall u n m, typed n m u -> MLL.typed s t n m (to_MLL u).
    Proof. induction 1; simpl; eauto. Qed.

    Lemma ltyped_to_MLL: forall l n m, ltyped n m l -> MLL.ltyped s t m n (lto_MLL l).
    Proof. induction 1; simpl; eauto using typed_to_MLL. Qed.

    Lemma to_MLL_typed: forall u n m, MLL.typed s t n m (to_MLL u) -> typed n m u.
    Proof. 
      induction u; simpl; intros; MLL.inverse_types; eauto.
      apply t_dual in H4. rewrite dual_invol in H4. eauto.
      apply t_dual in H5. rewrite dual_invol in H5. eauto.
    Qed.

    Lemma to_MLL_ltyped: forall l n m, MLL.ltyped s t n m (lto_MLL l) -> ltyped m n l.
    Proof. 
      induction l; simpl; intros; MLL.inverse_types; eauto.
      apply t_dual in H5. rewrite dual_invol in H5. eauto using to_MLL_typed.
    Qed.

    (** sequent proof system for residuated monoids *)
    Inductive leq: I -> I -> list T -> T -> Prop :=
    | leq_var: forall i, leq (s i) (t i) [var i] (var i)
    | one_intro: forall n, leq n n [] 1
    | one_elim: forall n m l l' u, leq n m (l++l') u -> leq n m (l++1::l') u
    | dot_intro: forall n m p l l' u u', leq n m l u -> leq m p l' u' -> leq n p (l++l') (u * u')
    | dot_elim: forall n m l v w l' u, leq n m (l++v::w::l') u -> leq n m (l++(v * w)::l') u
    | rdv_intro: forall n m p u v l, typed p m v -> leq n m (l++[v]) u -> leq n p l (u / v)
    | rdv_elim: forall n m p q l k v w l' u, ltyped m q l' -> 
      leq n m k v -> leq p q (l++w::l') u -> leq p q (l++(w / v)::k++l') u
    | ldv_intro: forall n m p u v l, typed n p v -> leq n m (v::l) u -> leq p m l (v \ u)
    | ldv_elim: forall n m p q l k v w l' u, ltyped p m l -> 
      leq m n k v -> leq p q (l++w::l') u -> leq p q (l++k++(v \ w)::l') u.

    (** sanity check: derivable sequents are correctly typed *)
    Lemma leq_typed: forall l u n m, leq n m l u -> ltyped n m l /\ typed n m u.
    Proof.
      induction 1; intuition (inverse_types; injective_types; eauto).
    Qed.

    Hint Rewrite lto_MLL_app : permut_norm.
    
    (** "one output, several input" cyclic MLL derivable sequents yield derivable IMLL sequents 
       (we start from an untyped sequent for commodity, so that we do not have to bother about 
       types when applying induction hypotheses)
      *)
    Theorem uMLL_to_IMLL: forall n m l u, ltyped n m l -> typed n m u -> 
      useq (to_MLL u::lto_MLL l) -> leq n m l u.
    Proof.
      cut (forall l0, useq l0 -> forall n m l u, 
        ltyped n m l -> typed n m u -> to_MLL u::lto_MLL l (=) l0 -> leq n m l u).
       intros H n m l u Hl Hu Hlu. eapply H; eauto. 
      induction 1; intros p q k u Hk Hu Heq.
    
       inverse. inverse_types. constructor.

       inverse; inverse_types; constructor.

       inverse; inverse_types.
        rewrite app_ass. constructor. apply IHseq; eauto. solve_perm.

       inverse; subst; inverse_types; clean_untyped.
        eapply useq_mono in H0. 2: eauto using typed_to_MLL, ltyped_to_MLL. subst.
        econstructor. apply IHseq1; eauto. solve_perm. apply IHseq2; trivial. 

        eapply useq_mono in H. 2: eauto using typed_to_MLL, ltyped_to_MLL. subst.
        eapply (dot_intro (l:=[]) (l':=k)); eauto. 

        eapply useq_mono in H0. 2: eauto using typed_to_MLL, ltyped_to_MLL. subst.
        rewrite app_ass. simpl. eapply (ldv_elim (l:=[])); eauto. 

        elim (linput_not_seq H0). auto using to_MLL_output, lto_MLL_linput. 

        elim (linput_not_seq H). auto using to_MLL_output, lto_MLL_linput.
 
        eapply useq_mono in H. 2: eauto using typed_to_MLL, ltyped_to_MLL. subst.
        rewrite 2app_ass. simpl. econstructor; eauto. apply IHseq1; eauto. solve_perm. 
         apply IHseq2; eauto. solve_perm. 

        eapply useq_mono in H. 2: eauto using typed_to_MLL, ltyped_to_MLL. subst.
        econstructor; eauto. apply IHseq1; eauto. solve_perm.

        eapply useq_mono in H0. 2: eauto using typed_to_MLL, ltyped_to_MLL. subst.
        rewrite app_ass. econstructor; eauto. apply IHseq1; eauto. solve_perm. 

        elim (linput_not_seq H0). auto using to_MLL_output, lto_MLL_linput. 

       inverse; inverse_types.
        econstructor; eauto. apply IHseq; eauto. solve_perm.
        econstructor; eauto. apply IHseq; eauto. solve_perm.
        econstructor; eauto. apply IHseq; eauto. solve_perm.
        econstructor; eauto. apply IHseq; eauto. solve_perm.
        rewrite app_ass. constructor. apply IHseq; eauto. solve_perm. 
   
       inverse; subst; inverse_types; apply IHseq; eauto; solve_perm. 
    Qed.

  End types.
  
  (** [untyped] means typed in the trivial environment ;
      [uleq] mean derivable in the untyped setting ;  
    *)
  Notation untyped u := (typed ttt ttt _ _ u).
  Notation uleq := (leq ttt ttt tt tt).

  Hint Constructors typed.
  Lemma always_untyped: forall u, typed ttt ttt tt tt u.
  Proof. 
    induction u; eauto.
    generalize (t_var ttt ttt x); destruct (ttt x); auto. 
  Qed.

  Hint Constructors ltyped.
  Lemma always_luntyped: forall l, ltyped ttt ttt tt tt l.
  Proof. 
    induction l; eauto using always_untyped.
  Qed.

  Hint Resolve MLL.always_untyped MLL.always_luntyped. 
  Hint Rewrite lto_MLL_app dual_invol : permut_norm.

  (* apply a rotation to the current sequent (and possibly solves the goal) *)
  Ltac rot := permut_norm; (eapply seq_rot' || eapply seq_rot); permut_norm; eauto.
  (* solve a sequent which appears rotated in the hypotheses (may loop) *)
  Ltac solve_rot := repeat rot. 

  (** non commutative IMLL derivable sequents yield cyclic MLL derivable sequents ;
     it suffices to prove it for the untyped setting *)
  Theorem uIMLL_to_uMLL: forall l u, uleq l u -> useq (to_MLL u::lto_MLL l).
  Proof.
    induction 1; clean_untyped; permut_norm.
     rot. generalize (MLL.seq_ax ttt ttt i); destruct (ttt i); auto.
     constructor.
     rot. rot. constructor. solve_rot. 
     eapply seq_dot'; eauto. 
     rot. rot. constructor. solve_rot.  
     constructor. assumption.
     rot. rot. econstructor; eauto. solve_rot. solve_rot.
     constructor. solve_rot.
     rot. rot. eapply seq_dot'; eauto. solve_rot. 
  Qed.

  Section erase.

    Variable I: Set.
    Variables s t: X -> I.
  
    Hint Constructors leq.

    Notation ltyped := (ltyped s t).
    Notation typed := (typed s t).
    Notation leq := (leq s t).

    (** untyping theorem for residuated monoids (non-commutative IMLL)  *)
    Theorem untype: forall l u, uleq l u -> forall n m, ltyped n m l -> typed n m u -> leq n m l u.
    Proof.
      intros l u Hlu n m Hl Hu.
      apply uMLL_to_IMLL; trivial.
      apply uIMLL_to_uMLL, Hlu.
    Qed.

    (** typed derivable sequents are untyped derivable (straightforward) *)
    Lemma erase: forall l u n m, leq n m l u -> uleq l u.
    Proof.
      induction 1; eauto using always_untyped, always_luntyped.
      generalize (leq_var ttt ttt i); destruct (ttt i); auto.
    Qed.

    (** typed conversions between IMLL and MLL  *)
    Theorem IMLL_to_MLL: forall l u n m, leq n m l u -> seq s t n (to_MLL u::lto_MLL l).
    Proof.
      intros. apply MLL.untype.
       apply uIMLL_to_uMLL. eapply erase. eassumption.
       apply leq_typed in H. intuition eauto using typed_to_MLL, ltyped_to_MLL.
    Qed.
    Theorem MLL_to_IMLL: forall l u n m, ltyped n m l -> typed n m u -> seq s t n (to_MLL u::lto_MLL l) -> leq n m l u.
    Proof. intros. eauto using uMLL_to_IMLL, MLL.erase. Qed.

  End erase.

End IMLL.