Library BioFLL.InversionTactics

Inversion Tactics

Building on a focusing system for linear logic, we implement several tactics that ease the proof of properties of the system. In particular, given a sequent (to be proved) of the form

|-F- Gamma ; Delta ; UP []

where Gamma is the unbounded context containing the set of encoded rules and Delta is the linear context (representing the current state of the system), the tactic applyRule R automatizes the process of applying the rule R to the sequent producing, as a new goal,

|-F- Gamma ; Delta' ; UP []

where Delta' is the resulting state after applying R .

We also implement some tactics for correctly inverting hypotheses of the shape H : |-F- Theory ; M ; DW (Rule). These tactics are quite useful for the proof of meta properties of the model.

Require Import Coq.Logic.FunctionalExtensionality.
Require Import LL.SequentCalculiBasicTheory.
Require Import Definitions.
Require Import Utils.

This tactic finishes the proof when there are hypotheses of the shape H: F:Lexp = G : Lexp and F, G are not the same kind of formulas

Ltac InvContradiction :=
try LexpContr;try invRel;try LexpSubst.

Asynchronous (?F $ ?G) is a contradiction and then, this tactic finishes the proof

Ltac NotAsyncSolve :=
try match goal with
| [H: ¬ Asynchronous (?F $ ?G) |- _] ⇒
(assert(Asynchronous (F $ G)) by constructor);contradiction
end.

Inversion of the par ($) subformula in the biological rules

Ltac InversionPar :=
  match goal with
    [ H: |-F - _; _; DW (?F $ ?G) |- _] ⇒
    inversion H;InvContradiction;subst;invNegAtom;clear H;
    match goal with
      [H1 : |-F - _; _; UP [F $ G] |- _] ⇒
      inversion H1;InvContradiction;subst;NotAsyncSolve;clear H1;
      match goal with
        [H2: |-F - _; _ ; UP [F;G] |- _] ⇒
        inversion H2;InvContradiction;subst;clear H2;
        match goal with
          [H3 : |-F - _; _ ++ [F]; UP [G] |- _ ] ⇒
          inversion H3;InvContradiction;subst;clear H3
        end
      end
    end
  end;
  repeat match goal with
         | [H: ¬ Asynchronous _ |- _ ] ⇒ clear H
         | [H: Release _ |- _ ] ⇒ clear H
         end.

Inferring equalities when the par subformula of the rules is introduced

Lemma FocusonParAtom:
∀ A1 A2 B M, |-F - B ; M ; DW ((A1 ⁺) $ (A2 ⁺)) →
|-F - B ; (M ++ [A1 ⁺]) ++ [A2 ⁺] ; UP [] .
intros.
InversionPar;auto.
Qed.

Inferring equalities when the initial rule is used

Lemma FocusAtom : ∀ M A, ¬Release (A ⁻) → |-F - Theory ; M ; DW (A ⁻) → M = [A ⁺] .
  intros.
  inversion H0 ;InvContradiction;subst ;invNegAtom;auto.
  apply multFalse in H5; apply AtomNotInTheory in H5;contradiction.
  contradiction.
Qed.

Inversion of the initial rule

Ltac InversionInit :=
  match goal with
    [H : |-F - _ ; ?M ; DW (?A ⁻) |- _] ⇒
    assert(M = [A ⁺]) by
        (let HRel := fresh "H" in apply FocusAtom;auto;intro HRel;
              inversion HRel;subst;
             match goal with [H : false = _ |- _] ⇒ simpl in H; inversion H end);
    clear H;subst
  end.

Inversion of the tensor

Ltac InversionTensor :=
  match goal with
    [H: |-F - _; _; DW ( ?F ** ?G ) |- _] ⇒
    inversion H;InvContradiction;subst;invNegAtom;clear H
  end.

inferring all the needed equalities when there is a proof of the shape |-F- Theory ; M ; DW ( A1 ⁻ ** A2 ⁻ )

Lemma FocusTensorAtom : ∀ M A1 A2,
  ¬Release (A1 ⁻) → ¬Release (A2 ⁻) →
  |-F - Theory ; M ; DW ( A1 ⁻ ** A2 ⁻ ) → M =mul = [A1 ⁺ ; A2 ⁺].
  intros.
  InversionTensor ; do 2 InversionInit.
  rewrite H3; auto.
Qed.

Ltac InversionRule H := inversion H;InvContradiction;clear H.

Assuming that there is a proof starting with focusing on one of the rules of the Theory , this lemma concludes all the facts that can be deduced from that proof (e.g., the shape of the linear context )

Lemma InvRuleTheory :∀ Delta c f lm c' f' lm' delay ,
    |-F - Theory ; Delta ;
      DW (fun T : Type ⇒
        ex (fun t : T ⇒
          ex (fun n : T ⇒
            tensor
              (tensor (perp TX { var t }) (perp CX { n ; c ; f ; lm }))
                (par (atom TX { DX { delay , var t }}) (atom CX { n ; c'; f'; lm'}))))) →
  ∃ M t n ,
  Delta =mul = M ++ [T { t } ⁺; (AP 1 [n ; Cte c ; Cte f ; Cte lm ]) ⁺] ∧ |-F - Theory ;
(M ++ [T { delay s + t } ⁺]) ++ [(AP 1 [n ; Cte c'; Cte f'; Cte lm']) ⁺]; UP [].
Proof.

  intros.
  match goal with
    [ H1 : |-F - _ ; _ ; DW ?R |- _] ⇒
    InversionRule H1;invNegAtom
  end;
    match goal with
      [ H2 : |-F - _ ; _ ; DW (Subst _ _) |-_ ] ⇒ InversionRule H2; invNegAtom
    end;
    match goal with
      [ H3 : |-F - _ ; _ ; DW (Subst _ _) |-_ ] ⇒ InversionRule H3; invNegAtom
    end.
  match goal with [HFG : ?F ** ?G = _ |- _ ] ⇒
                  let HFG' := fresh "HFG" in
                  assert(HFG' : F = Tensor ( Perp (T { t })) (Perp (AP 1 [t0; Cte c; Cte f; Cte lm])) ∧
                                G = Par (Atom T { FC1 delay t}) (Atom (AP 1 [t0 ; Cte c'; Cte f'; Cte lm'])) ) by
                      (split; let T' := fresh "T" in
                              extensionality T;apply @equal_f_dep with (x:=T) in H; inversion H; subst;
                              match goal with [H : ?F T' = _ |- ?F T' = _] ⇒ rewrite H end;rewrite TermFlattenG; reflexivity);
                    destruct HFG';subst;clear HFG

  end.

  apply FocusonParAtom in H5.
  match goal with
    [H : |-F - _ ; ?N ; DW ((?A1 ⁻) ** (?A2 ⁻)) |- _ ] ⇒
    assert( N =mul = [A1 ⁺ ; A2 ⁺])
      by (apply FocusTensorAtom;auto;intro HRel; inversion HRel;subst;
          match goal with [H : false = _ |- _] ⇒ simpl in H; inversion H end);
      clear H
  end.

  rewrite H in H0.
  eauto.
Qed.

Similar to InvRuleTheory but for rules going to apoptosis

Lemma InvRuleTheoryAp :∀ Delta c f lm delay ,
    |-F - Theory ; Delta ;
    DW (fun T : Type ⇒
      ex (fun t : T ⇒
        ex (fun n : T ⇒
          tensor
            (tensor (perp TX { var t }) (perp CX { n ; c ; f ; lm }))
            (par (atom TX { DX { delay , var t }}) (atom AX { n }))))) →
  ∃ M t n ,
        Delta =mul = M ++ [T { t } ⁺; (AP 1 [n ; Cte c ; Cte f ; Cte lm ]) ⁺] ∧
        |-F - Theory ; (M ++ [T { delay s + t } ⁺]) ++ [(AP 5 [n ]) ⁺];
          UP [].
  intros.

  match goal with
    [ H1 : |-F - _ ; _ ; DW ?R |- _] ⇒
    InversionRule H1;invNegAtom
  end;
    match goal with
      [ H2 : |-F - _ ; _ ; DW (Subst _ _) |-_ ] ⇒ InversionRule H2; invNegAtom
    end;
    match goal with
      [ H3 : |-F - _ ; _ ; DW (Subst _ _) |-_ ] ⇒ InversionRule H3; invNegAtom
    end.
  match goal with [HFG : ?F ** ?G = _ |- _ ] ⇒
                  let HFG' := fresh "HFG" in
                  assert(HFG' : F = Tensor ( Perp (T { t })) (Perp (AP 1 [t0; Cte c; Cte f; Cte lm])) ∧
                                G = Par (Atom T { FC1 delay t}) (Atom (AP 5 [t0])) ) by
                      (split; let T' := fresh "T" in
                              extensionality T;apply @equal_f_dep with (x:=T) in H; inversion H; subst;
                              match goal with [H : ?F T' = _ |- ?F T' = _] ⇒ rewrite H end;rewrite TermFlattenG; reflexivity);
                    destruct HFG';subst;clear HFG

  end.
  apply FocusonParAtom in H5.
  match goal with
    [H : |-F - _ ; ?N ; DW ((?A1 ⁻) ** (?A2 ⁻)) |- _ ] ⇒
    assert( N =mul = [A1 ⁺ ; A2 ⁺])
      by (apply FocusTensorAtom;auto;intro HRel; inversion HRel;subst;
          match goal with [H : false = _ |- _] ⇒ simpl in H; inversion H end);
      clear H
  end.

  rewrite H in H0.
  eauto.
Qed.

Checks whether a rule from the theory can be applied or not

Ltac DecomposeRule :=
  match goal with
    [ H : |-F - _ ; _ ; DW ?R |- _] ⇒
    idtac "Case " R ;
    first [apply InvRuleTheory in H | apply InvRuleTheoryAp in H]
  end;
  match goal with
    [ H : ∃ _, _ |- _] ⇒
    let M' := fresh "M"in
    let t' := fresh "time" in
    let n' := fresh "id" in
    let H' := fresh "H" in
    destruct H as [M' H];
    destruct H as [t' H];
    destruct H as [n' H];
    destruct H as [H H']
  end.

After the application of a rule in the Theory, this tactic infers all the needed equalities of the whole positive and negative phases

Ltac FindUnification :=
  match goal with
    [H' : [_ ; _] =mul = ?M ++ ?N |- _] ⇒
    let H0' := fresh "H" in
    apply Multiset2_empty in H' as H0';subst;simpl in H';
    apply axPair in H';destruct H';
    [ match goal with [H : _∧_ |-_] ⇒ inversion H;LexpContr;clear H end
    | match goal with [H : _∧_ |-_] ⇒ destruct H end];
    match goal with
      [H0 : [_] = [_] |- _] ⇒ inversion H0; LexpSubst;clear H0
    end
  end;LexpContr;

  match goal with
  | [H1: Tn { ?t } ⁺ = T { ?time} ⁺|- _] ⇒
    let TT := fresh "T" in
    assert(Cte t = time)
    by (extensionality TT;
        eapply @equal_f_dep with (x:=TT) in H1;inversion H1;subst;auto)
  end;

  match goal with
  | [H1: C { ?n ; _ ; _ ; _ } ⁺ = (AP 1 [?id ;_ ; _ ;_ ]) ⁺|- _] ⇒
    let TT := fresh "T" in
    assert(Cte n = id) by (extensionality TT;
                           eapply @equal_f_dep with (x:=TT) in H1;inversion H1;subst;auto)
  end;
  match goal with
  | [H1: C { _ ; _ ; _ ; _ } = (AP 1 [_ ;_ ; _ ;_ ]) |- _] ⇒
    eapply @equal_f_dep with (x:=unit) in H1;inversion H1
  end;
  subst; simpl;
  match goal with [H : |-F - _ ; _ ; UP [] |- _] ⇒ simpl in H
  end.

Case analysis on each of the rules of the Theory

Ltac CaseRule :=
  match goal with
    [ HR : In _ ?R |- _ ] ⇒ inversion HR;subst;clear HR
  end.