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

lemmas about input lists
  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).

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

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.
This page has been generated by coqdoc