Library BioFLL.Utils

General description

This file provides some auxiliary results

Checking whether a formula belongs to the unbounded context

Lemma InMeq : ∀ Gamma F, In F Gamma → ∃ Gamma', Gamma =mul = F ::Gamma'.
Proof.
  intros.
  induction Gamma;inversion H;subst.
  eauto.
  apply IHGamma in H0 as Hi.
  destruct Hi as [L].
  ∃ (a::L).
  eauto.
Qed.

A more practical way of using the rule tri_dec2 (decision on the unbounded context )

Lemma tri_dec2A : ∀ Gamma Delta F,
    |-F - Gamma ; Delta ; DW (F) →
    In F Gamma →
    ¬IsPositiveAtom F →
    |-F - Gamma ; Delta ; UP [].
  intros.
  apply InMeq in H0 as Hi.
  destruct Hi as [Gamma'].
  eapply tri_dec2 with (F:=F);auto.
Qed.

Solves goals of the form In F Theory

Ltac SolveInTheory :=
  simpl;
  repeat match goal with
         | [|- ?F = ?F ∨ ?G] ⇒ left;auto
         | _ ⇒ right
         end.

Focus on one of the rules in the unbounded context. Only the ramining (focused) proof is left as goal

Ltac tri_decide2_auto Fr :=
eapply tri_dec2A with (F:= Fr);[auto | SolveInTheory | apply NotPAExists].

Simplification of dependent terms

Lemma ExTXT: ∀ t, (fun T : Type ⇒ TX { t T }) = T { t }.
  auto.
Qed.
Lemma EqT: ∀ n m, (fun T : Type ⇒ ap n [cte m ]) = AP n [Cte m ].
  auto.
Qed.

Lemma EqL: ∀ n a b c d,
    (fun T : Type ⇒ ap n [cte a ; cte b ; cte c ; cte d ]) =
    AP n [Cte a ; Cte b ; Cte c ; Cte d ].
  auto.
Qed.

Lemma EqTFC: ∀ n m fn,
    (fun T : Type ⇒ ap n [fc1 fn (cte m)]) =
    AP n [(FC1 fn (Cte m))].
  auto.
Qed.

Lemma EqC :∀ n p1 p2 p3 p4 ,
    (fun T:Type ⇒ ap n [Cte p1 T ; cte p2 ; cte p3 ; cte p4 ]) =
    AP n [Cte p1 ; Cte p2 ; Cte p3 ; Cte p4 ].
  auto.
Qed.

List of positive atoms

Definition ListPosAtom (L: list Lexp) : Prop := Forall IsPositiveAtom L.
Hint Unfold ListPosAtom.

Any proof must start by focusing on one of the formulas in Theory

Theorem FocusOnlyTheory:
∀ L, ListPosAtom L →
   |-F - Theory ; L ; UP [] →
   ∃ R, In R Theory ∧ |-F - Theory ; L ; DW R.
Proof.
  intros L LPosAt H.
  inversion H;subst.
  +
    apply multFalse in H1.
    assert ( ∀ F , In F L → IsPositiveAtom F).
    apply Forall_forall;auto.
    apply H3 in H1.
    contradiction.
  + ∃ F.
    split;auto.
    eapply multFalse;eauto.
Qed.

There are no atomic formulas in Theory

Ltac NotInTheory :=
  repeat match goal with
         | [H: In ?F ?T |- _] ⇒ inversion H;clear H; LexpContr
         end.
Lemma AtomNotInTheory: ∀ A, In (A ⁻)° Theory → False.
  intros.
  inversion H; NotInTheory.
Qed.

solveF solves most of the "irrelevant" goals for the focused system (e.g., testing if an atom is positive or negative, checking if a formula can be released, etc)

Ltac solveF :=
  auto;subst; simplifyG;
  repeat rewrite EqT; repeat rewrite EqC; repeat rewrite EqTFC; repeat rewrite ExTXT;
  try(
      match goal with
      | [|- Release _] ⇒ try(auto using IsPositiveAtomRelease); try(constructor)
      | [|- IsNegativeAtom _] ⇒ constructor;auto
      | [|-¬ Asynchronous _] ⇒ eauto using NotAsyncAtom, NotAsyncAtom',
                                NotAsyncOne ,NotAsyncZero, NotAsyncTensor,
                                NotAsyncPlus, NotAsyncEx, NotAsyncBang
      | [|- ¬ IsPositiveAtom ?F] ⇒ eauto using NotPATop,NotPABot,NotPAOne,
                                                NotPAZero,NotPATensor,NotPAPlus,
                                                NotPAWith,NotPAPar,NotPABang,
                                                NotPAQuest,NotPAExists,NotPAForall
      | [|- ?M =mul = ?N] ⇒ try ( (timeout 1 solve_permutation) )
      | [ |- |-F - _ ; _ ; DW (Subst _ _)] ⇒ unfold Subst; simpl
      end).

tri_negP performs the whole negative phase of a proof

applyRw applies a hypothesis involving focused sequents. Before that, some equalities are inferred.

Ltac applyRw :=
  match goal with
    [ H : |-F - ?BR ; ?Delta1 ; UP [] |- |-F - ?BR ; ?Delta2 ; UP []] ⇒
    MReplace Delta2 Delta1;
    apply H
  end.

Tactic applyRule specifies the application of a (biological) rule. This tactic decomposes the bipole and what we observe is a macro rule introducing one of the rules and then finishing in a negative phase.

Tactic Notation "applyRule" constr(Rule) :=

  match goal with
    [|- context[ T { ?time} ⁺ ] ] ⇒
    match goal with
      [|- context[ C { ?n; ?pos; ?f; ?lf} ⁺ ] ] ⇒
      tri_decide2_auto Rule ;
      apply tri_ex with (t:= time);
      apply tri_ex with (t:= Cte n) ;
      eapply tri_tensor with (N:= [ T { time} ⁺ ; C { n; pos; f; lf} ⁺]);
      [solve_permutation | eapply tri_tensor;[solve_permutation |
       apply Init1;auto | apply Init1;auto] | apply tri_rel;solveF;tri_negP ]
    end
  end.