Hydrophobic-polar protein folding model: basics

A treatment of the hydrophobic-polar protein folding model in a generality that covers rectangular, triangular and hexagonal lattices: P_rect, P_tri, P_hex.

We formalize the non-monotonicity of the objective function, refuting an unpublished conjecture of Stecher.

We prove objective function bounds: P_tri ≤ P_rect ≤ P_hex (using a theory of embeddings) and for any model, P ≤ b * l and P ≤ l * (l-1)/2 [see pts_earned_bound_loc']

(The latter is worth keeping when l ≤ 2b+1.)

where b is the number of moves and l is the word length. We also prove P ≤ b * l / 2 using "handshake lemma" type reasoning that was pointed out in Agarwala, Batzoglou et al. (RECOMB 97, Lemma 2.1) and a symmetry assumption on the folding model that holds for rect and hex but not for tri. The latter result required improving our definitions.

We prove the correctness of our backtracking algorithm for protein folding.

To prove some results about rotations (we can always assume our fold starts by going to the right) we use the type Fin n → α instead of Vector α n

theorem sum_pred₀ (n : ℕ) : ∑ k ∈ Finset.range n, (k - 1) = (n - 1) * (n - 2) / 2

∑₀^(n-1) (k-1) = (n-1)(n-2)/2. This uses the Lean convention 0-1=0.

theorem sum_pred (n : ℕ) : ∑ k ∈ Finset.range n.succ, (k - 1) = n * (n - 1) / 2

∑ⁿ₀ (k-1) = n (n-1) / 2. This uses the Lean convention 0-1=0.

def quad₃ : Fin 6 → ℤ × ℤ × ℤ → ℤ × ℤ × ℤ

The original protein folding model introduced by Ken Dill in 1985.

Equations

• quad₃ 0 = fun (x : ℤ × ℤ × ℤ) => x + (1, 0, 0)
• quad₃ 1 = fun (x : ℤ × ℤ × ℤ) => x + (-1, 0, 0)
• quad₃ 2 = fun (x : ℤ × ℤ × ℤ) => x + (0, 1, 0)
• quad₃ 3 = fun (x : ℤ × ℤ × ℤ) => x + (0, -1, 0)
• quad₃ 4 = fun (x : ℤ × ℤ × ℤ) => x + (0, 0, 1)
• quad₃ 5 = fun (x : ℤ × ℤ × ℤ) => x + (0, 0, -1)

def pp : ℤ × ℤ → ℤ × ℤ

The convention is that p is plus, m is minus, and s is stationary.

Equations

• pp x = x + (1, 1)

def go_D : ℤ × ℤ → ℤ × ℤ

When using keys WASD for navigation, this is D.

Equations

• go_D x = x + (1, 0)

def sp : ℤ × ℤ → ℤ × ℤ

The convention is that p is plus, m is minus, and s is stationary.

Equations

• sp x = x + (0, 1)

def mm : ℤ × ℤ → ℤ × ℤ

The convention is that p is plus, m is minus, and s is stationary.

Equations

• mm x = x + (-1, -1)

def go_A : ℤ × ℤ → ℤ × ℤ

When using keys WASD for navigation, this is A.

Equations

• go_A x = x + (-1, 0)

def sm : ℤ × ℤ → ℤ × ℤ

The convention is that p is plus, m is minus, and s is stationary.

Equations

• sm x = x + (0, -1)

def pm : ℤ × ℤ → ℤ × ℤ

The convention is that p is plus, m is minus, and s is stationary.

Equations

• pm x = x + (1, -1)

def mp : ℤ × ℤ → ℤ × ℤ

The convention is that p is plus, m is minus, and s is stationary.

Equations

• mp x = x + (-1, 1)

def go_X : ℤ × ℤ → ℤ × ℤ

When using keys WAZXDE for hexagonal navigation, this is X.

Equations

• go_X x = if Even x.2 then sp x else pp x

def go_W : ℤ × ℤ → ℤ × ℤ

When using keys WAZXDE for hexagonal navigation, this is W.

Equations

• go_W x = if Even x.2 then mm x else sm x

def go_Z : ℤ × ℤ → ℤ × ℤ

When using keys WAZXDE for hexagonal navigation, this is Z.

Equations

• go_Z x = if Even x.2 then mp x else sp x

def go_E : ℤ × ℤ → ℤ × ℤ

When using keys WAZXDE for hexagonal navigation, this is E.

Equations

• go_E x = if Even x.2 then sm x else pm x

def rectMap (a : Fin 4) : ℤ × ℤ

The four directions, horizontal and vertical.

Equations

• rectMap 0 = (1, 0)
• rectMap 1 = (-1, 0)
• rectMap 2 = (0, 1)
• rectMap 3 = (0, -1)

def rect₃Map (a : Fin 3) : ℤ × ℤ

Basically a fintype for the directions: left, right, up.

Equations

• rect₃Map 0 = (1, 0)
• rect₃Map 1 = (-1, 0)
• rect₃Map 2 = (0, 1)

def rect₃ (a : Fin 3) (x : ℤ × ℤ) : ℤ × ℤ

Three directions: left, right, up. Allows for polynomial-time optimal folding.

Equations

• rect₃ a x = x + rect₃Map a

def rect (a : Fin 4) (x : ℤ × ℤ) : ℤ × ℤ

The four directions as a map.

Equations

• rect a x = x + rectMap a

@[reducible, inline]

abbrev κ (a : Fin 4) (x : ℤ × ℤ) : ℤ × ℤ

.

Equations

• κ = rect

def hexMap (a : Fin 6) : ℤ × ℤ

move_hex represents the degree-6 hexagonal/triangular lattice, although that in itself requires checking. This representation was designed to make the y-axis vertical to fit with a computer game. def move_hex : Fin 6 → ℤ×ℤ → ℤ×ℤ | 0 => go_D | 1 => go_A | 2 => go_X | 3 => go_W | 4 => go_E | 5 => go_Z #eval move_hex 0 (0,0) #eval move_hex 5 (1,0) If computer games are not to be used we can use this simpler implementation.

Equations

• hexMap 0 = (1, 0)
• hexMap 1 = (-1, 0)
• hexMap 2 = (0, 1)
• hexMap 3 = (0, -1)
• hexMap 4 = (1, 1)
• hexMap 5 = (-1, -1)

def hex₄Map (a : Fin 4) : ℤ × ℤ

A limited move set for hexMap.

Equations

• hex₄Map 0 = (1, 0)
• hex₄Map 1 = (-1, 0)
• hex₄Map 2 = (0, 1)
• hex₄Map 3 = (1, 1)

def hex (a : Fin 6) (x : ℤ × ℤ) : ℤ × ℤ

hexMap as a function on the plane.

Equations

• hex a x = x + hexMap a

def hex₄ (a : Fin 4) (x : ℤ × ℤ) : ℤ × ℤ

hex₄Map as a function on the plane.

Equations

• hex₄ a x = x + hex₄Map a

theorem hexMap_injective : Function.Injective hexMap

hexMap is injective.

def go_WS : ℤ × ℤ → ℤ × ℤ

In the brick wall lattice, this function goes in whichever vertical direction is available.

Equations

• go_WS x = if Even (x.1 + x.2) then sp x else sm x

def tri : Fin 3 → ℤ × ℤ → ℤ × ℤ

The available moves in brick wall lattice folding.

Equations

• tri 0 = go_D
• tri 1 = go_A
• tri 2 = go_WS

def Fin_trans {l : ℕ} {k : Fin l} (i : Fin ↑k) : Fin l

Casting from Fin k to Fin l, where k < l.

Equations

• Fin_trans i = ⟨↑i, ⋯⟩

def Fin_trans_pred {l : ℕ} {k : Fin l} (i : Fin (↑k).pred) : Fin l

Casting from Fin k.pred to Fin l, where k < l.

Equations

• Fin_trans_pred i = ⟨↑i, ⋯⟩

def nearby {α : Type} {β : Type} [DecidableEq α] [Fintype β] (go : β → α → α) (p : α) (q : α) : Bool

Two points are nearby if they are one move apart.

Equations

• nearby go p q = decide (∃ (a : β), q = go a p)

def pt_loc {α : Type} {β : Type} [DecidableEq α] [Fintype β] (go : β → α → α) {l : ℕ} (fold : Mathlib.Vector α l) (i : Fin l) (j : Fin l) (phobic : Mathlib.Vector Bool l) : Bool

The (H-P reduced) amino acid sequence phobic has a match at locations i, j, according to the fold fold.

Equations

• pt_loc go fold i j phobic = (phobic.get i && phobic.get j && decide ((↑i).succ < ↑j) && nearby go (fold.get i) (fold.get j))

def pts_at' {α : Type} {β : Type} [DecidableEq α] [Fintype β] (go : β → α → α) {l : ℕ} (k : Fin l) (ph : Mathlib.Vector Bool l) (fold : Mathlib.Vector α l) : ℕ

The number of matches achieved with the fold fold for the amino acid sequence ph.

Equations

• pts_at' go k ph fold = (Finset.filter (fun (i : Fin l) => pt_loc go fold i k ph = true) Finset.univ).card

def map_predicate {β : Type} {α : Type} [Fintype β] [Fintype α] (P : β → Bool) (φ : α → β) [DecidablePred fun (i : β) => P i = true] : { x : α // x ∈ Finset.filter (fun (i : α) => P (φ i) = true) Finset.univ } → { x : β // x ∈ Finset.filter (fun (i : β) => P i = true) Finset.univ }

φ maps φ⁻¹' P to P.

Equations

• map_predicate P φ i = ⟨φ ↑i, ⋯⟩

def embed_pred {l : ℕ} (k : Fin l) (P : Fin l → Fin l → Bool) [DecidablePred fun (i : Fin l) => P i k = true] : { x : Fin (↑k).pred // x ∈ Finset.filter (fun (i : Fin (↑k).pred) => P (Fin_trans_pred i) k = true) Finset.univ } → { x : Fin l // x ∈ Finset.filter (fun (i : Fin l) => P i k = true) Finset.univ }

Cast a member of P to a member of P.

Equations

• embed_pred k P = map_predicate (fun (i : Fin l) => P i k) Fin_trans_pred

theorem embed_pred_inj {l : ℕ} (k : Fin l) (P : Fin l → Fin l → Bool) [DecidablePred fun (i : Fin l) => P i k = true] : Function.Injective (embed_pred k P)

embed_pred casting is injective.

theorem embed_pred_surj {l : ℕ} (k : Fin l) (P : Fin l → Fin l → Bool) [DecidablePred fun (i : Fin l) => P i k = true] (h : ∀ {x y : Fin l}, P x y = true → ↑x < (↑y).pred) : Function.Surjective (embed_pred k P)

embed_pred casting is surjective.

theorem embed_pred_bij {l : ℕ} (k : Fin l) {P : Fin l → Fin l → Bool} [DecidablePred fun (i : Fin l) => P i k = true] (h : ∀ {x y : Fin l}, P x y = true → ↑x < (↑y).pred) : Function.Bijective (embed_pred k P)

embed_pred casting is bijective.

theorem change_type_card_general'' {l : ℕ} (k : Fin l) (P : Fin l → Fin l → Bool) [DecidablePred fun (i : Fin l) => P i k = true] (h : ∀ {x y : Fin l}, P x y = true → (↑x).succ < ↑y) : Fintype.card { x : Fin l // x ∈ Finset.filter (fun (i : Fin l) => P i k = true) Finset.univ } = Fintype.card { x : Fin (↑k).pred // x ∈ Finset.filter (fun (i : Fin (↑k).pred) => P (Fin_trans_pred i) k = true) Finset.univ }

The number of P's is the same if we count beyond the greatest element of P.

theorem change_type_card_improved {α : Type} {β : Type} [Fintype β] (go : β → α → α) [DecidableEq α] {l : ℕ} (k : Fin l) (ph : Mathlib.Vector Bool l) (fold : Mathlib.Vector α l) : Fintype.card { x : Fin l // x ∈ Finset.filter (fun (i : Fin l) => pt_loc go fold i k ph = true) Finset.univ } = Fintype.card { x : Fin (↑k).pred // x ∈ Finset.filter (fun (i : Fin (↑k).pred) => pt_loc go fold (Fin_trans_pred i) k ph = true) Finset.univ }

The number of points is the same if we count beyond the last point.

def path_aux {α : Type} {β : Type} {l : ℕ} (go : β → α → α) (hd : β) (tl : Mathlib.Vector α l.succ) : Mathlib.Vector α l.succ.succ

Helper function for path_at.

Equations

• path_aux go hd tl = ⟨go hd tl.head :: ↑tl, ⋯⟩

def path_at {α : Type} {β : Type} (base : α) (go : β → α → α) (moves : List β) : Mathlib.Vector α moves.length.succ

Inductively defined path, starting at base (the origin, say), and proceeding through all moves according to the rules of go.

Equations

• path_at base go [] = ⟨[base], ⋯⟩
• path_at base go (head :: tail) = path_aux go head (path_at base go tail)

def path {α : Type} [Zero α] {β : Type} (go : β → α → α) (moves : List β) : Mathlib.Vector α moves.length.succ

Using OfNat here since ℤ×ℤ and ℤ×ℤ×ℤ have a natural notion of base point or zero.

Equations

• path go = path_at 0 go

def embeds_in {α : Type} {b₀ : ℕ} {b₁ : ℕ} (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) : Prop

The move set go₁ can simulate the move set go₀.

Equations

• embeds_in go₀ go₁ = ∀ (i : Fin b₀) (x : α), ∃ (j : Fin b₁), go₀ i x = go₁ j x

def is_embedding {α : Type} {b₀ : ℕ} {b₁ : ℕ} (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (f : Fin b₀ → α → Fin b₁) : Prop

The move set go₁ simulates the move set go₀ via the map f.

Equations

• is_embedding go₀ go₁ f = ∀ (i : Fin b₀) (x : α), go₀ i x = go₁ (f i x) x

def embeds_in_strongly {α : Type} {b₀ : ℕ} {b₁ : ℕ} (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) : Prop

Like embeds_in, but with an explicit Skolem function.

Equations

• (go₀ ≼ go₁) = ∃ (f : Fin b₀ → α → Fin b₁), is_embedding go₀ go₁ f

def «term_≼_» : Lean.TrailingParserDescr

.

Equations

• «term_≼_» = Lean.ParserDescr.trailingNode `«term_≼_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼ ") (Lean.ParserDescr.cat `term 51))

theorem embeds_in_strongly_transitive {α : Type} {b₀ : ℕ} {b₁ : ℕ} {b₂ : ℕ} (go₀ : Fin b₀ → α → α) (go₁ : Fin b₁ → α → α) (go₂ : Fin b₂ → α → α) : go₀ ≼ go₁ → go₁ ≼ go₂ → go₀ ≼ go₂

Embedding of move sets is transitive.

theorem embeds_in_strongly_reflexive {α : Type} {b : ℕ} (go : Fin b → α → α) : go ≼ go

Embedding of move sets is reflexive.

theorem embeds_of_strongly_embeds {α : Type} {b₀ : ℕ} {b₁ : ℕ} {go₀ : Fin b₀ → α → α} {go₁ : Fin b₁ → α → α} (h_embed : go₀ ≼ go₁) : embeds_in go₀ go₁

Embedding using a Skolem function implies ordinary embedding.

def tri_rect_embedding : Fin 3 → ℤ × ℤ → Fin 4

For tri we can only assert a pointwise version of embed_models: It follows from tri_rect_embedding that any sequence of moves under tri generates a sequence in ℤ×ℤ that can also be generated using quad.

Equations

• tri_rect_embedding 0 = fun (x : ℤ × ℤ) => 0
• tri_rect_embedding 1 = fun (x : ℤ × ℤ) => 1
• tri_rect_embedding 2 = fun (x : ℤ × ℤ) => if Even (x.1 + x.2) then 2 else 3

def rect_hex_embedding : Fin 4 → ℤ × ℤ → Fin 6

Hexagonal move set extend rectangular.

Equations

• rect_hex_embedding x = fun (x_1 : ℤ × ℤ) => ↑↑x

def rect₃_rect_embedding : Fin 3 → ℤ × ℤ → Fin 4

Rectangular move set extends limited rectangular.

Equations

• rect₃_rect_embedding x = fun (x_1 : ℤ × ℤ) => ↑↑x

theorem rect₃_rect_embedding_is_embedding (i : Fin 3) (x : ℤ × ℤ) : rect₃ i x = rect (rect₃_rect_embedding i x) x

rect₃_rect_embedding works as advertised.

theorem rect_hex_embedding_is_embedding (i : Fin 4) (x : ℤ × ℤ) : rect i x = hex (rect_hex_embedding i x) x

rect_hex_embedding works as advertised.

theorem tri_rect_embedding_is_embedding (i : Fin 3) (x : ℤ × ℤ) : tri i x = rect (tri_rect_embedding i x) x

tri_rect_embedding works as advertised.

def left_injective {α : Type} {β : Type} {γ : Type} (go : β → α → γ) : Prop

A function of two variables is left injective if it is injective in its first argument.

Equations

• left_injective go = ∀ (a : α), Function.Injective fun (b : β) => go b a

def right_injective {α : Type} {β : Type} {γ : Type} (go : β → α → γ) : Prop

A function of two variables is right injective if it is injective in its second argument.

Equations

• right_injective go = ∀ (b : β), Function.Injective fun (a : α) => go b a

theorem rect₃_rect_embedding_left_injective : left_injective rect₃_rect_embedding

rect₃_rect_embedding is left injective.

theorem tri_rect_embedding_left_injective : left_injective tri_rect_embedding

tri_rect_embedding is left injective.

theorem sp_injective : Function.Injective sp

sp is injective.

theorem sm_injective : Function.Injective sm

sm is injective.

theorem go_WS_injective : Function.Injective go_WS

go_WS is injective.

theorem right_injective_tri : right_injective tri

tri is right injective.

theorem left_injective_tri : left_injective tri

tri is left injective.

theorem rectMap_injective : Function.Injective rectMap

rectMap is injective.

theorem rect₃Map_injective : Function.Injective rect₃Map

rect₃Map is injective.

theorem left_injective_hex : left_injective hex

hex is left injective.

theorem left_injective_rect : left_injective rect

rect is left injective.

theorem left_injective_rect₃ : left_injective rect₃

rect₃ is left injective.

theorem right_injective_rect : right_injective rect

rect is right injective.

theorem right_injective_rect₃ : right_injective rect₃

rect₃ is right injective.

theorem right_injective_hex : right_injective hex

hex is right injective.

def choice_ex {β : Type} [Fintype β] {l : ℕ} (P : β → Fin l → Prop) [DecidablePred fun (a : β) => ∃ (i : Fin l), P a i] [DecidablePred fun (i : Fin l) => ∃ (a : β), P a i] [(a : β) → DecidablePred fun (n : ℕ) => ∃ (hq : n < l), P a ⟨n, hq⟩] : { x : β // x ∈ Finset.filter (fun (a : β) => ∃ (i : Fin l), P a i) Finset.univ } → { x : Fin l // x ∈ Finset.filter (fun (i : Fin l) => ∃ (a : β), P a i) Finset.univ }

If Anna has a brother, return a boy who has a sister.

Equations

• choice_ex P a = ⟨⟨Nat.find ⋯, ⋯⟩, ⋯⟩

theorem choice_ex_injective {β : Type} [Fintype β] {l : ℕ} {P : β → Fin l.succ → Prop} [DecidablePred fun (a : β) => ∃ (i : Fin l.succ), P a i] [DecidablePred fun (i : Fin l.succ) => ∃ (a : β), P a i] [(a : β) → DecidablePred fun (n : ℕ) => ∃ (hq : n < l.succ), P a ⟨n, hq⟩] (h_unique_dir : ∀ {i : Fin l.succ} {a₀ a₁ : β}, P a₀ i → P a₁ i → a₀ = a₁) : Function.Injective (choice_ex P)

If each girl has at most one brother, the map from girl-who-has-a-brother to boy-who-has-a-sister is injective.

theorem choice_ex_aux {β : Type} [Fintype β] {l : ℕ} {P : β → Fin l → Prop} [DecidablePred fun (i : Fin l) => ∃ (a : β), P a i] [DecidablePred fun (a : β) => ∃ (i : Fin l), P a i] [(a : β) → DecidablePred fun (n : ℕ) => ∃ (hq : n < l), P a ⟨n, hq⟩] {i : { x : Fin l // x ∈ Finset.filter (fun (i : Fin l) => ∃ (a : β), P a i) Finset.univ }} {a : β} (ha : P a ↑i) : P a ↑(choice_ex P ⟨a, ⋯⟩)

Anna is a sister of a chosen brother who has Anna as his sister.

theorem choice_ex_surjective {β : Type} [Fintype β] {l : ℕ} {P : β → Fin l.succ → Prop} [DecidablePred fun (a : β) => ∃ (i : Fin l.succ), P a i] [DecidablePred fun (i : Fin l.succ) => ∃ (a : β), P a i] [(a : β) → DecidablePred fun (n : ℕ) => ∃ (hq : n < l.succ), P a ⟨n, hq⟩] (h_unique_loc : ∀ {a : β} {i₀ i₁ : Fin l.succ}, P a i₀ → P a i₁ → i₀ = i₁) : Function.Surjective (choice_ex P)

If each girl has at most one brother, the map from girl-who-has-a-brother to boy-who-has-a-sister is surjective.

theorem choice_ex_bijective {β : Type} [Fintype β] {l : ℕ} {P : β → Fin l.succ → Prop} [DecidablePred fun (a : β) => ∃ (i : Fin l.succ), P a i] [DecidablePred fun (i : Fin l.succ) => ∃ (a : β), P a i] [(a : β) → DecidablePred fun (n : ℕ) => ∃ (hq : n < l.succ), P a ⟨n, hq⟩] (h_unique_loc : ∀ {a : β} {i₀ i₁ : Fin l.succ}, P a i₀ → P a i₁ → i₀ = i₁) (h_unique_dir : ∀ {i : Fin l.succ} {a₀ a₁ : β}, P a₀ i → P a₁ i → a₀ = a₁) : Function.Bijective (choice_ex P)

If each boy has at most one sister, and each girl has at most one brother, then the map that sends a boy who has a sister to a girl who has a brother is bijective.

theorem choice_ex_finset_card {β : Type} [Fintype β] {l : ℕ} {P : β → Fin l.succ → Prop} [DecidablePred fun (a : β) => ∃ (i : Fin l.succ), P a i] [DecidablePred fun (i : Fin l.succ) => ∃ (a : β), P a i] [(a : β) → DecidablePred fun (n : ℕ) => ∃ (hq : n < l.succ), P a ⟨n, hq⟩] (h_unique_loc_dir : (∀ {a : β} {i₀ i₁ : Fin l.succ}, P a i₀ → P a i₁ → i₀ = i₁) ∧ ∀ {i : Fin l.succ} {a₀ a₁ : β}, P a₀ i → P a₁ i → a₀ = a₁) : (Finset.filter (fun (a : β) => ∃ (i : Fin l.succ), P a i) Finset.univ).card = (Finset.filter (fun (i : Fin l.succ) => ∃ (a : β), P a i) Finset.univ).card

If each boy has at most one sister, and each girl has at most one brother, then there are an equal number of boys who have a sister and girls who have a brother is bijective.