Library BioFLL.Definitions


General description

This file defines the encoding of biochemical rules into first-order linear logic. More precisely, we specify the rules governing the process of Tumorigenosis.


Constants and notations

In this section we define constants for the specification of mutations, list of mutations and locations. We also introduce some notation to ease the writing of properties and proofs.
Mutations
Definition TGFbeta := 1 .
Definition EPCAM := 2 .
Definition CD47 := 3 .
Definition CD44 := 4 .
Definition MET := 5 .
Definition seeded := 6.

Locations
Definition breast := 1.
Definition blood := 2.
Definition bone := 3.

Binary encoding of (some) lists of Mutations
Definition NONE := 0 .
Definition TG := 32 .
Definition EP := 16 .
Definition EPCD := 24 .
Definition EPCDME := 26 .
Definition EPCDCD := 28 .
Definition EPCDCDME := 30 .
Definition EPCDCDMEse := 31 .

Inductive plusOne : nat →nat → Prop :=
| po_nt : plusOne NONE TG
| po_ne :plusOne TG EP
| po_ep1 : plusOne EP EPCD
| po_epcd1 : plusOne EPCD EPCDME
| po_epcd2 : plusOne EPCD EPCDCD
| po_epcdme1 : plusOne EPCDCD EPCDCDME
| po_epcdme2 : plusOne EPCDME EPCDCDME
| po_epmese : plusOne EPCDCDME EPCDCDMEse.

Hint Constructors plusOne.

Time delays for rules

Definition d00 := 1 .
Definition d01 (f:nat) := 1 .
Definition d02 := 3 .
Definition d10 := 1 .
Definition d10r := 1 .
Definition d11 (f:nat) := 1 .
Definition d12 := 3 .
Definition d20 (f:nat) := 1 .
Definition d20r (f:nat) := f .
Definition d21 (f:nat) := f .
Definition d22 (f:nat) := 1 .
Definition d30 (f:nat) := 1 .
Definition d30r (f:nat) := f .
Definition d31 (f:nat) := f .
Definition d32 (f:nat) := f .
Definition d40 (f:nat) := f .
Definition d41 (f:nat) := f .
Definition d42 (f:nat) := f .
Definition d43 (f:nat) := f .
Definition d50 (f:nat) := f .
Definition d51 (f:nat) := match f with
                          | 1 | 2 ⇒ f
                          | 3 | 4 ⇒ f -1
                          | _ ⇒ f -2
                          end.
Definition d52 (f:nat) := 3 .
Definition d60 (f:nat) := 1 .
Definition d61 (f:nat) := match f with
                          | 1 | 2 ⇒ f
                          | 3 | 4 ⇒ f -1
                          | _ ⇒ f -2
                          end.
Definition d62 (f:nat) := 3 .
Definition d70 (f:nat) := 1 .

Definition d71 (f:nat) := match f with
                          | 1 | 2 ⇒ f
                          | 3 | 4 ⇒ f -1
                          | 5 | 6 ⇒ f -2
                          | _ ⇒ f -3
                          end.

Definition d72 (f:nat) := 2 .
Definition d80 (f:nat) := 1 .

Definition d81 (f:nat) := match f with
                          | 1 ⇒ f
                          | 2 | 3 ⇒ 2
                          | 4 | 5 ⇒ 3
                          | 6 | 7 ⇒ 4
                          | _ ⇒ 5
                          end.

Definition d82 (f:nat) := 2 .

The following notation will be used:
  • T(t) representing the current time unit.
  • C(n,c,f,lm) representing a cell where n is a Nat used as Id, c is the compartment where the cell is located, f a Nat representing the fitness of the cell and lf a list of mutations.
  • A(n) representing a cell n in the state of apoptosis

Notation "T{ t }" := (AP 3 [ t ]) .
Notation "TX{ x }" := (ap 3 [ x ]) .
Notation "Tn{ n }" := T{ (Cte n) } .
Notation "S{ t }" := (FC1 1 t).
Notation "SX{ x }" := (fc1 1 x).
Notation "DX{ n , x }" := (fc1 n x).
Notation "C{ n ; c ; f ; lm }" := (AP 1 [(Cte n) ;(Cte c) ;(Cte f) ;(Cte lm) ]) .
Notation "CX{ x ; c ; f ; lm }" := (ap 1 [(var x) ;(cte c) ;(cte f) ;(cte lm) ]) .
Notation "CF{ n ; c ; f ; lm }" :=(ap 1 [(cte n) ;(cte c) ;(var f) ;(cte lm) ]) .
Notation "A{ n }" := (AP 5 [ (Cte n) ]) .
Notation "AX{ x }" := (ap 5 [ (var x) ]) .
Notation "d 's+' t" := (FC1 d t) (at level 80, right associativity).

Rules of the System

Rules of the form T(t) x C(n;l;f;lm) --> T(t+delta) x C(n;l';f';lm') are defined as follows:
Definition EncodeRule (Dt loc fit listMut loc' fit' listMut': nat) : Lexp :=
  fun T:Type ⇒
   ex(fun t :T ⇒
     ex (fun n : T ⇒
       tensor
         (tensor (perp ( TX{ var t })) (perp (CX{n ; loc ; fit ; listMut})))
         (par (atom ( TX{ DX{ Dt , (var t) }})) (atom (CX{ n ; loc' ; fit' ; listMut'}))))) .

Rules for apoptosis
Definition EncodeRuleAP (Dt loc fit listMut : nat) : Lexp :=
  fun T:Type ⇒
    ex(fun t :T ⇒
         ex (fun n : T ⇒
               tensor
                 (tensor (perp ( TX{ var t })) (perp (CX{n ; loc ; fit ; listMut})))
                 (par (atom ( TX{ DX{ Dt , (var t) }})) (atom (AX{ n }))))) .

Hint Unfold EncodeRule .
Hint Unfold EncodeRuleAP .

In the breast:
Definition br0 := EncodeRule d00 breast 1 NONE breast 0 NONE .
Definition br1 (f:nat) := EncodeRuleAP (d01 f) breast f NONE .
Definition br2 := EncodeRule d02 breast 1 NONE breast 1 TG .
Definition brt0 := EncodeRule d10 breast 1 TG breast 0 TG .
Definition brt0r := EncodeRule d10r breast 1 TG breast 2 TG .
Definition brt1 (f:nat) := EncodeRuleAP (d11 f) breast f TG .
Definition brt2 (f:nat) := EncodeRule d12 breast f TG breast (f+1) EP .
Definition bre0 (f:nat) := EncodeRule (d20 f) breast f EP breast (f-1) EP .
Definition bre0r (f:nat) := EncodeRule (d20r f) breast f EP breast (f+1) EP .
Definition bre1 (f:nat) := EncodeRuleAP (d21 f) breast f EP .
Definition bre2 (f:nat) := EncodeRule (d22 f) breast f EP blood (f+1) EP .

In the blood:
Definition ble0 (f:nat) := EncodeRule (d30 f) blood f EP blood (f-1) EP .
Definition ble0r (f:nat) := EncodeRule (d30r f) blood f EP blood (f+1) EP .
Definition ble1 (f:nat) := EncodeRuleAP (d31 f) blood f EP .
Definition ble2 (f:nat) := EncodeRule (d32 f) blood f EP blood (f+2) EPCD .
Definition blec0 (f:nat) := EncodeRule (d40 f) blood f EPCD blood (f-1) EPCD .
Definition blec1 (f:nat) := EncodeRuleAP (d41 f) blood f EPCD .
Definition blec2 (f:nat) := EncodeRule (d42 f) blood f EPCD blood (f+2) EPCDCD .
Definition blec3 (f:nat) := EncodeRule (d43 f) blood f EPCD blood (f+2) EPCDME .
Definition blecc0 (f:nat) := EncodeRule (d50 f) blood f EPCDCD blood (f-1) EPCDCD .
Definition blecc1 (f:nat) := EncodeRuleAP (d51 f) blood f EPCDCD .
Definition blecc2 (f:nat) := EncodeRule (d52 f) blood f EPCDCD blood (f+2) EPCDCDME .
Definition blecm0 (f:nat) := EncodeRule (d60 f) blood f EPCDME blood (f-1) EPCDME .
Definition blecm1 (f:nat) := EncodeRuleAP (d61 f) blood f EPCDME .
Definition blecm2 (f:nat) := EncodeRule (d62 f) blood f EPCDME blood (f+2) EPCDCDME .
Definition bleccm0 (f:nat) := EncodeRule (d70 f) blood f EPCDCDME blood (f-1) EPCDCDME .
Definition bleccm1 (f:nat) := EncodeRuleAP (d71 f) blood f EPCDCDME .
Definition bleccm2 (f:nat) := EncodeRule (d72 f) blood f EPCDCDME bone (f+1) EPCDCDME .

In the bone:
Definition bo0 (f:nat) := EncodeRule (d80 f) bone f EPCDCDME bone (f-1) EPCDCDME .
Definition bo1 (f:nat) := EncodeRuleAP (d81 f) bone f EPCDCDME .
Definition bo2 (f:nat) := EncodeRule (d82 f) bone f EPCDCDME bone (f+1) EPCDCDMEse .

Theory containing the whole set of rules
Definition GenRs (R : nat → Lexp) (l: list nat) := map R l.

Definition Theory := [br0] ++ (GenRs br1 [0;1]) ++ [br2 ; brt0 ; brt0r] ++
                           (GenRs brt1 [0;1;2]) ++ (GenRs brt2 [1;2]) ++
                           (GenRs bre0 [1;2;3]) ++ (GenRs bre0r [1;2]) ++
                           (GenRs bre1 [0;1;2;3]) ++ (GenRs bre2 [1;2;3]) ++
                           
                           (GenRs ble0 [1;2;3;4]) ++ (GenRs ble0r [1;2;3]) ++
                           (GenRs ble1 [0;1;2;3;4]) ++
                           (GenRs ble2 [1;2;3;4]) ++ (GenRs blec0 [1;2;3;4;5;6]) ++
                           (GenRs blec1 [0;1;2;3;4;5;6]) ++ (GenRs blec2 [1;2;3;4;5;6]) ++
                           (GenRs blec3 [1;2;3;4;5;6]) ++ (GenRs blecc0 [1;2;3;4;5;6]) ++
                           (GenRs blecc1 [0;1;2;3;4;5;6;7;8]) ++
                           (GenRs blecc2 [1;2;3;4;5;6;7;8]) ++
                           (GenRs blecm0 [1;2;3;4;5;6;7;8]) ++
                           (GenRs blecm1 [0;1;2;3;4;5;6;7;8]) ++
                           (GenRs blecm2 [1;2;3;4;5;6;7;8]) ++
                           (GenRs bleccm0 [1;2;3;4;5;6;7;8;9;10]) ++
                           (GenRs bleccm1 [0;1;2;3;4;5;6;7;8;9;10]) ++
                           (GenRs bleccm2 [1;2;3;4;5;6;7;8;9;10]) ++
                           
                           (GenRs bo0 [1;2;3;4;5;6;7;8;9;10;11]) ++
                           (GenRs bo1 [0;1;2;3;4;5;6;7;8;9;10;11]) ++
                           (GenRs bo2 [1;2;3;4;5;6;7;8;9;10;11]).