(***********************************************************) (* This file is distributed under the terms of the *) (* GNU Lesser General Public License version 3 *) (* *) (* Copyright 2009-2010: Damien Pous. *) (* *) (***********************************************************) (** * This file contains Coq proofs of untyping theorems for: - ## cyclic MALL without additive constants (involutive residuated lattices)##, - ## non commutative IMALL without additive constants ##. *) (** 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). *) Require Import Relations List. Require Import Program. Require Import Setoid Morphisms. Set Implicit Arguments. Unset Printing Implicit Defensive. Unset Strict Implicit. (* inversion tactics *) Ltac inversion' H := inversion H; subst; clear H. (* useful lemma to exploit hypotheses *) 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'. Proof. induction h; intros; destruct h'; simpl in *; dependent destruction H; eauto. specialize (IHh _ _ _ x). intuition; subst; auto. destruct IHh; intuition; subst; eauto. Qed. Lemma nil_app: forall (h k: list A), [] = h++k -> []=h /\ []=k. Proof. intros. destruct h; destruct k; auto; discriminate. Qed. Lemma consnil_app: forall u (h k: list A), [u] = h++k -> [u]=h /\ []=k \/ []=h /\ [u]=k. Proof. intros. destruct h; dependent destruction H; auto. apply nil_app in x. intuition; subst. auto. Qed. 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. Proof. intros. destruct h; dependent destruction H; eauto. Qed. 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'. Proof. induction h; intros; destruct h'; simpl in *; dependent destruction H; eauto. specialize (IHh _ _ _ x). intuition; subst; auto. destruct IHh; intuition; subst; eauto. Qed. Inductive perm: relation (list A) := | perm_app: forall h k, perm (h++k) (k++h). Global Instance perm_equivalence: Equivalence perm. Proof. constructor; red; intros. rewrite app_nil_end. apply (perm_app [] x). inversion' H. constructor. inversion' H. inversion' H0. apply app_app in H1 as [l ?]. intuition; subst. rewrite <- app_ass. rewrite app_ass at 1. constructor. rewrite app_ass. rewrite <- app_ass. constructor. Qed. Infix " (=) " := perm (at level 80). Lemma permut_cons: forall u l k, l++[u] (=) k -> u::l (=) k. Proof. intros. rewrite perm_app in H. assumption. Qed. Lemma permut_app: forall h l k, l++h (=) k -> h++l (=) k. Proof. intros. rewrite perm_app. assumption. Qed. Lemma pmor1: forall P: list A -> Prop, (forall a l, P (l++[a]) -> P (a::l)) -> Proper (perm ==> iff) P. Proof. intros P HP. assert (forall k h, P (h++k) -> P (k++h)). induction k; intros. rewrite <- app_nil_end in H. assumption. simpl; apply HP. rewrite app_ass. apply IHk. rewrite app_ass. assumption. repeat intro. inversion' H0. split; auto. Qed. End perm. (** equality of lists, modulo cyclic permutations *) Infix " (=) " := perm (at level 80). Hint Extern 0 (_ (=) _) => reflexivity. (* tactic to solve cyclic permutations automatically *) Hint Rewrite app_ass : permut_norm. (* normalise concatenations (associativity), in goal and hypotheses *) Ltac permut_norm := repeat (simpl in *; autorewrite with permut_norm in *). (* rotate the left-hand side until reflexivity or until an assumption is obtained *) Ltac solve_perm_aux := permut_norm; solve [ auto | apply permut_cons; solve_perm_aux | apply permut_app; solve_perm_aux ]. (* final tactic: clear useless hypotheses *) Ltac solve_perm := repeat match goal with H: _ (=) _ |- _ => fail | H: _ |- _ => clear H end; solve_perm_aux. (** [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 (* | top: T *) (* | zer: T *) | var: X -> T | rav: 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 | par _ _ => idtac | wit _ _ => idtac | opl _ _ => idtac | var _ => idtac | rav _ => idtac | one => idtac | bot => idtac (* | top => idtac *) (* | zer => idtac *) | [] => idtac | _::_ => idtac end. (** printing $ #$# *) (** notations *) (* $ means \parr *) Delimit Scope U_scope with U. Open Scope U_scope. 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. (* Notation "⊤" := (top): U_scope. *) (* Notation "0" := (zer): 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 (* | 0 => ⊤ *) (* | ⊤ => 0 *) | var i => rav i | rav i => var i end. Lemma dual_invol: forall u, dual (dual u) = u. Proof. induction u; simpl; congruence. Qed. Lemma dual_inj: forall u v, dual u = dual v -> u = v. Proof. intros. rewrite <- (dual_invol u), <- (dual_invol v). rewrite H. reflexivity. Qed. (** 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_top: input ⊤ *) (* | i_zer: input 0 *) | 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_top: output ⊤ *) (* | o_zer: output 0 *) | o_wit: forall a b, output a -> output b -> output (a & b) | o_opl: forall a b, output a -> output b -> output (a ⨁ b) . Hint Constructors input output. (** input lists *) Inductive linput: list T -> Prop := | i_nil: linput nil | i_cons: forall i l, input i -> linput l -> linput (i::l). Hint Constructors linput. (** 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). Proof. induction 1; intros; simpl; auto. induction 1; intros; simpl; auto. Qed. (** lemmas about input lists *) Lemma i_app_inv: forall h k, linput (h++k) -> linput h /\ linput k. Proof. induction h; intros. auto. inversion' H. apply IHh in H3. intuition; auto. Qed. (* inversion of input/output hypotheses *) Ltac inverse_io := repeat match goal with | H: linput (_++_) |- _ => apply i_app_inv in H as [? ?] | H: linput ?u |- _ => is_constr u; inversion' H | H: input ?u |- _ => is_constr u; inversion' H | H: output ?u |- _ => is_constr u; inversion' H end. Lemma i_app: forall h k, linput h -> linput k -> linput (h++k). Proof. induction h; intros; inverse_io; simpl; auto. Qed. Hint Resolve i_app. (* inversion of list equalities, to do case analysis with cyclic permutation hypotheses *) Ltac inverse_app := repeat match goal with | H: [] = _++_ |- _ => apply nil_app in H; destruct H; subst | H: [_] = _++_ |- _ => apply consnil_app in H; destruct H as [[? ?]|[? ?]]; subst | H: _::_ = _++_ |- _ => apply cons_app in H; destruct H as [[? ?]|[? [? ?]]]; subst | H: [_] = [_] |- _ => dependent destruction H | H: _ :: _ = _ :: _ |- _ => dependent destruction H end. 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_top: forall n m, typed n m ⊤ *) (* | t_zer: forall n m, typed n m 0 *) | 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). Hint Constructors typed ltyped. 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. 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'). Proof. induction l; intros. eauto. inversion' H. destruct (IHl _ _ _ H5). 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. (** linear negation mirrors types *) Lemma t_dual: forall u n m, typed n m u -> typed m n (dual u). Proof. induction 1; simpl; eauto. Qed. Hint Resolve t_dual. Lemma t_ldual: forall l n m, ltyped n m l -> ltyped m n (ldual l). Proof. induction 1; simpl; eauto. Qed. Hint Resolve t_ldual. (** 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'. Proof. induction 1; intros; inverse_types; intuition (subst; auto). eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto). eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto). Qed. 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'. Proof. induction 1; intros; inverse_types; intuition (subst; auto). destruct (typed_inj H H6); intuition (subst; auto). apply IHltyped in H0. apply IHltyped in H7. intuition (subst; auto). Qed. (* unification of pre-types by the injectivity property (with case analysis) *) Ltac injective_types := repeat match goal with | H1: typed _ _ ?u, H2: typed _ _ ?u |- _ => destruct (typed_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2 | H1: ltyped _ _ ?u, H2: ltyped _ _ ?u |- _ => destruct (ltyped_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2 end. (** 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_top: forall l n, ltyped n 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 (* m *), (* typed n m a -> typed n m b -> ltyped m n l -> *) 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 -> (* ltyped m n l -> *) 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 -> (* ltyped m n l -> *) seq n (b::l) -> seq n (a ⨁ b::l) | seq_rot: forall a l n m, typed n m a -> (* ltyped m n l -> *) seq m (l++[a]) -> seq n (a::l). Hint Constructors seq. (** sanity check: derivable sequents have square types *) Lemma seq_typed: forall l n, seq n l -> ltyped n n l. Proof. induction 1; intuition (inverse_types; injective_types; eauto). Qed. (* apply a rotation to the current goal *) Ltac rot := eapply seq_rot; eauto; simpl. (** 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). Proof. intros h l n m ltyp. revert l. induction ltyp; simpl; intros; inverse_types. rewrite <- app_nil_end in H. assumption. rot. rewrite app_ass. apply IHltyp. rewrite app_ass. assumption. Qed. (** 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). Proof. intros. eapply (seq_rot' (h:=a ⨂ b::h)). apply seq_typed in H0. apply seq_typed in H1. inverse_types; injective_types; eauto. apply seq_dot; trivial. eapply seq_rot'; eauto. apply seq_typed in H0. inverse_types; injective_types; eauto. Qed. (** the sequent system is "reflexive" *) Lemma seq_refl: forall u n m, typed n m u -> seq m [dual u; u]. Proof. induction 1; simpl; eauto. rot. trivial. rot. eauto. apply seq_par. rot. refine (seq_dot (l:=[dual u]) _ _); eauto. rot. apply seq_par. rot. eauto 6. refine (seq_dot (l:=[v]) _ _); simpl; eauto. rot. eapply seq_wit; eauto; rot; eauto. eapply seq_wit; eauto; rot; eauto 7. Qed. (** input sequents cannot be proved *) Lemma linput_not_seq: forall l n, seq n l -> linput l -> False. Proof. induction 1; intros; inverse_io; auto. Qed. (** 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). Proof. Abort. 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). Hint Constructors seq typed ltyped. Hint Resolve t_app. (** terms and lists are always untyped *) Lemma always_untyped: forall u, typed ttt ttt tt tt u. Proof. induction u; eauto. generalize (t_var ttt ttt x); destruct (ttt x); auto. generalize (t_rav ttt ttt x); destruct (ttt x); auto. Qed. Lemma always_luntyped: forall l, ltyped ttt ttt tt tt l. Proof. induction l; eauto using always_untyped. 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. (* clearing useless hypotheses *) Ltac clean_untyped := repeat match goal with | t: unit |- _ => destruct t | H: untyped _ |- _ => clear H end. 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. Proof. (* generalisation: types of cyclic permutations of derivable sequents are squares *) assert (G: forall l, useq l -> forall h k n m, l=h++k -> ltyped n m (k++h) -> n=m). induction 1; intros; inverse_app; inverse_types; auto; clean_untyped. apply (IHseq nil l); trivial. rewrite <-app_nil_end. assumption. eauto. apply split_select in H1 as [h' ?]; intuition; subst; inverse_app; inverse_types. specialize (IHseq2 nil (b::h) m1 x refl). apply apply in IHseq2. 2: eauto. subst. apply (IHseq1 h0 (h'++[a])). apply app_ass. eauto. specialize (IHseq2 nil (b::h) m1 x refl). apply apply in IHseq2. 2: eauto. subst. eauto. specialize (IHseq1 nil (l++[a]) x m1 refl). apply apply in IHseq1. 2: eauto. subst. apply (IHseq2 (b::x0) k _ _ refl); eauto. apply (IHseq nil _ _ _ refl). rewrite <-app_nil_end. eauto. apply (IHseq (a::b::x) _ _ _ refl); eauto. apply (IHseq1 nil _ _ _ refl); eauto. apply (IHseq1 (a::x) _ _ _ refl); eauto. apply (IHseq nil _ _ _ refl); eauto. apply (IHseq (a::x) _ _ _ refl); eauto. apply (IHseq nil _ _ _ refl); eauto. apply (IHseq (b::x) _ _ _ refl); eauto. apply (IHseq l [a] _ _ refl); eauto. apply (IHseq x (k++[a])); eauto. apply app_ass. intros l H n m Hnm. apply (G _ H nil _ _ _ refl). rewrite <- app_nil_end. assumption. Qed. (** untyping theorem for cyclic MALL *) Theorem untype: forall l, useq l -> forall n, ltyped n n l -> seq n l. Proof. induction 1; intros; clean_untyped; inverse_types; eauto 6. assert (n0 = m0). eapply useq_mono in H0. 2: eauto. auto. subst. eauto 7. Qed. (** typed derivable sequents are untyped derivable *) Lemma erase: forall l n, seq n l -> useq l. Proof. induction 1; eauto using always_untyped. generalize (seq_ax ttt ttt i); destruct (ttt i); auto. Qed. End erase. End MALL. (** ** Untyping theorem for non commutative IMALL without additive constant, i.e., residuated lattices without bounds ## *) Module IMALL. Import MALL. Hint Resolve t_dual t_ldual dual_input dual_output. (** 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. (* 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 | ldv _ _ => idtac | rdv _ _ => idtac | inf _ _ => idtac | sup _ _ => idtac | var _ => idtac | one => idtac | [] => idtac | _::_ => idtac end. (** notations *) Delimit Scope V_scope with V. Open Scope V_scope. 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. Proof. induction h; intro; simpl. rewrite <- app_nil_end. reflexivity. rewrite IHh, app_ass. reflexivity. Qed. (** the encoding produces output formulae *) Lemma to_MALL_output: forall u, MALL.output (to_MALL u). Proof. induction u; simpl; auto using MALL.dual_input, MALL.dual_output. Qed. (** the encoding of list produces lists of input formulae *) Lemma lto_MALL_linput: forall l, MALL.linput (lto_MALL l). Proof. induction l; simpl; auto. apply MALL.i_app; trivial. constructor; trivial. apply MALL.dual_output, to_MALL_output. Qed. (* inversion on list equalities, to reason by case analysis about cyclic permutations *) Ltac inverse_app := repeat ( simpl in *; match goal with | H: [] = _::_ |- _ => discriminate H | H: _::_ = [] |- _ => discriminate H | H: _ (=) _ |- _ => inversion' H | H: [_] = [_] |- _ => inversion' H | H: _ :: _ = _ :: _ |- _ => inversion' H | H: _++_ = _++_ |- _ => apply app_app in H; destruct H as [? [[? ?]|[? ?]]]; subst | H: [] = _++_ |- _ => apply nil_app in H; destruct H; subst | H: _ ++ _ = [] |- _ => symmetry in H; apply nil_app in H; destruct H; subst | H: [_] = _++_ |- _ => apply consnil_app in H; destruct H as [[? ?]|[? ?]]; subst | H: _++_ = [_] |- _ => symmetry in H; apply consnil_app in H; destruct H as [[? ?]|[? ?]]; subst | H: _::_ = _++_ |- _ => apply cons_app in H; destruct H as [[? ?]|[? [? ?]]]; subst | H: _++_ = _::_ |- _ => symmetry in H; apply cons_app in H; destruct H as [[? ?]|[? [? ?]]]; subst | H: context[ _++[] ] |- _ => rewrite <- app_nil_end in H end). (** 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. Proof. induction q; simpl; intros. inverse_app. exists (@nil T). exists (@nil T). auto. inverse_app. exists (a::q). exists (@nil T). auto. exists q. exists [a]. intuition; auto. symmetry in H. apply IHq in H as (?&?&?&?&?). exists x0. exists (a::x1). simpl. rewrite H, H0, H1. auto. Qed. (** 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. Proof. induction q; simpl; intros. inverse_app. inverse_app. destruct q; inverse_app. exists (a). exists (@nil T). simpl. rewrite MALL.dual_invol. auto. symmetry in H. apply IHq in H as (?&?&?&?&?). subst. exists x0. exists (a::x1). simpl. auto. Qed. (* systematic case analysis *) Ltac inverse_conv := repeat match goal with | H: dual _ = dual _ |- _ => apply dual_inj in H | H: dual _ = _ |- _ => rewrite <- dual_invol in H; apply dual_inj in H | H: to_MALL _ = _ |- _ => symmetry in H | H: lto_MALL _ = _ |- _ => symmetry in H | H: ?x = to_MALL ?w |- _ => MALL.is_constr x; destruct w; try discriminate H; simpl in H; inversion' H | H: ?x = dual (to_MALL ?w) |- _ => MALL.is_constr x; destruct w; try discriminate H; simpl in H; inversion' H | H: [] = lto_MALL ?w |- _ => destruct w; [clear H| inverse_app] | H: _::_ = lto_MALL ?w |- _ => apply lto_MALL_cons_inv in H as (?&?&->&?&?); simpl in * | H: _++_ = lto_MALL ?w |- _ => apply lto_MALL_app_inv in H as (?&?&->&?&?) end. Ltac inverse := repeat progress (inverse_app; inverse_conv). 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). Hint Constructors typed ltyped. 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. 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'). Proof. induction l; intros. eauto. inversion' H. destruct (IHl _ _ _ H5). eauto. Qed. (* inversion on 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. (** 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'. Proof. induction 1; intros; inverse_types; intuition (subst; auto). eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto). eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto). eapply apply in IHtyped1; eauto. eapply apply in IHtyped2; eauto. intuition (subst; auto). Qed. 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'. Proof. induction 1; intros; inverse_types; intuition (subst; auto). destruct (typed_inj H H6); intuition (subst; auto). apply IHltyped in H0. apply IHltyped in H7. intuition (subst; auto). Qed. (* unification of pre-types by the injectivity property (with case analysis) *) Ltac injective_types := repeat match goal with | H1: typed _ _ ?u, H2: typed _ _ ?u |- _ => destruct (typed_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2 | H1: ltyped _ _ ?u, H2: ltyped _ _ ?u |- _ => destruct (ltyped_inj H1 H2) as [[? ?]|[? ?]]; repeat subst; clear H2 end. (** 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). Proof. induction 1; simpl; eauto. Qed. Lemma ltyped_to_MALL: forall l n m, ltyped n m l -> MALL.ltyped s t m n (lto_MALL l). Proof. induction 1; simpl; eauto using typed_to_MALL. Qed. Lemma to_MALL_typed: forall u n m, MALL.typed s t n m (to_MALL u) -> typed n m u. Proof. induction u; simpl; intros; MALL.inverse_types; eauto. apply t_dual in H4. rewrite dual_invol in H4. eauto. apply t_dual in H5. rewrite dual_invol in H5. eauto. Qed. Lemma to_MALL_ltyped: forall l n m, MALL.ltyped s t n m (lto_MALL l) -> ltyped m n l. Proof. induction l; simpl; intros; MALL.inverse_types; eauto. apply t_dual in H5. rewrite dual_invol in H5. eauto using to_MALL_typed. Qed. (** 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. Proof. induction 1; intuition (inverse_types; injective_types; eauto). Qed. Hint Rewrite lto_MALL_app : permut_norm. (** "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. Proof. cut (forall l0, useq l0 -> forall n m l u, ltyped n m l -> typed n m u -> to_MALL u::lto_MALL l (=) l0 -> leq n m l u). intros H n m l u Hl Hu Hlu. eapply H; eauto. induction 1; intros p q k u Hk Hu Heq. inverse. inverse_types. constructor. inverse; inverse_types; constructor. inverse; inverse_types. rewrite app_ass. constructor. apply IHseq; eauto. solve_perm. inverse; subst; inverse_types; clean_untyped. eapply useq_mono in H0. 2: eauto using typed_to_MALL, ltyped_to_MALL. subst. econstructor. apply IHseq1; eauto. solve_perm. apply IHseq2; trivial. eapply useq_mono in H. 2: eauto using typed_to_MALL, ltyped_to_MALL. subst. eapply (dot_intro (l:=[]) (l':=k)); eauto. eapply useq_mono in H0. 2: eauto using typed_to_MALL, ltyped_to_MALL. subst. rewrite app_ass. simpl. eapply (ldv_elim (l:=[])); eauto. elim (linput_not_seq H0). auto using to_MALL_output, lto_MALL_linput. elim (linput_not_seq H). auto using to_MALL_output, lto_MALL_linput. eapply useq_mono in H. 2: eauto using typed_to_MALL, ltyped_to_MALL. subst. rewrite 2app_ass. simpl. econstructor; eauto. apply IHseq1; eauto. solve_perm. apply IHseq2; eauto. solve_perm. eapply useq_mono in H. 2: eauto using typed_to_MALL, ltyped_to_MALL. subst. econstructor; eauto. apply IHseq1; eauto. solve_perm. eapply useq_mono in H0. 2: eauto using typed_to_MALL, ltyped_to_MALL. subst. rewrite app_ass. econstructor; eauto. apply IHseq1; eauto. solve_perm. elim (linput_not_seq H0). auto using to_MALL_output, lto_MALL_linput. inverse; inverse_types. econstructor; eauto. apply IHseq; eauto. solve_perm. econstructor; eauto. apply IHseq; eauto. solve_perm. econstructor; eauto. apply IHseq; eauto. solve_perm. econstructor; eauto. apply IHseq; eauto. solve_perm. rewrite app_ass. constructor. apply IHseq; eauto. solve_perm. inverse; inverse_types. constructor; eauto. constructor; eauto. rewrite app_ass. econstructor; eauto. apply IHseq1; eauto. solve_perm. apply IHseq2; eauto. solve_perm. inverse; inverse_types. apply sup_intro_r; auto. apply sup_intro_r; auto. rewrite app_ass. eapply inf_elim_l; eauto. apply IHseq; eauto. solve_perm. inverse; inverse_types. apply sup_intro_l; auto. apply sup_intro_l; auto. rewrite app_ass. eapply inf_elim_r; eauto. apply IHseq; eauto. solve_perm. inverse; subst; inverse_types; apply IHseq; eauto; solve_perm. Qed. 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). Hint Constructors typed. Lemma always_untyped: forall u, typed ttt ttt tt tt u. Proof. induction u; eauto. generalize (t_var ttt ttt x); destruct (ttt x); auto. Qed. Hint Constructors ltyped. Lemma always_luntyped: forall l, ltyped ttt ttt tt tt l. Proof. induction l; eauto using always_untyped. Qed. Hint Resolve MALL.always_untyped MALL.always_luntyped. Hint Rewrite lto_MALL_app dual_invol : permut_norm. (* apply a rotation to the current sequent *) Ltac rot := permut_norm; (eapply seq_rot' || eapply seq_rot); permut_norm; eauto. Ltac solve_rot := repeat rot. (** 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). Proof. induction 1; clean_untyped; permut_norm. rot. generalize (MALL.seq_ax ttt ttt i); destruct (ttt i); auto. constructor. rot. rot. constructor. solve_rot. eapply seq_dot'; eauto. rot. rot. constructor. solve_rot. constructor. assumption. rot. rot. econstructor; eauto. solve_rot. solve_rot. constructor. solve_rot. rot. rot. eapply seq_dot'; eauto. solve_rot. constructor; trivial. rot. rot. eapply seq_opl_l; eauto. solve_rot. rot. rot. eapply seq_opl_r; eauto. solve_rot. eauto. eauto. rot. rot. econstructor; eauto; solve_rot. Qed. Section erase. Variable I: Set. Variables s t: X -> I. Hint Constructors leq. 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. Proof. intros l u Hlu n m Hl Hu. apply uMALL_to_IMALL; trivial. apply uIMALL_to_uMALL, Hlu. Qed. (** typed derivable sequents are untyped derivable (straightforward) *) Lemma erase: forall l u n m, leq n m l u -> uleq l u. Proof. induction 1; eauto using always_untyped, always_luntyped. generalize (leq_var ttt ttt i); destruct (ttt i); auto. Qed. (** 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). Proof. intros. apply MALL.untype. apply uIMALL_to_uMALL. eapply erase. eassumption. apply leq_typed in H. intuition eauto using typed_to_MALL, ltyped_to_MALL. Qed. 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. Proof. intros. eauto using uMALL_to_IMALL, MALL.erase. Qed. End erase. End IMALL.