Library BioFLL.LL.Syntax


Syntax of Linear Logic

Formulas in LL are build from the following syntax
F:= A | A ^ | ⊤ | ⊥ | 0 | 1 | F ** F | F $ F | F ⊕ F | F & F | ! F | ? F 
    | E{ FX} | F{ FX}
where
  • A is an atom.
  • A ^ is the negation of the atom A.
  • ⊤,⊥,0,1 are the units
  • F ** F is multiplicative conjunction (tensor)
  • F $ F is multiplicative disjunction (par)
  • F & F is additive conjunction (with)
  • F F is additive disjunction (oplus)
  • !, ? are the exponentials.
  • E {FX} existential quantifier
  • F {FX} universal quantifier
The usual dualities, moving negation inwards, can be computed by Dual_LExp (notation A°).
The linear implication F -o F is defined as A° $ B.
The weight (or complexity) of a formula can be obtained via Lexp_weight.
This file also defines the polarity of formulas following Andreoli's focused system (https://www.cs.cmu.edu/~fp/courses/15816-s12/misc/andreoli92jlc.pdf). Many lemmas on polarities are proved in Section Polarities.


Module Syntax_LL (DT : Eqset_dec_pol).
  Export DT.

Parametric HOAS

Take a look on < a href="http://adam.chlipala.net/cpdt/html/Hoas.html">Library Hoas.
  Section Sec_lExp.
    Variable T : Type.
    Inductive term :=
    |var (t: T)
    |cte (e:A)
    |fc1 (n:nat) (t: term)
    |fc2 (n:nat) (t1 t2: term).
    Inductive aprop :=
    | ap : nat list term aprop.

    Inductive lexp :=
    | atom (a :aprop)
    | perp (a: aprop)
    | top | bot | zero | one
    | tensor (F G : lexp)
    | par (F G : lexp)
    | plus (F G : lexp)
    | witH (F G : lexp)
    | bang (F : lexp)
    | quest (F : lexp)
    | ex (f : T lexp)
    | fx (f : T lexp) .
  End Sec_lExp.

  Arguments var [T]. Arguments cte [T].
  Arguments fc1 [T]. Arguments fc2 [T].
  Arguments ap [T].
  Arguments atom [T]. Arguments perp [T].
  Arguments top [T]. Arguments one [T]. Arguments bot [T]. Arguments zero [T].
  Arguments tensor [T]. Arguments par [T]. Arguments plus [T]. Arguments witH [T].
  Arguments bang [T]. Arguments quest [T].
  Arguments ex [T]. Arguments fx [T].

Types for lexp
  Definition Term := T:Type, term T.
  Definition LTerm := list Term.

  Definition AProp := T:Type, aprop T.
  Definition Lexp := T:Type, lexp T.
  Definition Subs := T:Type, T lexp T.
  Definition SubsL := list Subs.
Useful Constructors (poly version of the connectives)
  Definition Cte (t : A) : Term := fun _cte t.
  Definition FC1 (n:nat) (t:Term): Term := fun _fc1 n (t _).
  Definition FC2 (n:nat) (t t':Term): Term := fun _fc2 n (t _) (t' _).
  Definition AP (n : nat) (l : list Term) : AProp := fun _ap n ( map (fun xx _) l) .
  Definition Atom (P: AProp) :Lexp := fun _atom (P _).
  Definition Perp (P: AProp) :Lexp := fun _perp(P _).
  Definition Top :Lexp := fun _top .
  Definition Bot :Lexp := fun _bot.
  Definition One :Lexp := fun _one.
  Definition Zero :Lexp := fun _zero .
  Definition Tensor (F G: Lexp) :Lexp := fun _tensor (F _) (G _).
  Definition Par (F G: Lexp) :Lexp := fun _par (F _) (G _).
  Definition Plus (F G: Lexp) :Lexp := fun _plus (F _) (G _).
  Definition With (F G: Lexp) :Lexp := fun _witH (F _) (G _).
  Definition Bang (F: Lexp) :Lexp := fun _bang (F _ ).
  Definition Quest (F: Lexp) :Lexp := fun _quest (F _ ).
  Definition Ex (Fx : Subs) : Lexp := fun _ex (Fx _).
  Definition Fx (Fx : Subs) : Lexp := fun _fx (Fx _).

Closed Terms
  Inductive ClosedT : Term Prop :=
  | cl_cte: C, ClosedT (Cte C)
  | cl_fc1: n t1, ClosedT t1 ClosedT (FC1 n t1)
  | cl_fc2: n t1 t2, ClosedT t1 ClosedT t2 ClosedT (FC2 n t1 t2).

Closed Atomic Propositions
  Inductive ClosedA : AProp Prop :=
  | cl_ap : n l, Forall ClosedT l ClosedA (AP n l).

Closed Formulas
  Inductive Closed : Lexp Prop :=
  | cl_atom : A, ClosedA A Closed (Atom A )
  | cl_perp : A, ClosedA A Closed (Perp A )
  | cl_one : Closed One
  | cl_bot : Closed Bot
  | cl_zero : Closed Zero
  | cl_top : Closed Top
  | cl_tensor : F G, Closed F Closed G Closed (Tensor F G)
  | cl_par : F G, Closed F Closed G Closed (Par F G)
  | cl_plus : F G, Closed F Closed G Closed (Plus F G)
  | cl_with : F G, Closed F Closed G Closed (With F G)
  | cl_bang : F, Closed F Closed (Bang F)
  | cl_quest : F, Closed F Closed (Quest F)
  | cl_ex : FX, Closed (Ex FX)
  | cl_fx : FX, Closed (Fx FX).

Axioms of Closedeness
  Axiom ax_closedT : X:Term, ClosedT X.
  Axiom ax_closedA : A: AProp, ClosedA A.
  Axiom ax_closed : F:Lexp, Closed F.

We assume equality on formulas to be decidable
  Axiom FEqDec : (F G: Lexp ), {F = G} + {F G}.
  Lemma not_eqLExp_sym : x y: Lexp, x y y x.
  Proof. intuition.
  Qed.

Case analysis on a formula
  Ltac caseLexp F :=
    let Hx := fresh "HF" in
    assert(Hx : Closed F) by (apply ax_closed);
    inversion Hx.
Induction on a formula
  Ltac indLexp F :=
    let Hx := fresh "HF" in
    assert(Hx : Closed F) by (apply ax_closed);
    induction Hx.
Dealing with equality on LExp
  Ltac lexp_contr H :=
    eapply @equal_f_dep with (x:=unit) in H;
    inversion H.
  Ltac lexp_contr_unit H :=
    eapply @equal_f_dep with (x:=unit) in H;
    inversion H.
  Ltac LexpContr :=
    try(match goal with [H : ?F = ?G |- _] ⇒
                        assert(False) by lexp_contr_unit H;contradiction
        end).

Dualities on formulas
  Section Dualities.
    Variable T: Type.
Dualilities
    Fixpoint dual_LExp (X: lexp T) :=
      match X with
      | atom Aperp A
      | perp Aatom A
      | onebot
      | botone
      | zerotop
      | topzero
      | tensor F Gpar (dual_LExp F) (dual_LExp G)
      | par F Gtensor (dual_LExp F) (dual_LExp G)
      | plus F GwitH (dual_LExp F) (dual_LExp G)
      | witH F Gplus (dual_LExp F) (dual_LExp G)
      | bang Fquest (dual_LExp F)
      | quest Fbang (dual_LExp F)
      | ex Xfx (fun xdual_LExp (X x))
      | fx Xex (fun xdual_LExp (X x))
      end.

    Theorem ng_involutive: F: lexp T, F = dual_LExp (dual_LExp F).
    Proof.
      intro.
      induction F; simpl; auto;
        try( try(rewrite <- IHF1); try(rewrite <- IHF2); try(rewrite <- IHF);auto);
        try(assert (f = fun xdual_LExp (dual_LExp (f x))) by
               (extensionality t; apply H); rewrite <- H0; auto).
    Qed.

Linear implication
    Definition imp (A B: lexp T): lexp T := par (dual_LExp A) B.
  End Dualities.

  Arguments dual_LExp [T].

  Definition Imp (A B : Lexp) : Lexp := fun _imp (A _) (B _).
  Definition Dual_LExp (X: Lexp) : Lexp := fun _dual_LExp (X _).

Notation on Formulas
  Module LLNotation.
    Notation "⊥" := Bot.
    Notation "⊤" := Top.
    Notation "A ** B" := (Tensor A B) (at level 50) .
    Notation "A $ B" := (Par A B) (at level 50) .
    Notation "A ⊕ B" := (Plus A B) (at level 50).
    Notation "A & B" := (With A B) (at level 50) .
    Notation "! A" := (Bang A) (at level 50) .
    Notation "? A" := (Quest A) (at level 50) .
    Notation "A ⁺" := (Atom A) (at level 10) .
    Notation "A ⁻" := (Perp A) (at level 10) .
    Notation "'F{' FX '}'" := (Fx FX) (at level 10) .
    Notation "'E{' FX '}'" := (Ex FX) (at level 10) .
    Notation "P °" := (Dual_LExp P) (at level 1, left associativity, format "P °").
    Notation"A -o B" := (Imp A B) (at level 70).
  End LLNotation.

  Export LLNotation.

  Lemma one_bot : One° = .
  Proof. auto. Qed.
  Lemma bot_one : ° = One.
  Proof. auto. Qed.
  Lemma top_zero : ° = Zero.
  Proof. auto. Qed.
  Lemma zero_top : Zero° = .
  Proof. auto. Qed.
  Lemma atom_perp A: (A = A .
  Proof. auto. Qed.
  Lemma perp_atom A: (A = A .
  Proof. auto. Qed.
  Lemma tensor_par A B: (A ** B = A° $ B°.
  Proof. extensionality T. apply @equal_f_dep. auto. Qed.
  Lemma par_tensor A B: (A $ B = A° ** B°.
  Proof. extensionality T. apply @equal_f_dep. auto. Qed.
  Lemma with_plus A B: (A & B = A° B°.
  Proof. extensionality T. apply @equal_f_dep. auto. Qed.
  Lemma plus_with A B: (A B = A° & B°.
  Proof. extensionality T. apply @equal_f_dep. auto. Qed.
  Lemma bang_quest A: (! A = ? A°.
  Proof. auto. Qed.
  Lemma quest_bang A: (? A = ! A°.
  Proof. auto. Qed.
  Lemma fx_ex FX: F{FX}° = Ex (fun _ xdual_LExp(FX _ x)).
  Proof. extensionality T. apply @equal_f_dep. auto. Qed.
  Lemma ex_fx FX: E{FX}° = Fx (fun _ xdual_LExp(FX _ x)).
  Proof. extensionality T. apply @equal_f_dep. auto. Qed.
  Lemma AtomNeg : A, (A = A .
    auto.
  Qed.
  Lemma AtomPos : A, (A = A .
    auto.
  Qed.
  Lemma Neg2pos: A, Atom A = Dual_LExp (Perp A).
  Proof.
    auto.
  Qed.
  Theorem Ng_involutive: F: Lexp, F = Dual_LExp (Dual_LExp F).
  Proof.
    intro.
    unfold Dual_LExp.
    extensionality T.
    rewrite <- ng_involutive with (T:=T);auto.
  Qed.

  Hint Rewrite Neg2pos Ng_involutive.

Substitutions
  Section Substitution.
    Variable T : Type.
    Fixpoint flattenT (t : term ( (term T))) : term T :=
      match t with
      | var xx
      | cte xcte x
      | fc1 n xfc1 n (flattenT x)
      | fc2 n x yfc2 n (flattenT x) (flattenT y)
      end.

    Fixpoint flatten (e : lexp ( (term T))) : lexp ( T) :=
      match e with
      | atom (ap n l) ⇒ atom (ap n (map flattenT l))
      | perp (ap n l) ⇒ perp (ap n (map flattenT l))
      | toptop
      | botbot
      | zerozero
      | oneone
      | tensor F Gtensor (flatten F) (flatten G)
      | par F Gpar (flatten F) (flatten G)
      | plus F Gplus (flatten F) (flatten G)
      | witH F GwitH (flatten F) (flatten G)
      | bang Fbang (flatten F)
      | quest Fquest (flatten F)
      | ex FXex (fun xflatten (FX (var x)))
      | fx FXfx (fun xflatten (FX (var x)))
      end.
  End Substitution.

Polymorphic version of substitutions
  Definition Subst (S : Subs ) (X : Term) : Lexp :=
    fun T:Typeflatten (S (term T) (X T)).

  Fixpoint SubstL (S : SubsL ) (X : Term) : list Lexp := map (fun sSubst s X) S.
  Hint Unfold Subst .

Equality on LExp Formulas

  Section EqualityFormulas.
    Lemma AtomEq: A A', Atom A = Atom A' A = A'.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma PerpEq: A A', Perp A = Perp A' A = A'.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma ParEq1 : F G F0 G0, F0 $ G0 = F $ G F = F0.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma ParEq2 : F G F0 G0, F0 $ G0 = F $ G G = G0.
      intros. extensionality T.
      apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma WithEq1 : F G F0 G0, F0 & G0 = F & G F = F0.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma WithEq2 : F G F0 G0, F0 & G0 = F & G G = G0.
      intros. extensionality T.
      apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma TensorEq1 : F G F0 G0, F0 ** G0 = F ** G F = F0.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma TensorEq2 : F G F0 G0, F0 ** G0 = F ** G G = G0.
      intros. extensionality T.
      apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma PlusEq1 : F G F0 G0, F0 G0 = F G F = F0.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma PlusEq2 : F G F0 G0, F0 G0 = F G G = G0.
      intros. extensionality T.
      apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma BangEq : F F', ! F = ! F' F = F'.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma QuestEq : F F', ? F = ? F' F = F'.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma FxEq : F F', F{ F } = F{ F' } F = F'.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma ExEq : F F', E{ F } = E{ F' } F = F'.
      intros.
      extensionality T. apply @equal_f_dep with (x:=T) in H.
      inversion H. auto.
    Qed.

    Lemma CteEqt : t t', Cte t = Cte t' t = t'.
      intros.
      apply @equal_f_dep with (x:=unit) in H.
      inversion H;auto.
    Qed.

    Lemma F1Eqn : n n' t t', FC1 n t = FC1 n' t' n = n'.
      intros.
      apply @equal_f_dep with (x:=unit) in H.
      inversion H;auto.
    Qed.

    Lemma F1Eqt : n n' t t', FC1 n t = FC1 n' t' t = t'.
      intros.
      extensionality T.
      apply @equal_f_dep with (x:=T) in H.
      inversion H;auto.
    Qed.

    Lemma F2Eqn : n1 n2 t1 t1' t2 t2', FC2 n1 t1 t2 = FC2 n2 t1' t2' n1 = n2.
      intros.
      apply @equal_f_dep with (x:=unit) in H.
      inversion H;auto.
    Qed.

    Lemma F2Eqt1 : n1 n2 t1 t1' t2 t2', FC2 n1 t1 t2 = FC2 n2 t1' t2' t1 = t1'.
      intros.
      extensionality T.
      apply @equal_f_dep with (x:=T) in H.
      inversion H;auto.
    Qed.

    Lemma F2Eqt2 : n1 n2 t1 t1' t2 t2', FC2 n1 t1 t2 = FC2 n2 t1' t2' t2 = t2'.
      intros.
      extensionality T.
      apply @equal_f_dep with (x:=T) in H.
      inversion H;auto.
    Qed.

    Lemma Terms_cte_fc1 : t n t', Cte t FC1 n t'.
      intros t n t' Hn.
      apply @equal_f_dep with (x:=unit) in Hn.
      inversion Hn.
    Qed.

    Lemma Terms_cte_fc2 : t n t' t'', Cte t FC2 n t' t''.
      intros t n t' t'' Hn.
      apply @equal_f_dep with (x:=unit) in Hn.
      inversion Hn.
    Qed.

    Lemma Terms_fc1_fc2 : t n t' t'' n', FC1 n t FC2 n' t' t''.
      intros t n t' t'' n' Hn.
      apply @equal_f_dep with (x:=unit) in Hn.
      inversion Hn.
    Qed.

    Lemma APInv : n m l l', AP n l = AP m l' n = m.
      intros.
      unfold AP in H.
      apply @equal_f_dep with (x:=unit) in H.
      inversion H;auto.
    Qed.

    Lemma APInvL : n m l l', AP n l = AP m l' l = l'.
      induction l;intros;
        unfold AP in H.
      + apply @equal_f_dep with (x:=unit) in H;
          inversion H;auto.
        symmetry in H2.
        apply map_eq_nil in H2;auto.
      + destruct l'.
        ++ simpl in H.
            apply @equal_f_dep with (x:=unit) in H; inversion H;auto.
        ++ assert(a= t).
           extensionality T.
           apply @equal_f_dep with (x:=T) in H.
           inversion H;auto.

           assert(l=l');subst.
           apply IHl.
           unfold AP.
           extensionality T.
           simpl in H;inversion H.
           apply @equal_f_dep with (x:=T) in H1.
           inversion H1;auto.
           reflexivity.
    Qed.

    Lemma EqAtom : A , (fun T : Typeatom (A T)) = Atom (A) .
    Proof. intuition. Qed.

    Lemma EqPerp : A , (fun T : Typeperp (A T)) = Perp (A) .
    Proof. intuition. Qed.

    Lemma EqTop : (fun T : Typetop) = Top .
    Proof. intuition. Qed.

    Lemma EqBot : (fun T : Typebot) = Bot.
    Proof. intuition. Qed.

    Lemma EqOne : (fun T : Typeone) = One.
    Proof. intuition. Qed.

    Lemma EqZero : (fun T : Typezero) = Zero .
    Proof. intuition. Qed.

    Lemma EqTensor : F G, (fun T : Typetensor (F T) (G T)) = Tensor F G.
    Proof. intuition. Qed.

    Lemma EqPar : F G, (fun T : Typepar (F T) (G T)) = Par F G.
    Proof. intuition. Qed.

    Lemma EqPlus : F G, (fun T : Typeplus (F T) (G T)) = Plus F G.
    Proof. intuition. Qed.

    Lemma EqWith : F G, (fun T : TypewitH (F T) (G T)) = With F G.
    Proof. intuition. Qed.

    Lemma EqBang : F, (fun T : Typebang (F T) ) = Bang F.
    Proof. intuition. Qed.

    Lemma EqQuest : F, (fun T : Typequest (F T) ) = Quest F.
    Proof. intuition. Qed.

    Lemma EqEx : FX, (fun T : Typeex (FX T) ) = Ex FX.
    Proof. intuition. Qed.

    Lemma EqFx : FX, (fun T : Typefx (FX T) ) = Fx FX.
    Proof. intuition. Qed.

    Lemma EqAP : n l , (fun T : Typeap n (map (fun tt T) l) ) = AP n l.
    Proof. intuition. Qed.

    Lemma EqCte : t , (fun T : Typecte t ) = Cte t.
    Proof. intuition. Qed.

    Lemma EqFC1 : n t , (fun T : Typefc1 n (t T) ) = FC1 n t.
    Proof. intuition. Qed.

    Lemma EqFC2 : n t t' , (fun T : Typefc2 n (t T) (t' T)) = FC2 n t t'.
    Proof. intuition. Qed.
  End EqualityFormulas.


Inversion on Hypotheses of the shape F:Lexp = G:Lexp
  Ltac LexpSubst :=
    match goal with
    | [H : AP ?n ?l = AP ?m ?l' |- _] ⇒
      assert (l = l') by ( apply APInvL in H;auto);
      assert (n = m) by ( apply APInv in H;auto);
      subst
    | [H : Atom ?F = Atom ?F' |- _] ⇒
      assert (F = F') by ( apply AtomEq in H;auto);
      subst
    | [H : Perp ?F = Perp ?F' |- _] ⇒
      assert (F = F') by ( apply PerpEq in H;auto);
      subst
    | [H : ?F ** ?G = ?F' ** ?G' |- _] ⇒
      assert (F = F') by ( apply TensorEq1 in H;auto);
      assert (G = G') by ( apply TensorEq2 in H;auto);
      subst; clear H
    | [H : ?F ?G = ?F' ?G' |- _] ⇒
      assert (F = F') by ( apply PlusEq1 in H;auto);
      assert (G = G') by ( apply PlusEq2 in H;auto);
      subst; clear H
    | [H : ?F $ ?G = ?F' $ ?G' |- _] ⇒
      assert (F = F') by ( apply ParEq1 in H;auto);
      assert (G = G') by ( apply ParEq2 in H;auto);
      subst; clear H
    | [H : ?F & ?G = ?F' & ?G' |- _] ⇒
      assert (F = F') by ( apply WithEq1 in H;auto);
      assert (G = G') by ( apply WithEq2 in H;auto);
      subst; clear H
    | [H : F{ ?F }= F{ ?F'} |- _] ⇒
      apply FxEq in H;subst
    | [H : Fx _= _ |- _] ⇒ apply FxEq in H;subst
    | [H : _= Fx _ |- _] ⇒ apply FxEq in H;subst
    | [H : E{ ?F }= E{ ?F'} |- _] ⇒ apply ExEq in H;auto; subst
    | [H : Ex _ = _ |- _] ⇒ apply ExEq in H;auto; subst
    | [H : _ = Ex _ |- _] ⇒ apply ExEq in H;auto; subst
    | [H : ! ?F = ! ?F' |- _] ⇒
      apply BangEq in H;auto; subst
    | [H : ? ?F = ? ?F' |- _] ⇒
      apply QuestEq in H; subst
    end.


Measures (weight/complexity) of Formulas
  Section Measures.

    Fixpoint lexp_weight (P:lexp unit) : nat :=
      match P with
      | atom X | perp X ⇒ 0
      | one | bot | zero | top ⇒ 0
      | tensor X Y ⇒ 1 + (lexp_weight X) + (lexp_weight Y)
      | par X Y ⇒ 1 + (lexp_weight X) + (lexp_weight Y)
      | plus X Y ⇒ 1 + (lexp_weight X) + (lexp_weight Y)
      | witH X Y ⇒ 1 + (lexp_weight X) + (lexp_weight Y)
      | bang X ⇒ 1 + lexp_weight X
      | quest X ⇒ 1 + lexp_weight X
      | ex FX ⇒ 1 + lexp_weight (FX tt)
      | fx FX ⇒ 1 + lexp_weight (FX tt)
      end.

    Definition Lexp_weight (P : Lexp) :nat := lexp_weight (P _).

    Hint Unfold Lexp_weight Dual_LExp.

    Theorem WeightDestruct0 : F:Lexp, 0%nat = Lexp_weight F
                                             ( A, F = Atom A) ( A, F = Perp A)
                                             F = One F = Bot F = Zero F = Top.
      autounfold.
      intros.
      caseLexp F;firstorder; try(rewrite <- H2 in H; inversion H);
        try(rewrite <- H1 in H; inversion H);
        try(rewrite <- H0 in H; inversion H).
      left;eauto.
      right;left;eauto.

    Qed.

    Definition eq_wt F G:= Lexp_weight F = Lexp_weight G.

    Lemma wt_refl : F, eq_wt F F.
    Proof. unfold eq_wt; auto. Qed.

    Lemma wt_symm : F G, eq_wt F G eq_wt G F.
    Proof. unfold eq_wt; auto. Qed.

    Lemma wt_trans: F G T, eq_wt F G eq_wt G T eq_wt F T.
    Proof. unfold eq_wt; intros; rewrite H, H0; auto. Qed.

    Hint Resolve wt_refl wt_symm wt_trans.

    Add Parametric Relation : (Lexp) eq_wt
        reflexivity proved by wt_refl
        symmetry proved by wt_symm
        transitivity proved by wt_trans as wt_linear.

    Lemma wt_eq : F G, F = G Lexp_weight F = Lexp_weight G.
      intros. rewrite H. auto.
    Qed.

    Lemma lweight_dual_unit :
       FX:Subs, lexp_weight (FX unit tt) = lexp_weight (dual_LExp (FX unit tt)).
    Proof.
      intros.
      induction (FX unit tt);try(reflexivity);
        try(simpl;try(rewrite IHl);try(rewrite IHl1);try(rewrite IHl2);reflexivity);
        (simpl; generalize (H tt);intro HH; rewrite HH; reflexivity).
    Qed.

    Lemma lweight_dual : F: Lexp , Lexp_weight F = Lexp_weight (Dual_LExp F).
    Proof.
      intro.
      indLexp F;try (reflexivity);autounfold in *;
        try(simpl; try(rewrite IHHF1);try(rewrite IHHF2);auto);
        rewrite lweight_dual_unit;auto.
    Qed.

    Lemma lweight_dual_plus :
       F G, Lexp_weight F + Lexp_weight G = Lexp_weight (Dual_LExp F) + Lexp_weight (Dual_LExp G).
    Proof.
      intros.
      rewrite lweight_dual with (F:=F).
      rewrite lweight_dual with (F:=G).
      auto.
    Qed.
  End Measures.

Equality UpTo Atoms
  Section EqUpTo.
    Variable T T':Type.
    Inductive xVariantT : term T term T' Prop :=
    | xvt_var : x y, xVariantT (var x) (var y)
    | xvt_cte : c, xVariantT (cte c) (cte c)
    | xvt_fc1 : n t t', xVariantT t t' xVariantT (fc1 n t) (fc1 n t')
    | xvt_fc2 : n t1 t2 t1' t2', xVariantT t1 t1' xVariantT t2 t2' xVariantT (fc2 n t1 t2) (fc2 n t1' t2').

    Inductive xVariantLT : list (term T) list (term T') Prop :=
    | xvlt_nil : xVariantLT [] []
    | xvlt_cond : t1 t2 l1 l2, xVariantT t1 t2 xVariantLT l1 l2 xVariantLT (t1 :: l1) (t2 :: l2).

    Inductive xVariantA : aprop T aprop T' Prop :=
    | xva_ap : n l l', xVariantLT l l' xVariantA (ap n l) (ap n l').

    Inductive EqualUptoAtoms : lexp T lexp T' Prop :=
    | eq_atom : A A', xVariantA A A' EqualUptoAtoms (atom A) (atom A')
    | eq_perp : A A', xVariantA A A' EqualUptoAtoms (perp A) (perp A')
    | eq_top : EqualUptoAtoms top top
    | eq_bot : EqualUptoAtoms bot bot
    | eq_zero : EqualUptoAtoms zero zero
    | eq_one : EqualUptoAtoms one one
    | eq_tensor : F G F' G', EqualUptoAtoms F F' EqualUptoAtoms G G' EqualUptoAtoms (tensor F G) (tensor F' G')
    | eq_par : F G F' G', EqualUptoAtoms F F' EqualUptoAtoms G G' EqualUptoAtoms (par F G) (par F' G')
    | eq_plus : F G F' G', EqualUptoAtoms F F' EqualUptoAtoms G G' EqualUptoAtoms (plus F G) (plus F' G')
    | eq_with : F G F' G', EqualUptoAtoms F F' EqualUptoAtoms G G' EqualUptoAtoms (witH F G) (witH F' G')
    | eq_bang : F F', EqualUptoAtoms F F' EqualUptoAtoms (bang F) (bang F')
    | eq_quest : F F', EqualUptoAtoms F F' EqualUptoAtoms (quest F) (quest F')
    | eq_ex : FX FX' , ( t t', EqualUptoAtoms (FX t) (FX' t')) EqualUptoAtoms (ex (FX )) (ex (FX'))
    | eq_fx : FX FX' , ( t t', EqualUptoAtoms (FX t) (FX' t')) EqualUptoAtoms (fx (FX )) (fx (FX')).

    Inductive EqualUptoAtomsL : list (lexp T) list (lexp T') Prop :=
    | eq_nil : EqualUptoAtomsL nil nil
    | eq_cons : F F' L L', EqualUptoAtoms F F' EqualUptoAtomsL L L' EqualUptoAtomsL (F :: L) (F' :: L').
  End EqUpTo.

We assume that substitutions cannot do pattern-matching nor in the type T nor in the term t
  Axiom ax_subs_uptoAtoms : (T T':Type) (t:T) (t' :T') (FX:Subs), EqualUptoAtoms (FX T t) (FX T' t').
  Axiom ax_lexp_uptoAtoms : (T T':Type) (F :Lexp), EqualUptoAtoms (F T) (F T').

  Theorem subs_uptoAtomsL : (T T':Type) (t:T) (t' :T') (FX:SubsL),
      EqualUptoAtomsL (map (fun s ⇒ (s T t) ) FX) (map (fun s ⇒ (s T' t') ) FX).
    intros.
    induction FX.
    +simpl;constructor.
    +simpl.
     constructor. apply ax_subs_uptoAtoms.
     apply IHFX.
  Qed.

Basic Definition for Focusing
  Section Polarities.
    Definition asynchronousF (F :lexp unit) :=
      match F with
      | atom _ | perp _false
      | toptrue
      | bottrue
      | zerofalse
      | onefalse
      | tensor _ _false
      | par _ _true
      | plus _ _false
      | witH _ _true
      | bang _false
      | quest _true
      | ex _false
      | fx _true
      end.
    Definition AsynchronousF (F:Lexp) : bool := asynchronousF (F _).
    Hint Unfold AsynchronousF.

    Inductive Asynchronous : Lexp Prop :=
    | aTop : Asynchronous Top
    | aBot : Asynchronous Bot
    | aPar : F G, Asynchronous (Par F G)
    | aWith : F G, Asynchronous (With F G)
    | aQuest : F , Asynchronous (Quest F)
    | aForall : FX , Asynchronous (Fx FX).

    Hint Constructors Asynchronous.

    Theorem AsyncEqL : F:Lexp , Asynchronous F AsynchronousF F = true.
    Proof.
      intros.
      inversion H;try(reflexivity).
    Qed.

    Theorem AsyncEqR : F: Lexp, AsynchronousF F = true Asynchronous F.
    Proof.
      intros.
      caseLexp F;auto;
        try( rewrite <- H1 in H);
        try( rewrite <- H0 in H);
        try( rewrite <- H2 in H); inversion H.
    Qed.

    Theorem AsyncEq : F:Lexp , Asynchronous F AsynchronousF F = true.
      split. apply AsyncEqL. apply AsyncEqR.
    Qed.

    Inductive IsNegativeAtom : Lexp Prop :=
    | IsNAP : n l, true = isPositive n IsNegativeAtom (Perp (AP n l ))
    | IsNAP' : n l, false = isPositive n IsNegativeAtom (Atom (AP n l )).

    Hint Constructors IsNegativeAtom.

    Inductive IsPositiveAtom : Lexp Prop :=
    | IsPAP : n l, false = isPositive n IsPositiveAtom (Perp (AP n l ))
    | IsPAP' : n l, true = isPositive n IsPositiveAtom (Atom (AP n l )).

    Hint Constructors IsPositiveAtom.

    Fixpoint exp_weight (P:lexp unit) : nat :=
      match P with
      | atom _ | perp _ | one | bot | zero | top ⇒ 1
      | tensor X Y ⇒ 1 + (exp_weight X) + (exp_weight Y)
      | par X Y ⇒ 1 + (exp_weight X) + (exp_weight Y)
      | plus X Y ⇒ 1 + (exp_weight X) + (exp_weight Y)
      | witH X Y ⇒ 1 + (exp_weight X) + (exp_weight Y)
      | bang X ⇒ 1 + exp_weight X
      | quest X ⇒ 1 + exp_weight X
      | ex FX ⇒ 1 + exp_weight (FX tt)
      | fx FX ⇒ 1 + exp_weight (FX tt)
      end.

    Definition Exp_weight (F:Lexp) :nat := exp_weight(F _).
    Hint Unfold Exp_weight.

    Theorem exp_weight0 : F:Lexp , Exp_weight F > 0.
      intros.
      unfold Exp_weight.
      induction F;simpl;omega.
    Qed.

    Theorem exp_weight0F : F:Lexp , Exp_weight F = 0%nat False.
    Proof.
      intros.
      generalize(exp_weight0 F).
      intro.
      rewrite H in H0.
      inversion H0.
    Qed.

    Fixpoint L_weight (L: list Lexp) : nat :=
      match L with
      | nil ⇒ 0
      | H :: L'(Exp_weight H) + (L_weight L')
      end.

    Theorem exp_weight0LF : l L, 0%nat = Exp_weight l + L_weight L False.
    Proof.
      intros.
      assert(Exp_weight l > 0%nat) by (apply exp_weight0).
      omega.
    Qed.

    Theorem L_weightApp : L M, L_weight (L ++M) = L_weight L + L_weight M.
    Proof.
      intros.
      induction L; auto.
      simpl.
      rewrite IHL.
      omega.
    Qed.

    Lemma WeightLeq: w l L, S w = L_weight (l :: L) L_weight L w.
    Proof.
      intros.
      simpl in H.
      generalize (exp_weight0 l);intro.
      apply GtZero in H0.
      destruct H0.
      rewrite H0 in H.
      omega.
    Qed.

    Lemma TermFlattenG: (t:Term) (T:Type) , flattenT (t (term T)) = (t T).
      intros.
      assert(ClosedT t) by apply ax_closedT.
      induction H; try(reflexivity).
      simpl. rewrite IHClosedT. auto.
      simpl. rewrite IHClosedT1. rewrite IHClosedT2. auto.
    Qed.

    Lemma TermFlattenFun : t:Term , (fun T : TypeflattenT (t (term T))) = t.
      intros.
      extensionality T.
      rewrite TermFlattenG;auto.
    Qed.

    Lemma TermFlattenFun': t:Term ,
        (fun T:TypeflattenT (flattenT (t (term (term T))))) = t.
      intros.
      extensionality T.
      do 2 rewrite TermFlattenG;auto.
    Qed.

    Lemma FlattenAtom : T, (A : aprop (term T)), A' , flatten (atom A) = atom A'.
      intros.
      destruct A0;simpl;eauto.
    Qed.

    Lemma FlattenPerp : T, (A : aprop (term T)), A' , flatten (perp A) = perp A'.
      intros.
      destruct A0;simpl;eauto.
    Qed.

    Lemma subs_weight_weak: (FX:Subs) x, Exp_weight (Subst FX x) = exp_weight (FX unit tt) .
      intros.
      autounfold. unfold Subst.
      assert (ClosedT x) by apply ax_closedT.
      inversion H.
      + assert(EqualUptoAtoms (FX (term unit) (Cte C unit)) (FX unit tt)) by apply ax_subs_uptoAtoms.
        induction H1;simpl; try(destruct H1);auto.
      + assert(EqualUptoAtoms (FX (term unit) (FC1 n t1 unit)) (FX unit tt)) by apply ax_subs_uptoAtoms.
        induction H2;simpl; try(destruct H2);auto.
      + assert(EqualUptoAtoms (FX (term unit) (FC2 n t1 t2 unit)) (FX unit tt)) by apply ax_subs_uptoAtoms.
        induction H3;simpl; try(destruct H3);auto.
    Qed.

    Theorem subs_weight : (FX : Subs) x y, Exp_weight(Subst FX x) = Exp_weight(Subst FX y).
      intros.
      rewrite subs_weight_weak.
      rewrite subs_weight_weak.
      auto.
    Qed.

    Lemma subs_weight_weak': (FX:Subs) x, Lexp_weight (Subst FX x) = (lexp_weight (FX unit tt)) .
      intros.
      unfold Lexp_weight.
      unfold Subst.

      assert (ClosedT x) by apply ax_closedT.
      inversion H.
      + assert(EqualUptoAtoms (FX (term unit) (Cte C unit)) (FX unit tt)) by apply ax_subs_uptoAtoms.
        induction H1;simpl ; try(destruct H1); unfold Lexp_weight; auto.
      + assert(EqualUptoAtoms (FX (term unit) (FC1 n t1 unit)) (FX unit tt)) by apply ax_subs_uptoAtoms.
        induction H2;simpl; try(destruct H2);auto.
      + assert(EqualUptoAtoms (FX (term unit) (FC2 n t1 t2 unit)) (FX unit tt)) by apply ax_subs_uptoAtoms.
        induction H3;simpl; try(destruct H3);auto.
    Qed.

    Theorem subs_weight' : (FX : Subs) x y, Lexp_weight(Subst FX x) = Lexp_weight(Subst FX y).
      intros.
      rewrite subs_weight_weak'.
      rewrite subs_weight_weak'.
      auto.
    Qed.

    Lemma Flatten_dual : T (F: lexp (term T)), flatten F = dual_LExp(flatten ( dual_LExp F)).
      intros.
      induction F;simpl;try(destruct a);try(reflexivity);
        try(simpl;rewrite IHF1;rewrite IHF2; intuition);
        try(simpl;rewrite IHF; intuition).

      assert(Hs : (fun x : Tflatten (f (var x))) = (fun x : Tdual_LExp (flatten (dual_LExp (f (var x))))))
        by (extensionality x; generalize(H (var x));auto);rewrite Hs; reflexivity.
      assert(Hs : (fun x : Tflatten (f (var x))) = (fun x : Tdual_LExp (flatten (dual_LExp (f (var x))))))
        by (extensionality x; generalize(H (var x));auto);rewrite Hs; reflexivity.
    Qed.

    Theorem SubsDual: (FX1 FX2 : Subs) t, (E{ FX1} = F{ FX2} (Subst FX1 t) = (Subst FX2 t.
      intros.
      unfold Dual_LExp in ×.
      simpl in ×.
      change ( (fun T : Typefx (fun x : Tdual_LExp (FX1 T x))))
        with (F{ fun _ xdual_LExp(FX1 _ x)}) in H.
      LexpSubst.
      unfold Subst.
      extensionality T.
      eapply Flatten_dual.
    Qed.

    Theorem SubsDual': (FX1 FX2 : Subs) t, (F{ FX1} = E{ FX2} (Subst FX1 t) = (Subst FX2 t.
      intros.
      unfold Dual_LExp in ×.
      simpl in ×.
      change ( (fun T : Typeex (fun x : Tdual_LExp (FX1 T x))))
        with (E{ fun _ xdual_LExp(FX1 _ x)}) in H.
      LexpSubst.
      unfold Subst.
      extensionality T.
      eapply Flatten_dual.
    Qed.

    Theorem WeightEF (FX1 FX2 : Subs) w t :
      S w = Lexp_weight (E{ FX1})
      (E{ FX1} = F{ FX2} Lexp_weight (Subst FX2 t) w.
    Proof.
      intros Hw Eq.
      assert (Lexp_weight (E{ FX1} = Lexp_weight (F{ FX2})) by
          solve [rewrite Eq; auto].
      inversion H. inversion Hw.
      rewrite subs_weight_weak'.
      rewrite <- H1. rewrite lweight_dual_unit. auto.
    Qed.

    Theorem WeightFE (FX1 FX2 : Subs) w t :
      S w = Lexp_weight (F{ FX1})
      (F{ FX1} = E{ FX2} Lexp_weight (Subst FX2 t) w.
    Proof.
      intros Hw Eq.
      assert (Lexp_weight (F{ FX1} = Lexp_weight (E{ FX2})) by
          solve [rewrite Eq; auto].
      inversion H. inversion Hw.
      rewrite subs_weight_weak'.
      rewrite <- H1. rewrite lweight_dual_unit. auto.
    Qed.

    Fixpoint LexpPos (l: list Lexp) : Prop :=
      match l with
      | nilTrue
      | H :: T'(AsynchronousF H = false) LexpPos T'
      end.

    Fixpoint BlexpPos (l: list Lexp) : bool :=
      match l with
      | niltrue
      | H :: Tandb (negb (AsynchronousF H)) ( BlexpPos T)
      end.

    Theorem PosBool : l, BlexpPos l = true LexpPos l.
    Proof.
      intros.
      split;induction l;simpl;auto.
      - intro;firstorder.

        rewrite andb_true_iff in H.
        destruct H;auto.
        rewrite negb_true_iff in H.
        auto.
        rewrite andb_true_iff in H.
        destruct H.
        auto.
      - intro.
        destruct H.
        apply IHl in H0.
        rewrite H;auto.
    Qed.

    Inductive LexpPos' : list Lexp Prop :=
    | l_nil : LexpPos' []
    | l_sin : a, (AsynchronousF a = false) LexpPos' [a]
    | l_cos : a l, LexpPos' [a] LexpPos' l LexpPos' (a::l).

    Hint Resolve l_nil l_sin l_cos.

    Lemma lexpPosUnion a L: LexpPos [a] LexpPos L LexpPos ([a] ++ L).
    Proof.
      intros.
      simpl; firstorder.
    Qed.

    Lemma lexpPosUnion_inv a L: LexpPos ([a] ++ L) LexpPos [a] LexpPos L.
    Proof.
      intros.
      simpl in H.
      split; firstorder.
    Qed.

    Lemma lexpPos_lexpPos' M: LexpPos' M LexpPos M.
    Proof.
      split; intros.
      × induction H;
          try solve [simpl; auto].
        apply lexpPosUnion; auto.
      × induction M; intros; auto.
        apply lexpPosUnion_inv in H.
        destruct H.
        apply l_cos; auto.
        apply l_sin; firstorder.
    Qed.

    Lemma AsynchronousFlexpPos : l, AsynchronousF l = false LexpPos [l].
    Proof.
      firstorder.
    Qed.

    Lemma NegPosAtom : F, IsNegativeAtom F IsPositiveAtom F° .
      intros.
      inversion H;try(constructor);auto.
    Qed.

    Inductive release : lexp unit Prop :=
    | RelNA1 : n l, false = isPositive n release (perp (ap n l))
    | RelNA1' : n l, true = isPositive n release (atom (ap n l))
    | RelTop : release top
    | RelBot : release bot
    | RelPar : F G, release (par F G)
    | RelWith : F G, release (witH F G)
    | RelQuest : F, release (quest F)
    | RelForall : FX, release (fx FX).

    Definition Release (F:Lexp) := release (F _).
    Hint Unfold Release.
    Hint Constructors release.

    Lemma IsPositiveAtomRelease: F, IsPositiveAtom F Release F.
      intros.
      inversion H;
        constructor;auto.
    Qed.

    Inductive NotAsynchronous : Lexp Prop :=
    | NAAtomP : v, NotAsynchronous (Atom v)
    | NAAtomN : v, NotAsynchronous (Perp v)
    | NAZero : NotAsynchronous Zero
    | NAOne : NotAsynchronous One
    | NATensor : F G, NotAsynchronous ( F ** G)
    | NAPlus : F G, NotAsynchronous ( Plus F G)
    | NABang : F, NotAsynchronous ( ! F )
    | NAExists : FX, NotAsynchronous ( Ex FX ).
    Hint Constructors NotAsynchronous.

    Theorem AsynchronousEquiv : F, NotAsynchronous F ¬ Asynchronous F.
    Proof.
      intros.
      split;intro.
      + inversion H;intro Hc;inversion Hc; apply @equal_f_dep with (x:=unit) in H2; inversion H2.
      + indLexp F;try(constructor);
          match goal with [H : ¬Asynchronous ?F |- _]
                          ⇒ assert(Asynchronous F) by auto; contradiction end.
    Qed.

    Theorem AsyncEqNeg : F:Lexp , ¬ Asynchronous F AsynchronousF F = false.
      split;intro H.
      + rewrite <- AsynchronousEquiv in H.
        inversion H;reflexivity.
      + intro HN.
        apply AsyncEqL in HN.
        rewrite H in HN.
        intuition.
    Qed.

    Inductive posOrNegAtom : lexp unit Prop :=
    | PPAtom1 : n l, false = isPositive n posOrNegAtom (atom (ap n l))
    | PPAtom1' : n l, true = isPositive n posOrNegAtom (perp (ap n l))
    | PPZero : posOrNegAtom zero
    | PPOne : posOrNegAtom one
    | PPTensor : F G, posOrNegAtom ( tensor F G)
    | PPPlus : F G, posOrNegAtom ( plus F G)
    | PPBang : F, posOrNegAtom ( bang F )
    | PPExists : FX, posOrNegAtom ( ex FX).
    Hint Constructors posOrNegAtom.
    Definition PosOrNegAtom (F:Lexp) := posOrNegAtom (F _).
    Hint Unfold PosOrNegAtom.

    Inductive posFormula : lexp unit Prop :=
    | PFZero : posFormula zero
    | PFOne : posFormula one
    | PFTensor : F G, posFormula ( tensor F G)
    | PFPlus : F G, posFormula ( plus F G)
    | PFBang : F, posFormula ( bang F )
    | PFExists : FX, posFormula ( ex FX).
    Hint Constructors posFormula.
    Definition PosFormula (F:Lexp) := posFormula (F _).
    Hint Unfold PosFormula.

    Lemma PosFormulaPosOrNegAtom : F, PosFormula F PosOrNegAtom F.
      intros.
      unfold PosOrNegAtom.
      inversion H;constructor.
    Qed.

    Lemma ApropPosNegAtom : A: AProp, IsPositiveAtom (Atom A) IsNegativeAtom(Atom A).
      intros.
      assert(HC : ClosedA A0) by apply ax_closedA.
      inversion HC;remember(isPositive n); destruct b;intuition.
    Qed.

    Lemma ApropPosNegAtom' : A: AProp, IsPositiveAtom (Perp A) IsNegativeAtom(Perp A).
      intros.
      assert(HC : ClosedA A0) by apply ax_closedA.
      inversion HC;remember(isPositive n); destruct b;intuition.
    Qed.

    Lemma NotAsynchronousPosAtoms : F, ¬ Asynchronous F PosFormula F IsPositiveAtom F IsNegativeAtom F.
      intros.
      caseLexp F;intuition;try (left;constructor);
        [idtac | idtac | (contradict H;subst;auto) .. ].
      generalize( ApropPosNegAtom A0); intro HA3;destruct HA3;intuition.
      generalize( ApropPosNegAtom' A0); intro HA3;destruct HA3;intuition.
    Qed.

    Lemma NegPosAtomContradiction: F, PosOrNegAtom F IsPositiveAtom F False.
      intros.
      inversion H0;
        rewrite <- H2 in H;
        inversion H;
        rewrite <- H4 in H1;
        intuition.
    Qed.

    Lemma IsNegativePosOrNegAtom : F, IsNegativeAtom F PosOrNegAtom F.
    Proof.
      intros.
      inversion H;constructor;auto.
    Qed.

    Lemma PosOrNegAtomAsync : F, PosOrNegAtom F AsynchronousF F = false.
    Proof.
      intros.
      inversion H;autounfold in *;
        try(rewrite <- H0) ; try(rewrite <- H1) ;simpl;auto.
    Qed.

    Lemma NotAsyncAtom : A, ¬ Asynchronous (A ).
      intros A3 Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotAsyncAtom' : A, ¬ Asynchronous (A ).
      intros A3 Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotAsyncOne : ¬ Asynchronous (One).
      intro Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotAsyncZero : ¬ Asynchronous (Zero).
      intro Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotAsyncTensor : F G, ¬ Asynchronous (Tensor F G).
      intros F G Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotAsyncPlus : F G, ¬ Asynchronous (Plus F G).
      intros F G Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotAsyncBang : F , ¬ Asynchronous (Bang F).
      intros F Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotAsyncEx : FX , ¬ Asynchronous (Ex FX).
      intros FX Hn.
      inversion Hn;auto;LexpContr.
    Qed.

    Lemma NotPATop : ¬IsPositiveAtom (Top).
      intros Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPABot : ¬IsPositiveAtom (Bot).
      intros Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAOne : ¬IsPositiveAtom (One).
      intros Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAZero : ¬IsPositiveAtom (Zero).
      intros Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPATensor : F G, ¬IsPositiveAtom (Tensor F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAPar : F G, ¬IsPositiveAtom (Par F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAPlus : F G, ¬IsPositiveAtom (Plus F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAWith : F G, ¬IsPositiveAtom (With F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPABang : F , ¬IsPositiveAtom (Bang F).
      intros F Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAQuest : F , ¬IsPositiveAtom (Quest F).
      intros F Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAExists : FX, ¬IsPositiveAtom (Ex FX).
      intros FX Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma NotPAForall : FX, ¬IsPositiveAtom (Fx FX).
      intros FX Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeOne : ¬ IsNegativeAtom One.
      intro Hn;inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeBot : ¬ IsNegativeAtom Bot.
      intro Hn;inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeZero : ¬ IsNegativeAtom Zero.
      intro Hn;inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeTop : ¬ IsNegativeAtom Top.
      intro Hn;inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeTensor : F G, ¬ IsNegativeAtom (Tensor F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativePar : F G, ¬ IsNegativeAtom (Par F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeWith : F G, ¬ IsNegativeAtom (With F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativePlus : F G, ¬ IsNegativeAtom (Plus F G).
      intros F G Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeBang : F, ¬ IsNegativeAtom (! F).
      intros F Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeQuest : F, ¬ IsNegativeAtom (? F).
      intros F Hn.
      inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeEx : F, ¬ IsNegativeAtom (Ex F).
      intros F Hn;inversion Hn;LexpContr.
    Qed.

    Lemma IsNegativeFx : F, ¬ IsNegativeAtom (Fx F).
      intros F Hn;inversion Hn;LexpContr.
    Qed.

    Lemma NotRelTensor: F G, ¬ Release (F ** G).
      intros F G Hn; inversion Hn.
    Qed.

    Lemma NotRelPlus: F G, ¬ Release (F G).
      intros F G Hn; inversion Hn.
    Qed.
    Lemma NotRelBang: F , ¬ Release (! F).
      intros F Hn; inversion Hn.
    Qed.

    Lemma NotRelEx: F, ¬ Release ( Ex F).
      intros F Hn; inversion Hn.
    Qed.

    Lemma NotRelOne: ¬ Release One.
      intros Hn; inversion Hn.
    Qed.

    Lemma NotRelZero: ¬ Release Zero.
      intros Hn; inversion Hn.
    Qed.

    Hint Resolve NotRelTensor NotRelPlus NotRelBang NotRelEx NotRelOne NotRelZero NotAsyncAtom NotAsyncAtom'.

    Lemma IsPositiveAtomNotAssync : F, IsPositiveAtom F ¬ Asynchronous F.
    Proof.
      intros.
      inversion H;auto.
    Qed.

    Lemma NotAsynchronousPosAtoms' : G, ¬Asynchronous G IsPositiveAtom G (PosFormula G IsNegativeAtom G).
      intros G HG.
      apply NotAsynchronousPosAtoms in HG;tauto.
    Qed.

    Lemma PosFNegAtomPorOrNegAtom: G, PosFormula G IsNegativeAtom G PosOrNegAtom G.
    Proof.
      intros.
      destruct H.
      inversion H; unfold PosOrNegAtom; rewrite <- H1; auto.
      inversion H; unfold PosOrNegAtom;constructor;auto.
    Qed.

    Lemma AsyncRelease: F, Asynchronous F Release F.
    Proof.
      intros.
      inversion H; constructor.
    Qed.

    Lemma AsIsPosRelease: F, (Asynchronous F IsPositiveAtom F ) Release F.
    Proof.
      intros.
      destruct H;auto using AsyncRelease.
      inversion H;constructor;auto.
    Qed.

    Lemma PositiveNegativeAtom : At, IsPositiveAtom (At ) IsNegativeAtom (At ).
    Proof.
      intros.
      inversion H; try(LexpSubst);try(LexpContr);try(constructor);auto.
    Qed.

    Lemma PositiveNegativeAtomNeg : At, IsPositiveAtom (At ) ¬ IsPositiveAtom (At ).
    Proof.
      intros.
      inversion H;intro; try(LexpSubst);
        apply PositiveNegativeAtom in H;
        apply IsNegativePosOrNegAtom in H;
        eapply NegPosAtomContradiction;eauto.
    Qed.


    Lemma NegativePositiveAtomNeg : At, IsNegativeAtom (At ) ¬ IsPositiveAtom (At ).
    Proof.
      intros.
      inversion H;intro; try(LexpSubst);try(LexpContr);try(constructor);auto;
        apply PositiveNegativeAtom in H2;
        apply IsNegativePosOrNegAtom in H2;
        eapply NegPosAtomContradiction;eauto.
    Qed.

    Lemma PositiveNegative : A, IsPositiveAtom A ¬ IsNegativeAtom A.
    Proof.
      intros.
      inversion H;intro; try(do 2 LexpSubst);try(constructor);auto;
        inversion H2;try(LexpContr);
          try(do 2 LexpSubst); try( rewrite <- H4 in H0); intuition.
    Qed.

    Lemma PosFIsNegAAsync : G, PosFormula G IsNegativeAtom G ¬ Asynchronous G.
    Proof.
      intros.
      destruct H.
      caseLexp G ;try(do 2 LexpSubst);try(constructor);auto; try( rewrite <- H0 in H; inversion H);
        try( rewrite <- H2 in H; inversion H);
        try( rewrite <- H1 in H; inversion H);
        inversion H;intro HA; inversion HA ;LexpContr.
      inversion H;intro HA; inversion HA ;LexpContr.
    Qed.

  End Polarities.

This tactic solves goals when there is a hypothesis IsNegativeAtom(F) and F cannot be a negative atom
  Ltac invNegAtom :=
    try(
        match goal with
        | [H: IsNegativeAtom ?F |- _] ⇒ assert(¬ IsNegativeAtom F)
            by (try(apply IsNegativeOne) ;
                try(apply IsNegativeBot) ;
                try(apply IsNegativeTop) ;
                try(apply IsNegativeZero) ;
                try(apply IsNegativeTensor) ;
                try(apply IsNegativePlus) ;
                try(apply IsNegativeWith) ;
                try(apply IsNegativePar) ;
                try(apply IsNegativeBang) ;
                try(apply IsNegativeQuest) ;
                try(apply IsNegativeEx);
                try(apply IsNegativeFx)
               ) ; contradiction
                     
        end
      ).

This tactic solves goals when there is a hipthesis Release(F) and F cannot be released.
  Ltac invRel :=
    try(
        match goal with
        | [H: Release ?F |- _] ⇒ assert(¬ Release F)
            by (
                try(apply NotRelTensor);
                try(apply NotRelPlus);
                try(apply NotRelBang);
                try(apply NotRelEx);
                try(apply NotRelOne);
                try(apply NotRelZero)
              );contradiction
        end).

  Ltac invPosOrNegAtom :=
    try(match goal with
          [H: PosOrNegAtom ?F |- _ ] ⇒
          match F with
          | Topinversion H
          | Oneinversion H
          | Botinversion H
          | Zeroinversion H
          | Tensor _ _inversion H
          | Par _ _inversion H
          | With _ _inversion H
          | Plus _ _inversion H
          | Quest _inversion H
          | Bang _inversion H
          | Ex _inversion H
          | Fx _inversion H
          end
        end).

Simplification of hypotheses with flattenT predicates
  Ltac simplifyH H :=
    unfold Subst in H;
    simpl in H;
    repeat
      match goal with
      | [H : context[fun _ : TypeflattenT( _ (term _))] |- _] ⇒ rewrite TermFlattenFun in H
      | [H : context[fun _ : TypeflattenT(flattenT ( _ (term _ ) ))] |- _] ⇒ rewrite TermFlattenFun' in H
      | [H : context[fun _ : Typeap _ _ ] |- _ ] ⇒ rewrite EqAP in H
      | [H : context[fun _ : Typecte _] |- _ ] ⇒ rewrite EqCte in H
      | [H : context[fun _ : Typefc1 _ _] |- _ ] ⇒ rewrite EqFC1 in H
      | [H : context[fun _ : Typefc2 _ _ _] |- _ ] ⇒ rewrite EqFC2 in H
      | [H : context[fun _ : Typeatom _] |- _ ] ⇒ rewrite EqAtom in H
      | [H : context[fun _ : Typeperp _] |- _ ] ⇒ rewrite EqPerp in H
      | [H : context[fun _ : Typetensor _ _] |- _ ] ⇒ rewrite EqTensor in H
      | [H : context[fun _ : Typepar _ _] |- _ ] ⇒ rewrite EqPar in H
      | [H : context[fun _ : TypewitH _ _] |- _ ] ⇒ rewrite EqWith in H
      | [H : context[fun _ : Typeplus _ _] |- _ ] ⇒ rewrite EqPlus in H
      | [H : context[fun _ : Typequest _] |- _ ] ⇒ rewrite EqQuest in H
      | [H : context[fun _ : Typebang _] |- _ ] ⇒ rewrite EqBang in H
      | [H : context[fun _ : Typeex _] |- _ ] ⇒ rewrite EqEx in H
      | [H : context[fun _ : Typefx _] |- _ ] ⇒ rewrite EqFx in H
      end.

Simplification of the goal with flattenT predicates
  Ltac simplifyG :=
    unfold Subst;
    simpl;
    repeat
      match goal with
      | [ |- context[fun _ : TypeflattenT( _ (term _))]] ⇒ rewrite TermFlattenFun
      | [ |- context[fun _ : TypeflattenT(flattenT ( _ (term _ ) ))]] ⇒ rewrite TermFlattenFun'
      | [ |- context[fun _ : Typeap _ _ ] ] ⇒ rewrite EqAP
      | [ |- context[fun _ : Typecte _]] ⇒ rewrite EqCte
      | [ |- context[fun _ : Typefc1 _ _]] ⇒ rewrite EqFC1
      | [ |- context[fun _ : Typefc2 _ _ _] ] ⇒ rewrite EqFC2
      | [ |- context[fun _ : Typeatom _]] ⇒ rewrite EqAtom
      | [ |- context[fun _ : Typeperp _]] ⇒ rewrite EqPerp
      | [ |- context[fun _ : Typetensor _ _]] ⇒ rewrite EqTensor
      | [ |- context[fun _ : Typepar _ _] ] ⇒ rewrite EqPar
      | [ |- context[fun _ : TypewitH _ _]] ⇒ rewrite EqWith
      | [ |- context[fun _ : Typeplus _ _]] ⇒ rewrite EqPlus
      | [ |- context[fun _ : Typequest _]] ⇒ rewrite EqQuest
      | [ |- context[fun _ : Typebang _]] ⇒ rewrite EqBang
      | [ |- context[fun _ : Typeex _] ] ⇒ rewrite EqEx
      | [ |- context[fun _ : Typefx _]] ⇒ rewrite EqFx
      end.
End Syntax_LL.

Module to be imported for LL Formulas
Module FormulasLL (DT : Eqset_dec_pol).
  Module Export Sy := Syntax_LL DT.

  Module lexp_eq <: Eqset_dec.
    Definition A := Lexp.
    Definition eqA_dec := FEqDec.
  End lexp_eq.

  Hint Rewrite Neg2pos Ng_involutive.
  Hint Resolve wt_refl wt_symm wt_trans.
  Hint Constructors Asynchronous.
  Hint Resolve l_nil l_sin l_cos.
  Hint Constructors release.
  Hint Constructors NotAsynchronous.
  Hint Constructors posOrNegAtom.

  Declare Module Export MSetList : MultisetList lexp_eq.

  Lemma LPos1 (L M :list Lexp) : L =mul= M LexpPos L LexpPos M.
  Proof.
    intros P H.
    apply lexpPos_lexpPos'.
    apply lexpPos_lexpPos' in H.
    apply Permutation_meq in P.
    induction P; subst.
    × apply l_nil.
    × inversion H; subst.
      apply l_cos; auto.
      apply l_cos; auto.
    × inversion_clear H.
      inversion_clear H1.
      apply l_cos; auto.
      apply l_cos; auto.
    × apply IHP2.
      apply IHP1;auto.
  Qed.

  Instance lexpPos_morph : Proper (meq ==> iff) (LexpPos ).
  Proof.
    intros L M Heq .
    split;intro.
    + eapply LPos1;eauto.
    + apply LPos1 with (L:=M);auto.
  Qed.

  Lemma LPos2 : M N L, L =mul= M ++ N LexpPos L LexpPos M.
  Proof.
    induction M;intros;simpl;auto.
    assert (L =mul= M ++ (a::N)) by solve[rewrite H; solve_permutation].
    apply IHM in H1;auto.
    firstorder.
    apply LPos1 in H;auto.
    inversion H;auto.
  Qed.

  Lemma LPos3: M N L, L =mul= M ++ N LexpPos L LexpPos N .
  Proof.
    intros.
    rewrite union_comm in H.
    eapply LPos2 ;eassumption.
  Qed.

  Lemma LexpPosConc : M F, LexpPos M ¬ Asynchronous F LexpPos (M ++ [F]).
    intros.
    assert(M ++ [F] =mul= [F] ++ M) by solve_permutation.
    rewrite H1.
    constructor;auto.
    apply AsyncEqNeg;auto.
  Qed.

  Lemma LexpPosCons : F L, LexpPos (F :: L) LexpPos L.
    intros.
    inversion H.
    auto.
  Qed.

  Lemma LexpPosOrNegAtomConc : M F, LexpPos M PosOrNegAtom F LexpPos (M ++ [F]).
    intros.
    assert(HS : M ++ [F] =mul= [F] ++ M) by solve_permutation.
    rewrite HS.
    constructor;auto using PosOrNegAtomAsync.
  Qed.
End FormulasLL.