Library BioFLL.MetaLevelProperties

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

Properties of the system

Here we prove some properties that require reasoning on the meta-level (e.g., checking whether it is possible to fire a rule or not and then, showing the resulting state).

Property 4

Any cell having a null fitness must go to apoptosis

Proposition Property4 :
  ∀ (n t :nat) c lm ,
  |-F - Theory ; [ Atom T { Cte t } ; Atom C { n ; c ; 0 ; lm } ] ; UP [] →
  ∃ d, |-F - Theory ; [ Atom T { d s + Cte t } ; Atom A { n } ] ; UP [].
  idtac "Proving Property 3".
  intros.
  apply FocusOnlyTheory in H;auto.
  destruct H as [R] ;destruct H.
  time "Solve:" repeat first [ CaseRule | DecomposeRule; FindUnification | eauto ].
Qed.

Property 5

The following property states one of the key properties of our model: Any cell in the blood has four possible evolutions:

acquiring passenger mutations: its fitness decreases by one and the driver mutations remain unchanged;
going to apoptosis;
acquiring a driver mutation: its fitness increases by two;
moving to the bone: its fitness increases by one and the driver mutations EPCAM, CD47, CD44, MET remain unchanged.

Definition GoalP5 (f n t m:nat) :=
  |-F - Theory ; [ Atom T { Cte t } ; Atom C { n ; blood ; f ; m } ] ; UP [] →
                                                                  In m [EPCDCD ;EPCDCDME ;EPCDCDMEse ] →
  ∃ (d m' :nat ),
  |-F - Theory ; [ Atom T { d s + Cte t } ; Atom C { n ;blood ; f -1; m } ] ; UP [] ∨
  |-F - Theory ; [ Atom T { d s + Cte t } ; Atom A { n } ] ; UP [] ∨
  (|-F - Theory ; [ Atom T { d s + Cte t } ; Atom C { n ;blood ; f +2; m' } ] ; UP [] ∧ (plusOne m m') ) ∨
  (m = EPCDCDME ∧ |-F - Theory ; [ Atom T { d s + Cte t } ; Atom C { n ;bone ; f + 1; EPCDCDME } ] ; UP []) .

Ltac SolveGoal :=
  match goal with
  | [ H: |-F - _; [T { ?d s + _} ⁺; C { _; _; _; ?m} ⁺]; UP [] |- _] ⇒
    ∃ d; ∃ m ;firstorder
  | [ H: |-F - _; [T { ?d s + _} ⁺; A { _} ⁺]; UP [] |- _] ⇒
    ∃ d; ∃ NONE;eauto
  end.

Proposition Property5 : ∀ (f n t m:nat) ,
    GoalP5 f n t m.
  idtac "Proving Property 5".
  intros f n t m HProof HCaseM.
  apply FocusOnlyTheory in HProof;auto;
    destruct HProof as [R HProof]; destruct HProof as [HIn HProof];
      time "Solve:" repeat (first [ CaseRule | DecomposeRule; FindUnification | SolveGoal]) .
Qed.