Neighbours

This file defines neighbouring lists.

inductive Neighbour {T : Type} (l₁ : List T) (l₂ : List T) : Prop

Lists which differ by the inclusion or modification of an element.

This is SampCert's private property.

• Addition: ∀ {T : Type} {l₁ l₂ a b : List T} {n : T}, l₁ = a ++ b → l₂ = a ++ [n] ++ b → Neighbour l₁ l₂
• Deletion: ∀ {T : Type} {l₁ l₂ a : List T} {n : T} {b : List T}, l₁ = a ++ [n] ++ b → l₂ = a ++ b → Neighbour l₁ l₂
• Update: ∀ {T : Type} {l₁ l₂ a : List T} {n : T} {b : List T} {m : T}, l₁ = a ++ [n] ++ b → l₂ = a ++ [m] ++ b → Neighbour l₁ l₂

def Neighbour_symm {T : Type} (l₁ : List T) (l₂ : List T) (H : Neighbour l₁ l₂) : Neighbour l₂ l₁

Neighbour relation is symmetric.

Equations

• ⋯ = ⋯