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.

auxiliary lemmas about strict terms
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.
This page has been generated by coqdoc