# This file contains Coq proofs of untyping theorems for:

The corresponding .v file (with proofs) is here; see module utas for monoids, semirings, Kleene algebras, and allegories; and module mll for cyclic MLL and residuated monoids (with unit).

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'.

Lemma nil_app: forall (h k: list A), [] = h++k -> []=h /\ []=k.

Lemma consnil_app: forall u (h k: list A), [u] = h++k -> [u]=h /\ []=k \/ []=h /\ [u]=k.

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.

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'.

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

Global Instance perm_equivalence: Equivalence perm.

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

Lemma permut_cons: forall u l k, l++[u] (=) k -> u::l (=) k.

Lemma permut_app: forall h l k, l++h (=) k -> h++l (=) k.

Lemma pmor1: forall P: list A -> Prop, (forall a l, P (l++[a]) -> P (a::l)) -> Proper (perm ==> iff) P.

End perm.

equality of lists, modulo cyclic permutations
Infix " (=) " := perm (at level 80).

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 MALL without additive constants (involutive residuated lattices)

Module MALL.

terms (formulae)
Inductive T: Set :=
| dot: T -> T -> T
| par: T -> T -> T
| wit: T -> T -> T
| opl: T -> T -> T
| one: T
| bot: T

| var: X -> T
| rav: X -> T.

notations
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 "x & y" := (wit x y) (at level 40, left associativity): U_scope.
Notation "x ⨁ y" := (opl x y) (at level 50, 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
| a & b => dual a dual b
| a b => dual a & dual b
| 1 =>
| => 1

| var i => rav i
| rav i => var i
end.

Lemma dual_invol: forall u, dual (dual u) = u.

Lemma dual_inj: forall u v, dual u = dual v -> u = v.

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)

| i_wit: forall a b, input a -> input b -> input (a & b)
| i_opl: forall a b, input 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)

| o_wit: forall a b, output a -> output b -> output (a & b)
| o_opl: forall a b, output a -> output b -> output (a b)
.

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

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).

Lemma i_app_inv: forall h k, linput (h++k) -> linput h /\ linput k.

Lemma i_app: forall h k, linput h -> linput k -> linput (h++k).

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.

MALL 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)

| t_wit: forall n m u v, typed n m u -> typed n m v -> typed n m (u & v)
| t_opl: forall n m u v, typed n m u -> typed n m v -> typed n m (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).

Lemma t_app: forall l l' n m p, ltyped n m l -> ltyped m p l' -> ltyped n p (l++l').

Lemma t_app_inv: forall l l' n p, ltyped n p (l++l') -> ex2 (fun m => ltyped n m l) (fun m => ltyped m p l').

linear negation mirrors types
Lemma t_dual: forall u n m, typed n m u -> typed m n (dual u).

Lemma t_ldual: forall l n m, ltyped n m l -> ltyped m n (ldual l).

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'.

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'.

typed sequent system for cyclic MALL
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_wit: forall a b l n ,
seq n (a::l) -> seq n (b::l) -> seq n (a & b::l)
| seq_opl_l: forall a b l n m, typed n m a -> typed n m b ->
seq n (a::l) -> seq n (a b::l)
| seq_opl_r: forall a b l n m, typed n m a -> typed n m b ->
seq n (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).

sanity check: derivable sequents have square types
Lemma seq_typed: forall l n, seq n l -> ltyped n n l.

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).

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).

the sequent system is "reflexive"
Lemma seq_refl: forall u n m, typed n m u -> seq m [dual u; u].

input sequents cannot be proved
Lemma linput_not_seq: forall l n, seq n l -> linput l -> False.

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).

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).

terms and lists are always untyped
Lemma always_untyped: forall u, typed ttt ttt tt tt u.

Lemma always_luntyped: forall l, ltyped ttt ttt tt tt l.

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.

untyping theorem for cyclic MALL
Theorem untype: forall l, useq l -> forall n, ltyped n n l -> seq n l.

typed derivable sequents are untyped derivable
Lemma erase: forall l n, seq n l -> useq l.

End erase.

End MALL.

## Untyping theorem for non commutative IMALL without additive constant,

i.e., residuated lattices without bounds
Module IMALL.

terms
Inductive T: Set :=
| dot: T -> T -> T
| ldv: T -> T -> T
| rdv: T -> T -> T
| inf: T -> T -> T
| sup: T -> T -> T
| one: T
| var: X -> T.

notations
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 "x /\ y" := (inf x y): V_scope.
Notation "x \/ y" := (sup x y): V_scope.
Notation "1" := (one): V_scope.

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

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

encoding of a concatenation
Lemma lto_MALL_app: forall h k, lto_MALL (h++k) = lto_MALL k ++ lto_MALL h.

the encoding produces output formulae
Lemma to_MALL_output: forall u, MALL.output (to_MALL u).

the encoding of list produces lists of input formulae
Lemma lto_MALL_linput: forall l, MALL.linput (lto_MALL l).

inversion lemmas, to reason about cyclic permutations
Lemma lto_MALL_app_inv: forall q l h,
l++h = lto_MALL q -> exists l', exists h', (q=h'++l' /\ lto_MALL l' = l /\ lto_MALL h' = h)%type.

inversion of the encoding
Lemma lto_MALL_cons_inv: forall q u h,
u::h = lto_MALL q -> exists u', exists h', (q=h'++[u'] /\ to_MALL u' = MALL.dual u /\ lto_MALL h' = h)%type.

Section types.

Variable I: Set.
Variables s t: X -> I.

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)
| t_inf: forall n m u v, typed n m u -> typed n m v -> typed n m (u /\ v)
| t_sup: forall n m u v, typed n m u -> typed n m v -> typed n m (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).

Lemma t_app: forall l l' n m p, ltyped n m l -> ltyped m p l' -> ltyped n p (l++l').

Lemma t_app_inv: forall l l' n p, ltyped n p (l++l') -> ex2 (fun m => ltyped n m l) (fun m => ltyped m p l').

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'.

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'.

the encoding preserve types
Lemma typed_to_MALL: forall u n m, typed n m u -> MALL.typed s t n m (to_MALL u).

Lemma ltyped_to_MALL: forall l n m, ltyped n m l -> MALL.ltyped s t m n (lto_MALL l).

Lemma to_MALL_typed: forall u n m, MALL.typed s t n m (to_MALL u) -> typed n m u.

Lemma to_MALL_ltyped: forall l n m, MALL.ltyped s t n m (lto_MALL l) -> ltyped m n l.

sequent proof system for residuated lattices without bounds
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
| inf_intro: forall n m l a b, leq n m l a -> leq n m l b -> leq n m l (a /\ b)
| inf_elim_l: forall n m p q l a b k v, typed p q a -> typed p q b -> ltyped n p l -> ltyped q m k ->
leq n m (l++a::k) v -> leq n m (l++(a /\ b)::k) v
| inf_elim_r: forall n m p q l a b k v, typed p q a -> typed p q b -> ltyped n p l -> ltyped q m k ->
leq n m (l++b::k) v -> leq n m (l++(a /\ b)::k) v
| sup_intro_l: forall n m l a b, typed n m a -> leq n m l b -> leq n m l (a \/ b)
| sup_intro_r: forall n m l a b, typed n m b -> leq n m l a -> leq n m l (a \/ b)
| sup_elim: forall n m p q l a b k v, typed p q a -> typed p q b -> ltyped n p l -> ltyped q m k ->
leq n m (l++a::k) v -> leq n m (l++b::k) v -> leq n m (l++(a \/ b)::k) v
.

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.

"one output, several input" cyclic MALL derivable sequents yield derivable IMALL sequents (we start from an untyped sequent for commodity, so that we do not have to bother about types when applying induction hypotheses)
Theorem uMALL_to_IMALL: forall n m l u, ltyped n m l -> typed n m u ->
useq (to_MALL u::lto_MALL l) -> leq n m l u.

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).

Lemma always_untyped: forall u, typed ttt ttt tt tt u.

Lemma always_luntyped: forall l, ltyped ttt ttt tt tt l.

non commutative IMALL derivable sequents yield cyclic MALL derivable sequents ; it suffices to prove it for the untyped setting
Theorem uIMALL_to_uMALL: forall l u, uleq l u -> useq (to_MALL u::lto_MALL l).

Section erase.

Variable I: Set.
Variables s t: X -> I.

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

untyping theorem for residuated lattices without bounds (non-commutative IMALL without additive connectives)
Theorem untype: forall l u, uleq l u -> forall n m, ltyped n m l -> typed n m u -> leq n m l u.

typed derivable sequents are untyped derivable (straightforward)
Lemma erase: forall l u n m, leq n m l u -> uleq l u.

typed conversiona between IMALL and MALL
Theorem IMALL_to_MALL: forall l u n m, leq n m l u -> seq s t n (to_MALL u::lto_MALL l).
Theorem MALL_to_IMALL: forall l u n m, ltyped n m l -> typed n m u -> seq s t n (to_MALL u::lto_MALL l) -> leq n m l u.

End erase.

End IMALL.