# Untyping theorems for:

The corresponding .v file (with proofs) is here; see module mll for cyclic MLL and residuated monoids (with unit), module mall for cyclic MALL (involutive residuated lattices) and residuated lattices (without additive constants), and module ring for non-commutative rings.

X is the set of variables, it could be kept abstract
Definition X := nat.

syntax of terms, shared by all proofs. unused constructions will be ignored using the typing rules
Inductive T: Set :=
| dot: T -> T -> T
| pls: T -> T -> T
| inf: T -> T -> T
| rdv: T -> T -> T
| ldv: T -> T -> T
| str: T -> T
| dag: T -> T
| one: T
| zer: T
| var: X -> T.

notations; note that * is the product operation, while # is the star operation
Notation "x + y" := (pls 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" := (inf x y) (at level 30, right associativity): U_scope.
Notation "x / y" := (rdv y x) (at level 40, left associativity) : U_scope.
Notation "y \ x" := (ldv y x) (at level 40, left associativity) : U_scope.
Notation "x #" := (str x) (at level 15, left associativity): U_scope.
Notation "x `" := (dag x) (at level 15, left associativity): U_scope.
Notation "1" := (one): U_scope.
Notation "0" := (zer): U_scope.

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

is some term equal to zero ?
Definition is_zer u := match u with 0 => true | _ => false end.
Lemma Is_zer u : is_zer u = true -> u=0.

cleaning function, that normalises terms w.r.t. annihilating laws
Fixpoint clean u :=
match u with
| u+v => let u := clean u in let v := clean v in if is_zer u then v else if is_zer v then u else u+v
| u*v => let u := clean u in let v := clean v in if is_zer u then 0 else if is_zer v then 0 else u*v
| u# => let u := clean u in if is_zer u then 1 else u#
| u` => let u := clean u in if is_zer u then 0 else u`
| _ => u
end.

a term is strict if its normal form is not zero
Notation strict u := (is_zer (clean u) = false).

the cleaning function is idempotent
Lemma clean_idem: forall u, clean (clean u) = clean u.

Lemma clean_strict: forall u, strict u -> strict (clean u).

Lemma strict_dot: forall u v, strict (u*v) <-> strict u /\ strict v.

Lemma strict_pls: forall u v, strict (u+v) <-> strict u \/ strict v.

## Untyping theorem for monoids

Module Monoid.

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.

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

typed equality judgement
Inductive equal: I -> I -> relation T :=
| vrefl: forall x, equal (s x) (t x) (var x) (var x)
| orefl: forall n, equal n n 1 1
| dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w)
| one_dot: forall u n m, typed n m u -> equal n m (1*u) u
| dot_one: forall u n m, typed n m u -> equal n m (u*1) u
| dot_compat: forall n m p, Proper (equal n m ==> equal m p ==> equal n p) dot
| trans: forall n m, Transitive (equal n m)
| sym: forall n m, Symmetric (equal n m).

End types.

untyped means typed in the trivial environment; == is the untyped equality
Notation untyped u := (typed ttt ttt u _ _).
Notation "u == v" := (equal ttt ttt tt tt u v) (at level 70, no associativity).

Section erase.

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

Notation typed := (typed s t).
Notation equal := (equal s t).

injectivity property of type derivations
Lemma typeinj: forall u n m, typed n m u -> forall m', typed n m' u -> m=m'.

equal terms have the same types
Lemma eqtype: forall u v, u == v -> forall n m, typed n m u <-> typed n m v.

untyping theorem for monoids
Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v.

End erase.

End Monoid.

## Untyping theorem for semirings

Module SemiRing.

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.

typing judgement
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_zer: forall n m, typed n m 0
| t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v)
| t_pls: forall n m u v, typed n m u -> typed n m v -> typed n m (u+v).

injectivity property for types of strict terms
Lemma typed_inj: forall u, strict u -> forall n m n' m',
typed n m u -> typed n' m' u -> (n=n' <-> m=m').

typed equality judgement
Inductive equal: I -> I -> relation T :=
| vrefl: forall x, equal (s x) (t x) (var x) (var x)
| orefl: forall n, equal n n 1 1
| zrefl: forall n m, equal n m 0 0
| dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w)
| one_dot: forall u n m, typed n m u -> equal n m (1*u) u
| dot_one: forall u n m, typed n m u -> equal n m (u*1) u
| zer_dot: forall u n m o, typed n m u -> equal o m (0*u) 0
| dot_zer: forall u n m o, typed n m u -> equal n o (u*0) 0
| pls_dot: forall u v w n m o, typed n m u -> typed o n v -> typed o n w -> equal o m ((v+w)*u) (v*u+w*u)
| dot_pls: forall u v w n m o, typed n m u -> typed m o v -> typed m o w -> equal n o (u*(v+w)) (u*v+u*w)
| pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u+(v+w)) ((u+v)+w)
| zer_pls: forall u n m, typed n m u -> equal n m (0+u) u
| pls_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u+v) (v+u)
| dot_compat: forall n m p u u' v v', equal n m u u' -> equal m p v v' -> equal n p (u*v) (u'*v')
| pls_compat: forall n m u u' v v', equal n m u u' -> equal n m v v' -> equal n m (u+v) (u'+v')
| trans: forall n m, Transitive (equal n m)
| sym: forall n m, Symmetric (equal n m).

strict typed equality judgement
Inductive sequal: I -> I -> relation T :=
| s_vrefl: forall x, sequal (s x) (t x) (var x) (var x)
| s_orefl: forall n, sequal n n 1 1
| s_zrefl: forall n m, sequal n m 0 0
| s_dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> sequal n p (u*(v*w)) ((u*v)*w)
| s_one_dot: forall u n m, typed n m u -> sequal n m (1*u) u
| s_dot_one: forall u n m, typed n m u -> sequal n m (u*1) u
| s_pls_dot: forall u v w n m o, strict u -> typed n m u -> typed o n v -> typed o n w -> sequal o m ((v+w)*u) (v*u+w*u)
| s_dot_pls: forall u v w n m o, strict u -> typed n m u -> typed m o v -> typed m o w -> sequal n o (u*(v+w)) (u*v+u*w)
| s_pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> sequal n m (u+(v+w)) ((u+v)+w)
| s_pls_comm: forall u v n m, typed n m u -> typed n m v -> sequal n m (u+v) (v+u)
| s_dot_compat: forall n m p u u' v v', sequal n m u u' -> sequal m p v v' -> sequal n p (u*v) (u'*v')
| s_pls_compat: forall n m u u' v v', sequal n m u u' -> sequal n m v v' -> sequal n m (u+v) (u'+v')
| s_trans: forall n m, Transitive (sequal n m)
| s_sym: forall n m, Symmetric (sequal n m).

strict equality is reflexive at each type, it is contained in equality
Lemma sequal_refl: forall n m u, typed n m u -> sequal n m u u.

Lemma sequal_equal: forall n m u v, sequal n m u v -> equal n m u v.

sanity requirement: equality relates well typed terms only
Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v.

the cleaning function preserves types
Lemma clean_typed: forall n m u, typed n m u -> typed n m (clean u).

Definition trans' n m u := @trans n m u.

the cleaning function returns a equivalent term
Lemma clean_correct: forall n m u, typed n m u -> equal n m u (clean u).

End types.

untyped means typed in the trivial environment ; == is the untyped equality ; =s= is the strict untyped equality
Notation untyped u := (typed ttt ttt tt tt u).
Notation "x == y" := (equal ttt ttt tt tt x y) (at level 70, no associativity).
Notation "x =s= y" := (sequal ttt ttt tt tt x y) (at level 70, no associativity).

Section erase.

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

Notation typed := (typed s t).
Notation equal := (equal s t).
Notation sequal := (sequal s t).

strictly equal terms have the same types
Lemma sequal_same_types: forall u v, u =s= v -> (forall n m, typed n m u <-> typed n m v).

untyping theorem for strict equalities
Lemma suntype: forall u v, u =s= v -> forall n m, typed n m u -> typed n m v -> sequal n m u v.

equal terms reduce to zero at the same time
Lemma clean_zer: forall u v, u == v -> is_zer (clean u) = is_zer (clean v).

factorisation lemma: equality proofs yield strict equality proofs between the normalised terms
Lemma factorise: forall u v, u == v -> clean u =s= clean v.

untyping theorem for semirings
Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v.

End erase.

End SemiRing.

## Untyping theorem for Kleene algebras

Module KleeneAlgebra.

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.

typing judgement
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_zer: forall n m, typed n m 0
| t_str: forall n u, typed n n u -> typed n n (u#)
| t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v)
| t_pls: forall n m u v, typed n m u -> typed n m v -> typed n m (u+v).

injectivity property for types of strict terms
Lemma typed_inj: forall u, strict u -> forall n m n' m',
typed n m u -> typed n' m' u -> (n=n' <-> m=m').

typed equality judgement
Inductive equal: I -> I -> relation T :=
| vrefl: forall x, equal (s x) (t x) (var x) (var x)
| orefl: forall n, equal n n 1 1
| zrefl: forall n m, equal n m 0 0
| dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w)
| one_dot: forall u n m, typed n m u -> equal n m (1*u) u
| dot_one: forall u n m, typed n m u -> equal n m (u*1) u
| zer_dot: forall u n m o, typed n m u -> equal o m (0*u) 0
| dot_zer: forall u n m o, typed n m u -> equal n o (u*0) 0
| pls_dot: forall u v w n m o, typed n m u -> typed o n v -> typed o n w -> equal o m ((v+w)*u) (v*u+w*u)
| dot_pls: forall u v w n m o, typed n m u -> typed m o v -> typed m o w -> equal n o (u*(v+w)) (u*v+u*w)
| pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u+(v+w)) ((u+v)+w)
| zer_pls: forall u n m, typed n m u -> equal n m (0+u) u
| pls_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u+v) (v+u)
| pls_idem: forall u n m, typed n m u -> equal n m (u+u) u
| str_fold_left: forall u n, typed n n u -> equal n n (1 + u#*u) (u#)
| str_ind_left: forall u v n m, typed n n u -> typed n m v -> equal n m (u*v+v) v -> equal n m (u#*v+v) v
| str_ind_right: forall u v n m, typed n n u -> typed m n v -> equal m n (v*u+v) v -> equal m n (v*u#+v) v
| dot_compat: forall n m p u u' v v', equal n m u u' -> equal m p v v' -> equal n p (u*v) (u'*v')
| pls_compat: forall n m u u' v v', equal n m u u' -> equal n m v v' -> equal n m (u+v) (u'+v')
| str_compat: forall n u u', equal n n u u' -> equal n n (u#) (u'#)
| trans: forall n m, Transitive (equal n m)
| sym: forall n m, Symmetric (equal n m).

strict typed equality judgement
Inductive sequal: I -> I -> relation T :=
| s_vrefl: forall x, sequal (s x) (t x) (var x) (var x)
| s_orefl: forall n, sequal n n 1 1
| s_zrefl: forall n m, sequal n m 0 0
| s_dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> sequal n p (u*(v*w)) ((u*v)*w)
| s_one_dot: forall u n m, typed n m u -> sequal n m (1*u) u
| s_dot_one: forall u n m, typed n m u -> sequal n m (u*1) u
| s_pls_dot: forall u v w n m o, strict u ->
typed n m u -> typed o n v -> typed o n w -> sequal o m ((v+w)*u) (v*u+w*u)
| s_dot_pls: forall u v w n m o, strict u ->
typed n m u -> typed m o v -> typed m o w -> sequal n o (u*(v+w)) (u*v+u*w)
| s_pls_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> sequal n m (u+(v+w)) ((u+v)+w)
| s_pls_comm: forall u v n m, typed n m u -> typed n m v -> sequal n m (u+v) (v+u)
| s_pls_idem: forall u n m, typed n m u -> sequal n m (u+u) u
| s_str_fold_left: forall u n, typed n n u -> sequal n n (1 + u#*u) (u#)
| s_str_ind_left: forall u v n m, strict v ->
typed n n u -> typed n m v -> sequal n m (u*v+v) v -> sequal n m (u#*v+v) v
| s_str_ind_right: forall u v n m, strict v ->
typed n n u -> typed m n v -> sequal m n (v*u+v) v -> sequal m n (v*u#+v) v
| s_dot_compat: forall n m p u u' v v', sequal n m u u' -> sequal m p v v' -> sequal n p (u*v) (u'*v')
| s_pls_compat: forall n m u u' v v', sequal n m u u' -> sequal n m v v' -> sequal n m (u+v) (u'+v')
| s_str_compat: forall n u u', sequal n n u u' -> sequal n n (u#) (u'#)
| s_trans: forall n m, Transitive (sequal n m)
| s_sym: forall n m, Symmetric (sequal n m).

strict equality is reflexive at each type, it is contained in equality
Lemma sequal_refl: forall n m u, typed n m u -> sequal n m u u.

Lemma sequal_equal: forall n m u v, sequal n m u v -> equal n m u v.

Lemma equal_refl: forall n m u, typed n m u -> equal n m u u.

Definition trans' n m u := @trans n m u.

Kleene star of zero is one
Lemma str_zer: forall n, equal n n (0#) 1.

sanity requirement: equality relates well typed terms only
Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v.

the cleaning function preserves types
Lemma clean_typed: forall n m u, typed n m u -> typed n m (clean u).

the cleaning function returns an equivalent term
Lemma clean_correct: forall n m u, typed n m u -> equal n m u (clean u).

End types.

untyped means typed in the trivial environment ; == is the untyped equality ; =s= is the strict untyped equality
Notation untyped u := (typed ttt ttt tt tt u).
Notation "x == y" := (equal ttt ttt tt tt x y) (at level 70, no associativity).
Notation "x =s= y" := (sequal ttt ttt tt tt x y) (at level 70, no associativity).

Section erase.

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

Notation typed := (typed s t).
Notation equal := (equal s t).
Notation sequal := (sequal s t).

strictly equal terms have the same types
Lemma sequal_same_types: forall u v, u =s= v -> (forall n m, typed n m u <-> typed n m v).

untyping theorem for strict equalities
Lemma suntype: forall u v, u =s= v -> forall n m, typed n m u -> typed n m v -> sequal n m u v.

equal terms reduce to zero at the same time
Lemma clean_zer: forall u v, u == v -> is_zer (clean u) = is_zer (clean v).

factorisation lemma: equality proofs yield strict equality proofs between the normalised terms
Lemma factorise: forall u v, u == v -> clean u =s= clean v.

untyping theorem for Kleene algebras
Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v.

End erase.

End KleeneAlgebra.

## Untyping theorem for allegories

Module Allegory.

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.

typing judgement
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_dag: forall n m u, typed n m u -> typed m n (u`)
| t_dot: forall n m q u v, typed n m u -> typed m q v -> typed n q (u*v)
| t_inf: forall n m u v, typed n m u -> typed n m v -> typed n m (u^v).

injectivity property of typing derivations
Lemma typed_inj: forall u n m n' m',
typed n m u -> typed n' m' u -> (n=n' <-> m=m').

typed equality judgement
Inductive equal: I -> I -> relation T :=
| vrefl: forall x, equal (s x) (t x) (var x) (var x)
| orefl: forall n, equal n n 1 1
| dot_assoc: forall u v w n m q p, typed n m u -> typed m q v -> typed q p w -> equal n p (u*(v*w)) ((u*v)*w)
| one_dot: forall u n m, typed n m u -> equal n m (1*u) u
| dot_one: forall u n m, typed n m u -> equal n m (u*1) u
| inf_assoc: forall u v w n m, typed n m u -> typed n m v -> typed n m w -> equal n m (u^(v^w)) ((u^v)^w)
| inf_comm: forall u v n m, typed n m u -> typed n m v -> equal n m (u^v) (v^u)
| dag_invol: forall u n m, typed n m u -> equal n m (u``) u
| dag_dot: forall u v n m p, typed n m u -> typed m p v -> equal p n ((u*v)`) (v`*u`)
| dag_inf: forall u v n m, typed n m u -> typed n m v -> equal m n ((u^v)`) (u`^v`)
| modular_law: forall u v w n m p, typed n m u -> typed m p v -> typed n p w ->
equal n p ((u*v) ^ w) ((u*(v^(u`*w))) ^ (u*v) ^ w)
| dag_compat: forall n m u u', equal n m u u' -> equal m n (u`) (u'`)
| dot_compat: forall n m p u u' v v', equal n m u u' -> equal m p v v' -> equal n p (u*v) (u'*v')
| inf_compat: forall n m u u' v v', equal n m u u' -> equal n m v v' -> equal n m (u^v) (u'^v')
| trans: forall n m, Transitive (equal n m)
| sym: forall n m, Symmetric (equal n m).

strict equality is reflexive at each type, and relates well-typed terms only
Lemma equal_refl: forall n m u, typed n m u -> equal n m u u.

Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v.

End types.

untyped means typed in the trivial environment, == is the untyped equality
Notation untyped u := (typed ttt ttt tt tt u).
Notation "x == y" := (equal ttt ttt tt tt x y) (at level 70, no associativity).

Section erase.

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

Notation typed := (typed s t).
Notation equal := (equal s t).

equal terms have the same types
Lemma equal_same_types: forall u v, u == v -> (forall n m, typed n m u <-> typed n m v).

untyping theorem for allegories
Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v.

End erase.

End Allegory.

## Untyping theorem for the Horn theory of monoids

Module HornMonoid.

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.

untyped proof assumptions (Horn hypotheses)
Variable h: I -> I -> relation T.

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

typed equality judgement
Inductive equal: I -> I -> relation T :=
| vrefl: forall x, equal (s x) (t x) (var x) (var x)
| orefl: forall n, equal n n 1 1
| dot_assoc: forall u v w n m o p, typed n m u -> typed m o v -> typed o p w -> equal n p (u*(v*w)) ((u*v)*w)
| one_dot: forall u n m, typed n m u -> equal n m (1*u) u
| dot_one: forall u n m, typed n m u -> equal n m (u*1) u
| dot_compat: forall n m p, Proper (equal n m ==> equal m p ==> equal n p) dot
| hyp: forall u v n m, h n m u v -> equal n m u v
| trans: forall n m, Transitive (equal n m)
| sym: forall n m, Symmetric (equal n m).

End types.

untyped means typed in the trivial environment; == is the untyped equality
Notation untyped u := (typed ttt ttt u _ _).

Section erase.

Variable I: Set.
Variables s t: X -> I.
Variable h: I -> I -> relation T.

Definition tth (_ _: unit) := fun u v => exists n m , h n m u v.
Notation "u == v" := (equal ttt ttt tth tt tt u v) (at level 70, no associativity).
Notation typed := (typed s t).
Notation equal := (equal s t h).

typing requirement about the Horn context
Hypothesis h_typed: forall n m u v, h n m u v -> typed n m u /\ typed n m v.
Hypothesis h_utyped: forall n m u v, h n m u v -> forall p q, typed p q u \/ typed p q v -> p=n /\ q=m.

Lemma h_utyped2: forall n m u v, h n m u v -> forall p q, typed p q u -> typed p q v -> p=n /\ q=m.

Lemma h_eqtyped: forall n m u v, h n m u v -> forall p q, typed p q u <-> typed p q v.

Lemma h_utyped': forall n m u v, h n m u v -> forall p q, typed p q u \/ typed p q v -> p=n /\ q=m.

injectivity property of type derivations
Lemma typeinj: forall u n m, typed n m u -> forall m', typed n m' u -> m=m'.

Lemma typeinj': forall u n m, typed n m u -> forall n' m', typed n' m' u ->
n=n' /\ m=m' \/ n=m /\ n'=m'.

equal terms have the same types
Lemma eqtype: forall u v, u == v -> forall n m, typed n m u <-> typed n m v.

untyping theorem for monoids
Theorem untype: forall u v, u == v -> forall n m, typed n m u -> typed n m v -> equal n m u v.

End erase.

End HornMonoid.

## Untyping theorem for residuated monoids without units : direct proof ,

see module mll for the proof with units, through cyclic MLL

Module UnitFreeResMonoid.

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.

typing judgement
Inductive typed: I -> I -> T -> Prop :=
| t_var: forall x, typed (s x) (t x) (var x)
| t_rdv: forall n m o u v, typed n o u -> typed m o v -> typed n m (u/v)
| t_ldv: forall n m o u v, typed n o u -> typed n m v -> typed m o (v\u)
| t_dot: forall n m o u v, typed n m u -> typed m o v -> typed n o (u*v).

typing judgement for lists of terms
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).

weak typing judgement for lists: each element has to be typeable
Inductive lwtyped: list T -> Prop :=
| wt_nil: lwtyped []
| wt_cons: forall n m l u, typed n m u -> lwtyped l -> lwtyped (u::l).

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

inversion lemma for typing judgements about concatenated lists
Lemma t_app_inv: forall l l' n p, ltyped n p (l++l') -> exists2 m, ltyped n m l & ltyped m p l'.

any typed list is weakly typed
Lemma lt_lwt: forall l n m, ltyped n m l -> lwtyped l.

weakly typing a concatenation
Lemma wt_app: forall l l', lwtyped l -> lwtyped l' -> lwtyped (l++l').

inversion lemma for weak typing judgements about concatenated lists
Lemma wt_app_inv: forall l l', lwtyped (l++l') -> lwtyped l /\ lwtyped l'.

(strong) injectivity property of typing judgements
Lemma typed_inj: forall u n m, typed n m u -> forall n' m', typed n' m' u -> n=n' /\ m=m'.

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

sanity checks: derivable sequents are correctly typed; the proof system is "reflexive"
Lemma leq_typed: forall l u n m, leq n m l u -> ltyped n m l /\ typed n m u.

Lemma leq_refl: forall u n m, typed n m u -> leq n m [u] u.

End types.

untyped means typed in the trivial environment ; <== is untyped derivability ;
Notation untyped u := (typed ttt ttt u _ _).
Notation "x <== y" := (leq ttt ttt tt tt x y) (at level 70, no associativity).

Section erase.

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

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

key lemma
Lemma untype_aux: forall l u, l <== u -> lwtyped l -> forall n m, typed n m u -> leq n m l u.

untyping theorem for residuated monoids without units
Theorem untype: forall l u, l <==u -> forall n m, ltyped n m l -> typed n m u -> leq n m l u.

End erase.

End UnitFreeResMonoid.