Neighbours

This file defines neighbouring lists.

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

Lists which differ by the inclusion or exclusion 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₂

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

Neighbour relation is symmetric.

Equations

• ⋯ = ⋯