Prelude for Interactive (Oracle) Reductions

This file contains preliminary definitions and instances that is used in defining I(O)Rs.

def «term_⊕ᵥ_» : Lean.TrailingParserDescr

⊕ᵥ is notation for Sum.rec, the dependent elimination of `Sum.

This sends (a : α) → γ (.inl a) and (b : β) → γ (.inr b) to (a : α ⊕ β) → γ a.

@[implicit_reducible]

instance instDecidableEqOption {α : Type u_1} [DecidableEq α] : DecidableEq (Option α)

class VCVCompatible (α : Type u_1) extends Fintype α, Inhabited α : Type u_1

VCVCompabible is a type class for types that are finite, inhabited, and have decidable equality. These instances are needed when the type is used as the range of some OracleSpec.

• elems : Finset α
• complete (x : α) : x ∈ elems
• default : α
• type_decidableEq' : DecidableEq α

@[implicit_reducible]

instance instDecidableEqOfVCVCompatible {α : Type u_1} [VCVCompatible α] : DecidableEq α

@[simp]

theorem Vector.ofFn_get {α : Type u_1} {n : ℕ} (v : Vector α n) : ofFn v.get = v

def Equiv.rootVectorEquivFin {α : Type u_1} {n : ℕ} : Vector α n ≃ (Fin n → α)

@[implicit_reducible]

instance Vector.instFintype {α : Type u_1} {n : ℕ} [VCVCompatible α] : Fintype (Vector α n)

@[implicit_reducible]

instance instVCVCompatibleForallFin {α : Type u_1} {n : ℕ} [VCVCompatible α] : VCVCompatible (Fin n → α)

@[implicit_reducible]

instance instVCVCompatibleVector {α : Type u_1} {n : ℕ} [VCVCompatible α] : VCVCompatible (Vector α n)

class Sampleable (α : Type) extends VCVCompatible α, SampleableType α : Type

Sampleable extends VCVCompabible with SampleableType

• elems : Finset α
• complete (x : α) : x ∈ elems
• default : α
• type_decidableEq' : DecidableEq α
• selectElem : ProbComp α
• mem_support_selectElem (x : α) : x ∈ support selectElem
• probOutput_selectElem_eq (x y : α) : Pr[= x | selectElem] = Pr[= y | selectElem]

@[implicit_reducible]

instance instDecidableEqOfSampleable {α : Type} [Sampleable α] : DecidableEq α

inductive Direction : Type

Enum type for the direction of a round in a protocol specification. It is either .P_to_V (the prover sends a message to the verifier) or .V_to_P (the verifier sends a challenge to the prover).

• P_to_V : Direction
• V_to_P : Direction

@[implicit_reducible]

instance instDecidableEqDirection : DecidableEq Direction

@[implicit_reducible]

instance instInhabitedDirection : Inhabited Direction

def instInhabitedDirection.default : Direction

def instReprDirection.repr : Direction → ℕ → Std.Format

@[implicit_reducible]

instance instReprDirection : Repr Direction

def Direction.equivFin2 : Direction ≃ Fin 2

Equivalence between Direction and Fin 2, sending V_to_P to 0 and P_to_V to 1 (the choice is essentially arbitrary).

def Direction.equivBool : Direction ≃ Bool

Equivalence between Direction and Bool, sending V_to_P to false and P_to_V to true (the choice is essentially arbitrary).

@[implicit_reducible]

instance Direction.instCoeFinOfNatNat : Coe (Fin 2) Direction

This allows us to write 0 for .V_to_P and 1 for .P_to_V.

@[implicit_reducible]

instance Direction.instCoeBool : Coe Bool Direction

@[simp]

theorem Direction.not_P_to_V_eq_V_to_P {x : Direction} (h : x ≠ V_to_P) : x = P_to_V

@[simp]

theorem Direction.not_V_to_P_eq_P_to_V {x : Direction} (h : x ≠ P_to_V) : x = V_to_P

@[reducible]

def Set.language {α : Type u_1} {β : Type u_2} (rel : Set (α × β)) : Set α

The associated language Set α for a relation Set (α × β).

@[simp]

theorem Set.mem_language_iff {α : Type u_1} {β : Type u_2} (rel : Set (α × β)) (stmt : α) : stmt ∈ rel.language ↔ ∃ (wit : β), (stmt, wit) ∈ rel

@[simp]

theorem Set.not_mem_language_iff {α : Type u_1} {β : Type u_2} (rel : Set (α × β)) (stmt : α) : stmt ∉ rel.language ↔ ∀ (wit : β), (stmt, wit) ∉ rel

def acceptRejectRel : Set (Bool × Unit)

The trivial relation on Boolean statement and unit witness, which outputs the Boolean (i.e. accepts or rejects).

def acceptRejectOracleRel : Set ((Bool × (Empty → Unit)) × Unit)

The trivial relation on Boolean statement, no oracle statements, and unit witness.

@[simp]

theorem acceptRejectRel_language : acceptRejectRel.language = {true}

@[simp]

theorem acceptRejectOracleRel_language : acceptRejectOracleRel.language = {(true, fun (a : Empty) => isEmptyElim a)}