(***********************************************************)
(*  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="##mo"># monoids#</a>#, 
   - #<a href="##sr"># semirings#</a>#, 
   - #<a href="##ka"># Kleene algebras#</a>#, 
   - #<a href="##al"># allegories#</a>#, 
   - #<a href="##hm"># Horn theory of monoids#</a>#. 
   - #<a href="##rm"># residuated monoids without unit (direct proof)#</a>#. 
   *)
(** The corresponding .v file (with proofs) is #<a href="utas.v">here</a>#;
   see module #<a href="mll.html">mll</a># for cyclic MLL and residuated monoids (with unit),
   module #<a href="mall.html">mall</a># for cyclic MALL (involutive residuated lattices) and residuated lattices (without additive constants),
   and module #<a href="ring.html">ring</a># for non-commutative rings. *)

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

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

(** [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.

(* 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
    | pls _ _ => idtac
    | inf _ _ => idtac
    | rdv _ _ => idtac
    | ldv _ _ => idtac
    | str _ => idtac
    | dag _ => idtac
    | var _ => idtac
    | one => idtac
    | zer => idtac
    | [] => idtac
    | _::_ => idtac
  end.

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

(** printing * #*# *)
(** notations; note that [*] is the product operation, while [#] is the star operation *)
Delimit Scope U_scope with U.
Open Scope U_scope.
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.
Proof. destruct u; firstorder discriminate. Qed.

(* tactic to automatically do case analyses on instances of the above tests appearing in the goal *)
Ltac destruct_tests tac :=
  repeat match goal with 
           | H: is_zer ?u = true |- _ => try rewrite (Is_zer H) in *; clear H
           | |- context[is_zer ?x] => 
             match x with context[is_zer _] => fail 1 | _ => idtac end;
             let H := fresh in
               case_eq (is_zer x); intro H; try rewrite H in *; try discriminate; tac
         end.

(** 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.
Proof.
  induction u; simpl; destruct_tests simpl; try congruence.
   rewrite <- IHu1 in H. discriminate.
   rewrite <- IHu2 in H0. discriminate.
   rewrite <- IHu1 in H. discriminate.
   rewrite <- IHu2 in H0. discriminate.
   rewrite <- IHu in H. discriminate.
   rewrite <- IHu in H. discriminate.
Qed.
   
(** auxiliary lemmas about strict terms *)
Lemma clean_strict: forall u, strict u -> strict (clean u).
Proof. intros. rewrite clean_idem. assumption. Qed.

Lemma strict_dot: forall u v, strict (u*v) <-> strict u /\ strict v.
Proof. intros. simpl. destruct_tests intuition. Qed.

Lemma strict_pls: forall u v, strict (u+v) <-> strict u \/ strict v.
Proof. intros. simpl. destruct_tests intuition. Qed.


(** ** Untyping theorem for monoids #<a name=mo></a># *)
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).
  Hint Constructors typed.

  Section erase.

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

    Notation typed := (typed s t).
    Notation equal := (equal s t).
  
    (* tactic to inverse typing derivations *)
    Ltac inverse_types := 
      repeat match goal with 
               | t: unit |- _ => destruct t
               | H: untyped _ |- _ => clear H
               | H: typed _ _ ?x |- _ => is_constr x; inversion' H
             end.

    (** injectivity property of type derivations *)
    Lemma typeinj: forall u n m, typed n m u -> forall m', typed n m' u -> m=m'.
    Proof.
      induction 1; intros; inverse_types; trivial. 
       firstorder (subst; auto).
    Qed.

    (* tactic to unify pre-types thanks to the above injectivity property *)
    Ltac injective_types :=
      repeat match goal with
               | H1: typed ?n _ ?u,  H2: typed ?n _ ?u |- _ => 
                 generalize (typeinj H1 H2); intro; subst; clear H2
             end.
  
    (** equal terms have the same types  *)
    Lemma eqtype: forall u v, u == v -> forall n m, typed n m u <-> typed n m v.
    Proof.
      induction 1; split; intro; trivial; inverse_types; eauto. 
       apply t_dot with m; firstorder.
       apply t_dot with m; firstorder.
       rewrite <- IHequal2, <- IHequal1; trivial.
       rewrite IHequal1, IHequal2; trivial.
       firstorder.
       firstorder.
     Qed.
    
    (** 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.
    Proof.
      induction 1; intros; inverse_types; injective_types; try solve [econstructor; eauto ].

       pose proof (proj1 (eqtype H _ _) H6).
       pose proof (proj1 (eqtype H0 _ _) H9).
       injective_types.
       apply dot_compat with m1; firstorder.
  
       pose proof (proj1 (eqtype H _ _) H1). 
       pose proof (proj1 (eqtype H0 _ _) H3).
       apply trans with y; eauto.
  
       apply sym. eauto.
    Qed.
  
  End erase.

End Monoid.





(** ** Untyping theorem for semirings #<a name=sr></a># *)
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).
  
    (* inversion of typing derivations *)
    Ltac inverse_types := 
      repeat match goal with 
               | H: typed _ _ ?x |- _ => is_constr x; inversion' H
             end.

    (** 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').
    Proof.
      intros u Hu n m n' m' H; revert n' m' Hu.
      induction H; intros; inverse_types; try tauto. 
       inversion Hu. 
       rewrite strict_dot in Hu. destruct Hu. apply IHtyped1 in H6; trivial. apply IHtyped2 in H7; tauto.
       rewrite strict_pls in Hu. firstorder. 
    Qed.    

    (** 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.
    Proof. induction 1; econstructor; eauto. Qed.

    Lemma sequal_equal: forall n m u v, sequal n m u v -> equal n m u v.
    Proof.
      induction 1; try solve [econstructor; eauto]. 
      apply sym; assumption.
    Qed.

    Hint Constructors typed.

    (** 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.
    Proof. induction 1; intuition eauto. Qed.

    (** the cleaning function preserves types *)
    Lemma clean_typed: forall n m u, typed n m u -> typed n m (clean u).
    Proof.
      induction 1; simpl; eauto.
      destruct_tests auto. eauto. 
      destruct_tests auto.
    Qed.

    Hint Constructors equal.
    Hint Resolve sequal_equal sequal_refl clean_typed.
    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).
    Proof.
      induction 1; simpl; auto.
       destruct_tests idtac; eauto using trans'.
       destruct_tests idtac; eauto using trans'. 
        apply trans with (clean u + 0); eauto. 
        eapply trans; [apply pls_comm|]; eauto. 
    Qed.

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

  Hint Constructors typed sequal equal.
  Hint Resolve sequal_equal sequal_refl clean_typed.

  (* inversion of typing derivations *)
  Ltac inverse_types := 
    repeat match goal with
             | H: typed _ _ _ _ ?x |- _ => is_constr x; inversion' H
             end.
  
  (* unification of pre-types by the injectivity property (with case analysis) *)
  Ltac injective_types :=
    repeat match goal with
             | H0: strict ?u, H1: typed _ _ ?n _ ?u,  H2: typed _ _ ?n _ ?u |- _ => 
               pose proof (proj1 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2
             | H0: strict ?u, H1: typed _ _ _ ?n ?u,  H2: typed _ _ _ ?n ?u |- _ =>
               pose proof (proj2 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2
           end.
    
  (* clearing useless hypotheses *)
  Ltac clean_untyped :=
    repeat match goal with 
             | t: unit |- _ => destruct t
           end.

  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).
    Proof.
      induction 1; split; intro; clean_untyped; trivial; inverse_types; injective_types; eauto;
        try solve [repeat econstructor; firstorder].
      apply t_dot with m; firstorder.
      apply t_dot with m; firstorder.
      rewrite <- IHsequal2, <- IHsequal1. trivial.
      rewrite IHsequal1, IHsequal2. trivial.
    Qed.
    
    (** 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.
    Proof.
      induction 1; intros; clean_untyped; inverse_types; injective_types; try solve [econstructor; eauto ].
  
       pose proof (sequal_same_types H).
       pose proof (sequal_same_types H0).
       apply s_dot_compat with m1; firstorder.
  
       pose proof (sequal_same_types H).
       pose proof (sequal_same_types H0).
       apply s_trans with y; firstorder. 
  
       apply s_sym. auto.
    Qed.
  

    (** 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).
    Proof.
      induction 1; auto; clean_untyped; simpl; destruct_tests auto.
      rewrite <- IHequal1 in IHequal2. discriminate.
      discriminate.
    Qed.

    (** factorisation lemma: equality proofs yield strict equality proofs between the normalised terms *)
    Lemma factorise: forall u v, u == v -> clean u =s= clean v.
    Proof.
      induction 1; clean_untyped; simpl; auto; try solve [destruct_tests auto; eauto 7 using clean_strict].

      rewrite (clean_zer H), (clean_zer H0).
       destruct_tests auto; eauto.  
      rewrite (clean_zer H), (clean_zer H0).
       destruct_tests auto; eauto.
      eapply s_trans; eassumption.
      apply s_sym; trivial.
    Qed. 
      
    (** 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.
    Proof.
      intros u v Huv n m Hu Hv.
      eapply trans. apply (clean_correct Hu).
      apply sym. eapply trans. apply (clean_correct Hv). apply sym.
      auto using suntype, factorise.  
    Qed.

  End erase.

End SemiRing.




(** ** Untyping theorem for Kleene algebras #<a name=ka></a># *)
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).
  
    (* inversion of typing derivations *)
    Ltac inverse_types := 
      repeat match goal with 
               | H: typed _ _ ?x |- _ => is_constr x; inversion' H
             end.

    (** 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').
    Proof.
      intros u Hu n m n' m' H; revert n' m' Hu.
      induction H; intros; inverse_types; try tauto. 
       inversion Hu. 
       rewrite strict_dot in Hu. destruct Hu. apply IHtyped1 in H6; trivial. apply IHtyped2 in H7; tauto.
       rewrite strict_pls in Hu. firstorder. 
    Qed. 


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

    Hint Constructors typed equal sequal.

    (** 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.
    Proof.
      induction 1; econstructor; eauto.
    Qed.

    Lemma sequal_equal: forall n m u v, sequal n m u v -> equal n m u v.
    Proof.
      induction 1; eauto.
      eapply trans; eauto.
      apply sym; assumption.
    Qed.

    Lemma equal_refl: forall n m u, typed n m u -> equal n m u u.
    Proof.
      intros. apply sequal_equal. apply sequal_refl. assumption.
    Qed.

    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.
    Proof.
      intro n.
      assert (H: equal n n (0#*1+1) 1). eauto 6 using trans'.
      eapply trans. 2: apply H.
      eapply trans. apply sym, str_fold_left; eauto.
      apply sym. eapply trans. apply H.
      eapply trans. 2: apply pls_compat. 3: apply sym; eauto. 2: apply equal_refl; eauto.
      eapply trans. apply sym, zer_pls; auto. auto.
    Qed.
    Hint Resolve str_zer.

    (** 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.
    Proof.
      induction 1; intuition eauto.
    Qed.

    (** the cleaning function preserves types *)
    Lemma clean_typed: forall n m u, typed n m u -> typed n m (clean u).
    Proof.
      induction 1; simpl; eauto; destruct_tests auto. eauto.
    Qed.
    Hint Resolve clean_typed.

    (** the cleaning function returns an equivalent term *)
    Lemma clean_correct: forall n m u, typed n m u -> equal n m u (clean u).
    Proof.
      induction 1; simpl; auto; destruct_tests idtac; eauto using trans'.
        apply trans with (clean u + 0); eauto. 
        eapply trans; [apply pls_comm|]; eauto. 
    Qed.

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

  Hint Constructors typed sequal equal.
  Hint Resolve sequal_refl clean_typed.

  (* inversion of typing derivations *)
  Ltac inverse_types := 
    repeat match goal with
             | H: typed _ _ _ _ ?x |- _ => is_constr x; inversion' H
             end.
  
  (* unification of pre-types by the injectivity property (with case analysis) *)
  Ltac injective_types :=
    repeat match goal with
             | H0: strict ?u, H1: typed _ _ ?n _ ?u,  H2: typed _ _ ?n _ ?u |- _ => 
               pose proof (proj1 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2
             | H0: strict ?u, H1: typed _ _ _ ?n ?u,  H2: typed _ _ _ ?n ?u |- _ =>
               pose proof (proj2 (typed_inj H0 H1 H2) (refl_equal _)); subst; clear H2
           end.
    
  (* clearing useless hypotheses *)
  Ltac clean_untyped :=
    repeat match goal with 
             | t: unit |- _ => destruct t
           end.

  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).
    Proof.
      induction 1; split; intro; clean_untyped; trivial; inverse_types; injective_types; eauto;
        try solve [repeat econstructor; firstorder].
      rewrite <- IHsequal in H3. inverse_types. injective_types; eauto.
      rewrite <- IHsequal in H3. inverse_types. injective_types; eauto.
      apply t_dot with m; firstorder.
      apply t_dot with m; firstorder.
      rewrite <- IHsequal2, <- IHsequal1. trivial.
      rewrite IHsequal1, IHsequal2. trivial.
    Qed.
    
    (** 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.
    Proof.
      induction 1; intros; clean_untyped; inverse_types; injective_types; eauto.
  
       pose proof (sequal_same_types H).
       pose proof (sequal_same_types H0).
       apply s_dot_compat with m; firstorder.
  
       pose proof (sequal_same_types H).
       pose proof (sequal_same_types H0).
       apply s_trans with y; firstorder. 
  
       apply s_sym. auto.
    Qed.
  
    (** 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).
    Proof.
      induction 1; auto; clean_untyped; simpl; destruct_tests auto.
      rewrite <- IHequal1 in IHequal2. discriminate.
      discriminate.
    Qed.

    (** factorisation lemma: equality proofs yield strict equality proofs between the normalised terms *)
    Lemma factorise: forall u v, u == v -> clean u =s= clean v.
    Proof.
      induction 1; clean_untyped; simpl; auto.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto 7 using clean_strict.
       destruct_tests auto; eauto 7 using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       destruct_tests auto; eauto using clean_strict.
       simpl in *. destruct_tests auto. simpl in *.
        eapply s_trans. apply s_pls_compat. apply s_one_dot; eauto. eauto. eauto. 
        apply s_str_ind_left; eauto using clean_strict.
       simpl in *. destruct_tests auto. simpl in *.
        eapply s_trans. apply s_pls_compat. apply s_dot_one; eauto. eauto. eauto. 
        apply s_str_ind_right; eauto using clean_strict.
       rewrite (clean_zer H), (clean_zer H0).
        destruct_tests auto; eauto.  
       rewrite (clean_zer H), (clean_zer H0).
        destruct_tests auto; eauto.
       rewrite (clean_zer H).
        destruct_tests auto; eauto.
       eapply s_trans; eassumption.
       apply s_sym; trivial.
    Qed. 
      
    (** 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.
    Proof.
      intros u v Huv n m Hu Hv.
      eapply trans. apply (clean_correct Hu).
      apply sym. eapply trans. apply (clean_correct Hv). apply sym.
      auto using suntype, factorise, sequal_equal.  
    Qed.

  End erase.

End KleeneAlgebra.




(** ** Untyping theorem for allegories #<a name=al></a># *)
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).

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

    (** 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').
    Proof.
      intros u n m n' m' H; revert n' m'.
      induction H; intros; inverse_types; try solve [firstorder].
      rewrite IHtyped1; eauto. 
    Qed.    

    (** 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.
    Proof. induction 1; econstructor; eauto. Qed.

    Hint Constructors typed.
    Lemma equal_typed: forall n m u v, equal n m u v -> typed n m u /\ typed n m v.
    Proof. 
      induction 1; intuition eauto 8. 
    Qed.

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

  Hint Constructors typed equal.
  Hint Resolve equal_refl.

  (* inversion of typing derivations *)
  Ltac inverse_types := 
    repeat match goal with
             | H: typed _ _ _ _ ?x |- _ => is_constr x; inversion' H
             end.
  
  (* unification of pre-types by the injectivity property (with case analysis) *)
  Ltac injective_types :=
    repeat match goal with
             | H1: typed _ _ ?n _ ?u,  H2: typed _ _ ?n _ ?u |- _ => 
               pose proof (proj1 (typed_inj H1 H2) (refl_equal _)); subst; clear H2
             | H1: typed _ _ _ ?n ?u,  H2: typed _ _ _ ?n ?u |- _ =>
               pose proof (proj2 (typed_inj H1 H2) (refl_equal _)); subst; clear H2
           end.
    
  (* clearing useless hypotheses *)
  Ltac clean_untyped :=
    repeat match goal with 
             | t: unit |- _ => destruct t
           end.

  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).
    Proof.
      induction 1; split; intro; clean_untyped; trivial; inverse_types; injective_types; eauto;
        try solve [repeat econstructor; firstorder].
      eauto 8.
      apply t_dot with m; firstorder.
      apply t_dot with m; firstorder.
      rewrite <- IHequal2, <- IHequal1. trivial.
      rewrite IHequal1, IHequal2. trivial.
    Qed.
    
    (** 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.
    Proof.
      induction 1; intros; clean_untyped; inverse_types; injective_types; try solve [econstructor; eauto ].
  
       pose proof (equal_same_types H).
       pose proof (equal_same_types H0).
       apply dot_compat with m1; firstorder.
  
       pose proof (equal_same_types H).
       pose proof (equal_same_types H0).
       apply trans with y; firstorder. 
  
       apply sym. auto.
    Qed.

  End erase.

End Allegory.




(** ** Untyping theorem for the Horn theory of monoids #<a name=hm></a># *)
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 _ _).
  Hint Constructors typed.

  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.
    Proof. intros. eauto. Qed.

    Lemma h_eqtyped: forall n m u v, h n m u v -> forall p q, typed p q u <-> typed p q v.
    Proof.
      intros. 
      destruct (h_typed H) as [Hu Hv]. 
      assert (H' := h_utyped H). specialize (H' p q). 
      firstorder subst; trivial.
    Qed.

    (* h_typed -> (h_typed <-> h_utyped2 /\ h_eqtyped) *)
    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.
    Proof.
      clear h_utyped.
      intros n m u v H p q [H'|H']; eapply h_utyped2; eauto; pose proof (h_eqtyped H p q); tauto.
    Qed.
      
    (* tactic to inverse typing derivations *)
    Ltac inverse_types := 
      repeat match goal with 
               | t: unit |- _ => destruct t
               | H: untyped _ |- _ => clear H
               | H: typed _ _ ?x |- _ => is_constr x; inversion' H
             end.

    (** injectivity property of type derivations *)
    Lemma typeinj: forall u n m, typed n m u -> forall m', typed n m' u -> m=m'.
    Proof.
      induction 1; intros; inverse_types; trivial. 
       firstorder (subst; auto).
    Qed.

    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'.
    Proof.
      induction 1; intros; inverse_types; auto.
       apply IHtyped1 in H6. apply IHtyped2 in H7. clear - H6 H7. intuition subst; auto.
    Qed.

    (* tactic to unify pre-types thanks to the above injectivity property *)
    Ltac injective_types :=
      repeat match goal with
               | H1: typed ?n _ ?u,  H2: typed ?n _ ?u |- _ => 
                 generalize (typeinj H1 H2); intro; subst; clear H2
             end.
  
    (** equal terms have the same types  *)
    Lemma eqtype: forall u v, u == v -> forall n m, typed n m u <-> typed n m v.
    Proof.
      induction 1; split; intro; trivial; inverse_types; eauto. 
       apply t_dot with m; firstorder.
       apply t_dot with m; firstorder. 
       destruct H as (?&?&H). eapply h_eqtyped in H. firstorder eauto.
       destruct H as (?&?&H). eapply h_eqtyped in H. firstorder eauto.
       rewrite <- IHequal2, <- IHequal1; trivial.
       rewrite IHequal1, IHequal2; trivial.
       firstorder.
       firstorder.
     Qed.
    
    (** 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.
    Proof.
      induction 1; intros; inverse_types; injective_types; try solve [econstructor; eauto ].

       pose proof (proj1 (eqtype H _ _) H6).
       pose proof (proj1 (eqtype H0 _ _) H9).
       injective_types.
       apply dot_compat with m1; firstorder.
 
       destruct H as (n&m&H). 
       destruct (h_utyped2 H H0 H1); subst. 
       apply hyp; assumption.

       pose proof (proj1 (eqtype H _ _) H1). 
       pose proof (proj1 (eqtype H0 _ _) H3).
       apply trans with y; eauto.
  
       apply sym. eauto.
    Qed.
  
  End erase.

End HornMonoid.





(** ** Untyping theorem for residuated monoids without units : direct proof #<a name=rm></a>#,
   see module #<a href="mll.html">mll</a># 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).

    Hint Constructors typed ltyped lwtyped.
  
    (** 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').
    Proof. 
      intros.  induction H; simpl; eauto.
    Qed.
    Hint Resolve t_app.

    (** 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'.
    Proof.
      induction l; intros.
       eauto.
       inversion_clear H. destruct (IHl _ _ _ H1). eauto.
    Qed.

    (** any typed list is weakly typed *)
    Lemma lt_lwt: forall l n m, ltyped n m l -> lwtyped l.
    Proof.
      induction 1; eauto.
    Qed.

    (** weakly typing a concatenation *)
    Lemma wt_app: forall l l', lwtyped l -> lwtyped l' -> lwtyped (l++l').
    Proof. 
      intros.  induction H; simpl; eauto.
    Qed.

    (** inversion lemma for weak typing judgements about concatenated lists *)
    Lemma wt_app_inv: forall l l', lwtyped (l++l') -> lwtyped l /\ lwtyped l'.
    Proof.
      induction l; intros l' H; simpl; auto.
      inversion_clear H. destruct (IHl _ H1). eauto. 
    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.

    (** (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'.
    Proof.
      induction 1; intros; inverse_types; firstorder.
    Qed.

    (* unification of pre-types thanks to the previous property *)
    Ltac injective_types :=
      repeat match goal with
               | H1: typed _ _ ?u,  H2: typed _ _ ?u |- _ => 
                 destruct (typed_inj H1 H2); repeat subst; clear H2
             end.

    (** 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
      .
    Hint Constructors leq.

    (** 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.
    Proof.
      induction 1; intuition (inverse_types; injective_types; eauto).
    Qed.  

    Lemma leq_refl: forall u n m, typed n m u -> leq n m [u] u.
    Proof.
      induction 1; eauto.
      econstructor. eassumption. eapply (rdv_elim (l:=[]) (k:=v::[]) (l':=[])); eauto. 
      econstructor. eassumption. refine (ldv_elim (l:=[]) (k:=v::[]) (l':=[]) _ _ _); eauto. 
      apply (dot_elim (l:=[])). eapply (dot_intro (l:=u::[]) (l':=v::[])); eauto.
    Qed.

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

  Hint Constructors leq typed ltyped lwtyped.
  Hint Resolve t_app wt_app lt_lwt.

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

    (* 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
               | H: lwtyped ?x |- _ => is_constr x; inversion' H
               | H: lwtyped (_++_) |- _ => destruct (wt_app_inv H); clear H
             end.
  
    (* unification of pre-types by the injectivity property *)
    Ltac injective_types :=
      repeat match goal with
               | H1: typed _ _ ?u,  H2: typed _ _ ?u |- _ => 
                 destruct (typed_inj H1 H2); repeat subst; clear H2
             end.
    
    (* clearing useless hypotheses *)
    Ltac clean_untyped :=
      repeat match goal with 
               | t: unit |- _ => destruct t
               | H: untyped _ |- _ => clear H
             end.

    (** key lemma *)
    Lemma untype_aux: forall l u, l <== u -> lwtyped l -> forall n m, typed n m u -> leq n m l u.
    Proof.
      induction 1; intros; clean_untyped; inverse_types; injective_types; eauto 6.
    Qed.

    (** 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.
    Proof.
      intros. eauto using untype_aux.
    Qed.
  
  End erase.

End UnitFreeResMonoid.