Documentation

MIPRE.Foundations.CL.DetypingProgBits

Contiguous graph and content encodings for detyping #

The abstract sum of graph and content registers is numbered with the graph first. Vector encodings are consequently ordinary concatenations of bit lists.

source
@[reducible, inline]
abbrev MIPRE.CL.Detyping.graphDim (T : Type u_2) [Fintype T] :
ℕ
Equations
Instances For
    source
    noncomputable def MIPRE.CL.Detyping.graphEquiv {T : Type u_1} [Fintype T] :
    Graph.Coord T ≃ Fin (graphDim T)
    Equations
    Instances For
      source
      noncomputable def MIPRE.CL.Detyping.registerEquiv {T : Type u_1} [Fintype T] (s : ℕ) :
      Coord T (Fin s) ≃ Fin (graphDim T + s)
      Equations
      Instances For
        source
        noncomputable def MIPRE.CL.Detyping.graphBits {T : Type u_1} [Fintype T] (g : Graph.Coord T → 𝔽₂) :
        Cost.BitStr
        Equations
        Instances For
          source
          noncomputable def MIPRE.CL.Detyping.graphOfBits {T : Type u_1} [Fintype T] (b : Cost.BitStr) :
          Graph.Coord T → 𝔽₂
          Equations
          Instances For
            source
            @[simp]
            theorem MIPRE.CL.Detyping.graphOfBits_graphBits {T : Type u_1} [Fintype T] [DecidableEq T] (g : Graph.Coord T → 𝔽₂) :
            graphOfBits (graphBits g) = g
            source
            @[simp]
            theorem MIPRE.CL.Detyping.length_graphBits {T : Type u_1} [Fintype T] [DecidableEq T] (g : Graph.Coord T → 𝔽₂) :
            List.length (graphBits g) = graphDim T
            source
            theorem MIPRE.CL.Detyping.ofBits_take_eq (d : ℕ) (l : Cost.BitStr) :
            ofBits d (List.take d l) = ofBits d l
            source
            theorem MIPRE.CL.Detyping.graphOfBits_take_eq {T : Type u_1} [Fintype T] [DecidableEq T] (l : Cost.BitStr) :
            graphOfBits (List.take (graphDim T) l) = graphOfBits l
            source
            theorem MIPRE.CL.Detyping.push_register {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) (x : Coord T (Fin s) → 𝔽₂) :
            push (registerEquiv s).toEmbedding x = Fin.append (push graphEquiv.toEmbedding (pull Function.Embedding.inl x)) (pull Function.Embedding.inr x)
            source
            theorem MIPRE.CL.Detyping.toBits_append {m n : ℕ} (x : Fin m → 𝔽₂) (y : Fin n → 𝔽₂) :
            toBits (Fin.append x y) = toBits x ++ toBits y
            source
            theorem MIPRE.CL.Detyping.toBits_register {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) (x : Coord T (Fin s) → 𝔽₂) :
            toBits (push (registerEquiv s).toEmbedding x) = graphBits (pull Function.Embedding.inl x) ++ toBits (pull Function.Embedding.inr x)

            Numbering the sum registers is exactly concatenation of their bit strings.

            source
            theorem MIPRE.CL.Detyping.bits_split {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) (z : Fin (graphDim T + s) → 𝔽₂) :
            toBits z = graphBits (pull Function.Embedding.inl (pull (registerEquiv s).toEmbedding z)) ++ toBits (pull Function.Embedding.inr (pull (registerEquiv s).toEmbedding z))
            source
            theorem MIPRE.CL.Detyping.graphOfBits_take {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) (z : Fin (graphDim T + s) → 𝔽₂) :
            graphOfBits (List.take (graphDim T) (toBits z)) = pull Function.Embedding.inl (pull (registerEquiv s).toEmbedding z)

            The graph parser reads exactly the graph part of every well-formed vector.

            source
            theorem MIPRE.CL.Detyping.ofBits_drop {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) (z : Fin (graphDim T + s) → 𝔽₂) :
            ofBits s (List.drop (graphDim T) (toBits z)) = pull Function.Embedding.inr (pull (registerEquiv s).toEmbedding z)

            The content parser reads exactly the independent content part.

            source
            noncomputable def MIPRE.CL.Detyping.numbered {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) :
            CLFun 𝔽₂ (Fin (graphDim T + s)) (ℓ + 2)

            The actual numbered detyped CL presentation used by the machine interface.

            Equations
            Instances For
              source
              theorem MIPRE.CL.Detyping.numbered_exactlyOn {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (hP : ∀ (t : T), (P t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) :
              (numbered E w P).ExactlyOn Finset.univ