Library BioFLL.LL.SequentCalculiBasicTheory

Basic proof theory

This file proves some structural properties of the triadic system. In particular, we prove that the exchange rule is admissible and then, it is possible to replace equivalent multisets (meq).

Module SqBasic (DT : Eqset_dec_pol).
  Module Export Sys := SqSystems DT.
  Hint Resolve Max.le_max_r.
  Hint Resolve Max.le_max_l.

Proofs with measures match proof without measures.

  Theorem AdequacyTri1 : ∀ n B M X, n |-F - B ; M ; X → |-F - B ; M ; X.
    induction n using strongind;intros.
    + inversion H;subst;eauto.
    + inversion H0;subst.
      eapply tri_init1;eauto.
      eapply tri_init2;eauto.
      eapply tri_one;eauto.
      eapply tri_tensor;eauto.
      eapply tri_plus1;eauto.
      eapply tri_plus2;eauto.
      eapply tri_bang;eauto.
      eapply tri_rel;eauto.
      eapply tri_top;eauto.
      eapply tri_bot;eauto.
      eapply tri_par;eauto.
      eapply tri_with;eauto.
      eapply tri_quest;eauto.
      eapply tri_store;eauto.
      eapply tri_dec1;eauto.
      eapply tri_dec2;eauto.
      eapply tri_ex;eauto.
      eapply tri_fx;eauto.
  Qed.

If the sequent S can be proved with a height n, then it can be proved for any m ≥ n

  Theorem Height_leq : ∀ B M X n m, n |-F - B ; M ; X → m ≥ n → m |-F - B ; M ; X.
    intros.
    generalize dependent m.
    induction H;subst;intros;
      try match goal with
            [H : ?m ≥ S ?n |- _] ⇒
            destruct m; [inversion H | auto]; assert (m≥n) by omega
          end.

    + eapply trih_init1;eauto.
    + eapply trih_init2;eauto.
    + eapply trih_one;eauto.
    + apply IHTriSystemh1 in H3 as HT1.
      apply IHTriSystemh2 in H3 as HT2.
      eapply trih_tensor;eauto.
    + apply IHTriSystemh in H1 as HT1.
      eapply trih_plus1;eauto.
    + apply IHTriSystemh in H1 as HT1.
      eapply trih_plus2;eauto.
    + eapply trih_bang;eauto.
    + apply IHTriSystemh in H2 as HT1.
      eapply trih_rel;eauto.
    + eapply trih_top.
    + apply IHTriSystemh in H1 as HT1.
      eapply trih_bot;eauto.
    + apply IHTriSystemh in H1 as HT1.
      eapply trih_par;eauto.
    + apply IHTriSystemh1 in H2 as HT1.
      apply IHTriSystemh2 in H2 as HT2.
      eapply trih_with;eauto.
    + apply IHTriSystemh in H1 as HT1.
      eapply trih_quest;eauto.
    + apply IHTriSystemh in H2 as HT1.
      eapply trih_store;eauto.
    + apply IHTriSystemh in H3 as HT1.
      eapply trih_dec1;eauto.
    + apply IHTriSystemh in H3 as HT1.
      eapply trih_dec2;eauto.
    + apply IHTriSystemh in H1 as HT1.
      eapply trih_ex;eauto.
    + eapply trih_fx;intro x.
      generalize (H x);intro Hx.
      eapply H0 in H2;eauto.
  Qed.

The B and M contexts can be substituted by equivalent multisets

  Theorem TriExchangeh :
    ∀ B B' M M' X n,
      n |-F - B ; M ; X → B =mul = B' → M =mul = M' → n |-F - B' ; M' ; X.
  Proof.
    intros.
    generalize dependent B.
    generalize dependent M.
    generalize dependent B'.
    generalize dependent M'.
    generalize dependent X.
    induction n using strongind;intros.
    + inversion H;subst.
      ++ apply MulSingleton in H1;subst.
         eapply trih_init1;auto.
      ++ apply meq_sym in H1.
         apply multiset_meq_empty in H1;subst.
         eapply trih_init2;eauto.
      ++ apply meq_sym in H1.
         apply multiset_meq_empty in H1;subst.
         eapply trih_one.
      ++ eapply trih_top.
    + inversion H0;subst;auto.
       ++ apply MulSingleton in H1;subst;auto.
       ++ apply meq_sym in H1.
          apply multiset_meq_empty in H1;subst;eauto.
       ++ apply meq_sym in H1.
          apply multiset_meq_empty in H1;subst;eauto.
       ++ apply H with (M':=N) (B':= B') in H5;auto.
          apply H with (M':=M0) (B':= B') in H6;eauto.
       ++ eapply H with (M':=M') (B':=B')in H4;auto.
       ++ eapply H with (M':=M') (B':=B')in H4;auto.
       ++ apply meq_sym in H1.
          apply multiset_meq_empty in H1;subst.
          eapply trih_bang.
          eapply H with (B:=B)(M:=[]) ;auto.
       ++ eapply trih_rel;eauto.
       ++ eapply trih_bot ;eauto.
       ++ eapply trih_par;eauto.
       ++ eapply trih_with;eauto.
       ++ eapply trih_quest;eauto.
       ++ eapply trih_store;eauto.
       ++ eapply trih_dec1;eauto.
       ++ eapply trih_dec2;eauto.
       ++ eapply H with (M':= M' ) (B':=B')in H4;eauto.
       ++ eapply trih_fx;auto ;intro.
          generalize (H4 x);intros.
          eapply H with (M':= M' ) (B':=B')in H3;auto.
  Qed.

Equivalent multisets can be replaced at will in the unbounded and in the linear context

  Generalizable All Variables.
  Instance trih_morphh : Proper (meq ==> meq ==> eq ==> iff) (TriSystemh n).
  Proof.
    intros n A B Hab C D Hcd X Y Hxy; subst.
    split;intro.
    + apply TriExchangeh with (B:=A) (M:=C);auto.
    + apply TriExchangeh with (B:=B) (M:=D);auto.
  Qed.
  Instance trih_morph' :
    Proper (meq ==> meq ==> @eq Arrow ==> iff) (TriSystemh n).
  Proof.
    intros n A B Hab C D Hcd X Y Hxy; subst.
    split;intro.
    + apply TriExchangeh with (B:=A) (M:=C);auto.
    + apply TriExchangeh with (B:=B) (M:=D);auto.
  Qed.

  Theorem TriExchange : ∀ B B' M M' X,
      |-F - B ; M ; X → B =mul = B' → M =mul = M' → |-F - B' ; M' ; X.
    intros.
    generalize dependent B'.
    generalize dependent M'.
    induction H;intros.
    + apply MulSingleton in H1;subst;auto.
    + apply meq_sym in H1.
      apply multiset_meq_empty in H1;subst.
      eapply tri_init2;eauto.
    + apply meq_sym in H1.
      apply multiset_meq_empty in H1;subst.
      eapply tri_one.
    + rewrite H2 in H.
      eapply tri_tensor with (N:=N) (M:=M);auto.
    + eapply tri_plus1;eauto.
    + eapply tri_plus2;eauto.
    + apply meq_sym in H1.
      apply multiset_meq_empty in H1;subst.
      eapply tri_bang;auto.
    + eapply tri_rel;auto.
    + eapply tri_top.
    + eapply tri_bot;auto.
    + eapply tri_par;auto.
    + eapply tri_with;auto.
    + eapply tri_quest;auto.
    + eapply tri_store;auto.
    + eapply tri_dec1;eauto.
    + eapply tri_dec2;eauto.
    + eapply tri_ex;eauto.
    + eapply tri_fx;eauto.
  Qed.

  Instance tri_morph : Proper (meq ==> meq ==> eq ==> iff) (TriSystem).
  Proof.
    intros A B Hab C D Hcd X Y Hxy; subst.
    split;intro.
    + apply TriExchange with (B:=A) (M:=C);auto.
    + apply TriExchange with (B:=B) (M:=D);auto.
  Qed.

  Instance tri_morph' : Proper (meq ==> meq ==> @eq Arrow ==> iff) (TriSystem).
  Proof.
    intros A B Hab C D Hcd X Y Hxy; subst.
    split;intro.
    + apply TriExchange with (B:=A) (M:=C);auto.
    + apply TriExchange with (B:=B) (M:=D);auto.
  Qed.

  Ltac inversionF H := inversion H;subst; LexpContr; try(LexpSubst);auto;invPosOrNegAtom;
                       try(match goal with [H : ¬ Asynchronous ?F |- _] ⇒ assert(Asynchronous F) by auto;contradiction
                           end).

Admissible (alternative) initial rules

  Lemma Init1: ∀ B n l,
      true = isPositive n →
      |-F - B ; [fun T : Type ⇒ atom (ap n (map (fun x ⇒ x T) l))];
        DW (fun T : Type ⇒ perp (ap n (map (fun x ⇒ x T) l))).
  Proof.
    intros.
    assert((fun T : Type ⇒ perp (ap n (map (fun x ⇒ x T) l)))° = (fun T : Type ⇒ atom (ap n (map (fun x ⇒ x T) l)))) by auto.
    rewrite <- H0.
    apply tri_init1. constructor;auto.
  Qed.

  Lemma Init2: ∀ B n l,
      true = isPositive n →
      |-F - B ++ [fun T : Type ⇒ atom (ap n (map (fun x ⇒ x T) l))]; [];
        DW (fun T : Type ⇒ perp (ap n (map (fun x ⇒ x T) l))).
  Proof.
    intros.
    assert((fun T : Type ⇒ perp (ap n (map (fun x ⇒ x T) l)))° = (fun T : Type ⇒ atom (ap n (map (fun x ⇒ x T) l)))) by auto.
    rewrite <- H0.
    eapply tri_init2;auto. constructor;auto.
  Qed.

  Lemma InitAtom : ∀ At B , IsPositiveAtom (At ⁺) → |-F - B ; [At ⁺]; DW (At ⁻).
  Proof.
    intros.
    assert((At ⁻) ° = At ⁺) by reflexivity.
    rewrite <- H0.
    apply tri_init1.
    apply PositiveNegativeAtom;auto.
  Qed.

  Lemma InitAtom' : ∀ At B , IsNegativeAtom (At ⁺) → |-F - B ; [At ⁻]; DW (At ⁺).
  Proof.
    intros.
    assert((At ⁺) ° = At⁻ ) by reflexivity.
    rewrite <- H0.
    apply tri_init1;auto.
  Qed.

  Lemma TopDown : ∀ M B, |-F - B ; M ; DW (Top).
    intros.
    apply tri_rel. constructor.
    apply tri_top.
  Qed.

End SqBasic.