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 : TypeTX{ t T}) = T{ t}.
  auto.
Qed.
Lemma EqT: n m, (fun T : Typeap n [cte m]) = AP n [Cte m].
  auto.
Qed.

Lemma EqL: n a b c d,
    (fun T : Typeap 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 : Typeap n [fc1 fn (cte m)]) =
    AP n [(FC1 fn (Cte m))].
  auto.
Qed.

Lemma EqC : n p1 p2 p3 p4 ,
    (fun T:Typeap 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
Ltac tri_negP :=
  repeat (
      autounfold;simpl;
      match goal with
      | [|- |-F- _ ; _ ; UP (?l :: ?L)] ⇒
        match l with
        | Atom _apply tri_store;solveF
        | Perp _apply tri_store;solveF
        | Topapply tri_top;solveF
        | Botapply tri_bot;solveF
        | Zeroapply tri_store;solveF
        | Oneapply tri_store;solveF
        | Tensor _ _apply tri_store;solveF
        | Plus _ _apply tri_store;solveF
        | Par _ _apply tri_par;solveF
        | With _ _apply tri_with;solveF;tri_negP
        | Bang _apply tri_store;solveF
        | Quest _apply tri_quest;solveF
        | Ex _apply tri_store;solveF
        | Fx _apply tri_fx;solveF;intro
        end
      end).

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.