Neighbours

This file defines the notion of neighbouring lists, in order to define a notion of sensitivity.

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

The notion of "difference" between lists for differential privacy.

• 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₂