You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
structure AGMProofSystemInstantiation (F : Type) [Field F] where
   
  Stmt : Type
   
  Sample : Type
   
  SRSElements_G1 : Type
  ListSRSElements_G1 : List SRSElements_G1
   
  SRSElements_G2 : Type
  ListSRSElements_G2 : List SRSElements_G2

   
  SRSElementValue_G1 : SRSElements_G1 → MvPolynomial Sample F
  SRSElementValue_G2 : SRSElements_G2 → MvPolynomial Sample F

   
  Proof_G1 : Type
  ListProof_G1 : List Proof_G1
  Proof_G2 : Type
  ListProof_G2 : List Proof_G2

   
  EqualityChecks : Type

   
  Pairings : EqualityChecks → Type

  ListPairings : (k : EqualityChecks) → List (Pairings k)

   
  verificationPairingSRS_G1 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements_G1 → F
   
  verificationPairingSRS_G2 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements_G2 → F
   
  verificationPairingProof_G1 : Stmt -> (k : EqualityChecks) → Pairings k → Proof_G1 → F
   
  verificationPairingProof_G2 : Stmt -> (k : EqualityChecks) → Pairings k → Proof_G2 → F

   
  Identified_Proof_Elems : List (Proof_G1 × Proof_G2) := []

def Prover (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) : Type :=
  (𝓟.Proof_G1 -> 𝓟.SRSElements_G1 -> F) × (𝓟.Proof_G2 -> 𝓟.SRSElements_G2 -> F)

noncomputable def proof_element_G1_as_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (pf_elem : 𝓟.Proof_G1) :
    MvPolynomial (𝓟.Sample) F :=
  (𝓟.ListSRSElements_G1.map fun SRS_elem =>
          MvPolynomial.C (prover.fst pf_elem SRS_elem) * (𝓟.SRSElementValue_G1 SRS_elem)).sum

noncomputable def proof_element_G2_as_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (pf_elem : 𝓟.Proof_G2) :
    MvPolynomial (𝓟.Sample) F :=
  (𝓟.ListSRSElements_G2.map fun SRS_elem =>
          MvPolynomial.C (prover.snd pf_elem SRS_elem) * (𝓟.SRSElementValue_G2 SRS_elem)).sum

noncomputable def pairing_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx) :
    MvPolynomial 𝓟.Sample F :=
  (
    ( 
      
      (
        (𝓟.ListProof_G1.map fun pf_elem => 
          C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_G1_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements_G1.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue_G1 SRS_elem)).sum
      )
    )
    *
    ( 
      
      (
        (𝓟.ListProof_G2.map fun pf_elem => 
          C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_G2_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements_G2.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue_G2 SRS_elem)).sum
      )
    )
  )

noncomputable def check_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) :
    MvPolynomial 𝓟.Sample F :=
  (
  (𝓟.ListPairings check_idx).map fun pairing =>
    𝓟.pairing_poly prover stmt check_idx pairing
  ).sum

def verify {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) : Prop :=
  (
    ∀ check_idx : 𝓟.EqualityChecks, 𝓟.check_poly prover stmt check_idx = 0
  )
  ∧
  ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
    𝓟.proof_element_G1_as_poly prover pfs.fst = 𝓟.proof_element_G2_as_poly prover pfs.snd

def soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

def completeness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (Wit : Type)
    (relation : 𝓟.Stmt -> Wit -> Prop)
    (prover : 𝓟.Stmt -> Wit -> 𝓟.Prover) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ wit : Wit,
      relation stmt wit -> 𝓟.verify (prover stmt wit) stmt

inductive Vars : Type where
  | r_v : Vars
  | r_w : Vars
  | α_v : Vars
  | α_w : Vars
  | α_y : Vars
  | β : Vars
  | γ : Vars
deriving Repr, BEq

local notation "poly_r_v" => X (some Vars.r_v)
local notation "poly_r_w" => X (some Vars.r_w)
local notation "poly_α_v" => X (some Vars.α_v)
local notation "poly_α_w" => X (some Vars.α_w)
local notation "poly_α_y" => X (some Vars.α_y)
local notation "poly_β" => X (some Vars.β)
local notation "poly_γ" => X (some Vars.γ)
local notation "poly_s" => X (none)

inductive Proof_G1_Idx : Type where
  | V_mid : Proof_G1_Idx
  | V_mid' : Proof_G1_Idx
  | W_mid : Proof_G1_Idx
  | W_mid' : Proof_G1_Idx
  | Y_mid : Proof_G1_Idx
  | Y_mid' : Proof_G1_Idx
  | Z : Proof_G1_Idx

inductive Proof_G2_Idx : Type where
  | W_mid : Proof_G2_Idx
  | H : Proof_G2_Idx

inductive ChecksIdx : Type where
  | CheckI : ChecksIdx
  | CheckII : ChecksIdx
  | CheckIII : ChecksIdx
  | CheckIV : ChecksIdx
  | CheckV : ChecksIdx

inductive PairingsI_Idx : Type where
  | lhs : PairingsI_Idx
  | rhs1 : PairingsI_Idx
  | rhs2 : PairingsI_Idx

inductive PairingsII_Idx : Type where
  | lhs : PairingsII_Idx
  | rhs : PairingsII_Idx

inductive PairingsIII_Idx : Type where
  | lhs : PairingsIII_Idx
  | rhs : PairingsIII_Idx

inductive PairingsIV_Idx : Type where
  | lhs : PairingsIV_Idx
  | rhs : PairingsIV_Idx

inductive PairingsV_Idx : Type where
  | lhs : PairingsV_Idx
  | rhs : PairingsV_Idx

inductive SRS_Elements_Idx {n_stmt n_wit d : ℕ} : Type where
  
  | EK_v : Fin n_wit -> SRS_Elements_Idx
  | EK_w : Fin n_wit -> SRS_Elements_Idx
  | EK_y : Fin n_wit -> SRS_Elements_Idx
  | EK_α_v : Fin n_wit -> SRS_Elements_Idx
  | EK_α_w : Fin n_wit -> SRS_Elements_Idx
  | EK_α_y : Fin n_wit -> SRS_Elements_Idx
  | EK_s_pow : Fin d -> SRS_Elements_Idx
  | EK_β_v_w_y : Fin n_wit -> SRS_Elements_Idx
  
  | VK_1 : SRS_Elements_Idx
  | VK_α_v : SRS_Elements_Idx
  | VK_α_w : SRS_Elements_Idx
  | VK_α_y : SRS_Elements_Idx
  | VK_γ : SRS_Elements_Idx
  | VK_βγ : SRS_Elements_Idx
  | VK_t : SRS_Elements_Idx
  | VK_v_0 : SRS_Elements_Idx
  | VK_w_0 : SRS_Elements_Idx
  | VK_y_0 : SRS_Elements_Idx
  | VK_v_stmt : Fin n_stmt -> SRS_Elements_Idx
  | VK_w_stmt : Fin n_stmt -> SRS_Elements_Idx
  | VK_y_stmt : Fin n_stmt -> SRS_Elements_Idx

noncomputable def Pinocchio
     
    {F : Type} [Field F]
     
    {n_stmt n_wit d : ℕ}
    
    
    
    
    
     
    {v_stmt : Fin n_stmt → Polynomial F }
    {w_stmt : Fin n_stmt → Polynomial F }
    {y_stmt : Fin n_stmt → Polynomial F }
    {v_wit : Fin n_wit → Polynomial F }
    {w_wit : Fin n_wit → Polynomial F }
    {y_wit : Fin n_wit → Polynomial F }
    {v_0 : Polynomial F }
    {w_0 : Polynomial F }
    {y_0 : Polynomial F }
     
    {t : Polynomial F}
    
    
    
    :
    AGMProofSystemInstantiation F :=
  { Stmt := Fin n_stmt → F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_Idx n_stmt n_wit d
    ListSRSElements_G1 :=
      ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_y i)
      ++ ((List.finRange d).map fun i => SRS_Elements_Idx.EK_s_pow i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_β_v_w_y i)
      ++ [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α_v, SRS_Elements_Idx.VK_α_w, SRS_Elements_Idx.VK_α_y, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βγ, SRS_Elements_Idx.VK_t, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_y_0]
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_v_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_w_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_y_stmt i)
    
    SRSElements_G2 := @SRS_Elements_Idx n_stmt n_wit d
    ListSRSElements_G2 :=
      ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_y i)
      ++ ((List.finRange d).map fun i => SRS_Elements_Idx.EK_s_pow i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_β_v_w_y i)
      ++ [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α_v, SRS_Elements_Idx.VK_α_w, SRS_Elements_Idx.VK_α_y, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βγ, SRS_Elements_Idx.VK_t, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_y_0]
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_v_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_w_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_y_stmt i)

    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.EK_v i => poly_r_v * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_w i => poly_r_w * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_y i => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars (y_wit i)
      | SRS_Elements_Idx.EK_α_v i => poly_r_v * poly_α_v * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_α_w i => poly_r_w * poly_α_w * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_α_y i => poly_r_v * poly_r_w * poly_α_y * to_MvPolynomial_Option Vars (y_wit i)
      | SRS_Elements_Idx.EK_s_pow i => poly_s ^ (i : ℕ)
      | SRS_Elements_Idx.EK_β_v_w_y i => poly_β * (poly_r_v * to_MvPolynomial_Option Vars (v_wit i) + poly_r_w * to_MvPolynomial_Option Vars (w_wit i) + poly_r_v * poly_r_w * to_MvPolynomial_Option Vars (y_wit i))
      | SRS_Elements_Idx.VK_1 => 1
      | SRS_Elements_Idx.VK_α_v => poly_α_v
      | SRS_Elements_Idx.VK_α_w => poly_α_w
      | SRS_Elements_Idx.VK_α_y => poly_α_y
      | SRS_Elements_Idx.VK_γ => poly_γ
      | SRS_Elements_Idx.VK_βγ => poly_β * poly_γ
      | SRS_Elements_Idx.VK_t => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.VK_v_0 => poly_r_v * to_MvPolynomial_Option Vars v_0
      | SRS_Elements_Idx.VK_w_0 => poly_r_w * to_MvPolynomial_Option Vars w_0
      | SRS_Elements_Idx.VK_y_0 => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars y_0
      | SRS_Elements_Idx.VK_v_stmt i => poly_r_v * to_MvPolynomial_Option Vars (v_stmt i)
      | SRS_Elements_Idx.VK_w_stmt i => poly_r_w * to_MvPolynomial_Option Vars (w_stmt i)
      | SRS_Elements_Idx.VK_y_stmt i => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars (y_stmt i)


    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.EK_v i => poly_r_v * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_w i => poly_r_w * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_y i => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars (y_wit i)
      | SRS_Elements_Idx.EK_α_v i => poly_r_v * poly_α_v * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_α_w i => poly_r_w * poly_α_w * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_α_y i => poly_r_v * poly_r_w * poly_α_y * to_MvPolynomial_Option Vars (y_wit i)
      | SRS_Elements_Idx.EK_s_pow i => poly_s ^ (i : ℕ)
      | SRS_Elements_Idx.EK_β_v_w_y i => poly_β * (poly_r_v * to_MvPolynomial_Option Vars (v_wit i) + poly_r_w * to_MvPolynomial_Option Vars (w_wit i) + poly_r_v * poly_r_w * to_MvPolynomial_Option Vars (y_wit i))
      | SRS_Elements_Idx.VK_1 => 1
      | SRS_Elements_Idx.VK_α_v => poly_α_v
      | SRS_Elements_Idx.VK_α_w => poly_α_w
      | SRS_Elements_Idx.VK_α_y => poly_α_y
      | SRS_Elements_Idx.VK_γ => poly_γ
      | SRS_Elements_Idx.VK_βγ => poly_β * poly_γ
      | SRS_Elements_Idx.VK_t => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.VK_v_0 => poly_r_v * to_MvPolynomial_Option Vars v_0
      | SRS_Elements_Idx.VK_w_0 => poly_r_w * to_MvPolynomial_Option Vars w_0
      | SRS_Elements_Idx.VK_y_0 => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars y_0
      | SRS_Elements_Idx.VK_v_stmt i => poly_r_v * to_MvPolynomial_Option Vars (v_stmt i)
      | SRS_Elements_Idx.VK_w_stmt i => poly_r_w * to_MvPolynomial_Option Vars (w_stmt i)
      | SRS_Elements_Idx.VK_y_stmt i => poly_r_v * poly_r_w * to_MvPolynomial_Option Vars (y_stmt i)

    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W_mid, Proof_G1_Idx.W_mid', Proof_G1_Idx.Y_mid, Proof_G1_Idx.Y_mid', Proof_G1_Idx.Z]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := [Proof_G2_Idx.W_mid, Proof_G2_Idx.H]
    EqualityChecks := ChecksIdx
    Pairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => PairingsI_Idx
      | ChecksIdx.CheckII => PairingsII_Idx
      | ChecksIdx.CheckIII => PairingsIII_Idx
      | ChecksIdx.CheckIV => PairingsIV_Idx
      | ChecksIdx.CheckV => PairingsV_Idx
    ListPairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs1, PairingsI_Idx.rhs2]
      | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
      | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
      | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
      | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs]
    verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_v_0 => 1
          | SRS_Elements_Idx.VK_v_stmt k => stmt k
          | _ => 0
        | PairingsI_Idx.rhs1 => match SRS_idx with
          | SRS_Elements_Idx.VK_t => 1
          | _ => 0
        | PairingsI_Idx.rhs2 => match SRS_idx with
          | SRS_Elements_Idx.VK_y_0 => 1
          | SRS_Elements_Idx.VK_y_stmt k => stmt k
          | _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsII_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsIII_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsIV_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsV_Idx.rhs => match SRS_idx with
          | _ => 0
    verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_w_0 => 1
          | SRS_Elements_Idx.VK_w_stmt k => stmt k
          | _ => 0
        | PairingsI_Idx.rhs1 => 0
        | PairingsI_Idx.rhs2 => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => -1 
          | _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsII_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α_v => -1 
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsIII_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α_w => -1 
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsIV_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α_y => -1 
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_γ => 1
          | _ => 0
        | PairingsV_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_βγ => -1 
          | _ => 0
    verificationPairingProof_G1 := fun stmt check_idx i pf_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
        | PairingsI_Idx.rhs1 => match pf_idx with
          | _ => 0
        | PairingsI_Idx.rhs2 => match pf_idx with
          | Proof_G1_Idx.Y_mid => 1
          | _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.V_mid' => 1
          | _ => 0
        | PairingsII_Idx.rhs => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.W_mid' => 1
          | _ => 0
        | PairingsIII_Idx.rhs => match pf_idx with
          | Proof_G1_Idx.W_mid => 1
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.Y_mid' => 1
          | _ => 0
        | PairingsIV_Idx.rhs => match pf_idx with
          | Proof_G1_Idx.Y_mid => 1
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.Z => 1
          | _ => 0
        | PairingsV_Idx.rhs => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | Proof_G1_Idx.W_mid => 1
          | Proof_G1_Idx.Y_mid => 1
          | _ => 0
    verificationPairingProof_G2 := fun stmt check_idx i pf_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match pf_idx with
          | Proof_G2_Idx.W_mid => 1
          | _ => 0
        | PairingsI_Idx.rhs1 => match pf_idx with
          | Proof_G2_Idx.H => -1 
          | _ => 0
        | PairingsI_Idx.rhs2 => match pf_idx with
          | _ => 0
      | ChecksIdx.CheckII => 0
      | ChecksIdx.CheckIII => 0
      | ChecksIdx.CheckIV => 0
      | ChecksIdx.CheckV => 0
    Identified_Proof_Elems := [(Proof_G1_Idx.W_mid, Proof_G2_Idx.W_mid)]
  }

structure ProofState where
  tacCtx : Elab.Tactic.Context
  tacState : Elab.Tactic.State
  termCtx : Elab.Term.Context
  termState : Elab.Term.State
  metaCtx : Meta.Context
  metaState : Meta.State

def ProofState.get : Elab.Tactic.TacticM ProofState :=
  fun tacCtx tacState termCtx termState metaCtx metaState => do
    let tacState ← tacState.get
    let termState ← termState.get
    let metaState ← metaState.get
    return { tacCtx, tacState, termCtx, termState, metaCtx, metaState }

def ProofState.with : ProofState → Elab.Tactic.TacticM α → CoreM α :=
  fun { tacCtx, tacState, termCtx, termState, metaCtx, metaState } x => do
    let tacState ← IO.mkRef tacState
    let termState ← IO.mkRef termState
    let metaState ← IO.mkRef metaState
    x tacCtx tacState termCtx termState metaCtx metaState

elab tk:"##" tac:(tacticSeq)? : command => do
  let state :: rest := proofStateExt.getState (← getEnv)
    | throwError "proof mode not started, use `start_proof`"
  Elab.Command.liftTermElabM do
    state.with do
      Elab.Tactic.withTacticInfoContext tk do
        if let some tac := tac then
          Elab.Tactic.evalTactic tac
      if (← Elab.Tactic.getUnsolvedGoals).isEmpty then
        logInfoAt tk "Goals accomplished 🎉"
        modifyEnv (proofStateExt.setState · rest)
      else
        modifyEnv (proofStateExt.setState · ((← ProofState.get) :: rest))

inductive Vars : Type where
  | α : Vars
  | β_v : Vars
  | β_w : Vars
  | β_y : Vars
  | γ : Vars
deriving Repr, BEq

local notation "poly_α" => X (some Vars.α)
local notation "poly_β_v" => X (some Vars.β_v)
local notation "poly_β_w" => X (some Vars.β_w)
local notation "poly_β_y" => X (some Vars.β_y)
local notation "poly_γ" => X (some Vars.γ)
local notation "poly_s" => X (none)

inductive Proof_G1_Idx : Type where
  | V_mid : Proof_G1_Idx
  | V_mid' : Proof_G1_Idx
  | W' : Proof_G1_Idx
  | Y : Proof_G1_Idx
  | H' : Proof_G1_Idx

inductive Proof_G2_Idx : Type where
  | W : Proof_G2_Idx
  | H : Proof_G2_Idx

inductive ChecksIdx : Type where
  | CheckI : ChecksIdx
  | CheckII : ChecksIdx
  | CheckIII : ChecksIdx
  | CheckIV : ChecksIdx
  | CheckV : ChecksIdx

inductive PairingsI_Idx : Type where
  | lhs : PairingsI_Idx
  | rhs : PairingsI_Idx

inductive PairingsII_Idx : Type where
  | lhs : PairingsII_Idx
  | rhs : PairingsII_Idx

inductive PairingsIII_Idx : Type where
  | lhs : PairingsIII_Idx
  | rhs : PairingsIII_Idx

inductive PairingsIV_Idx : Type where
  | lhs : PairingsIV_Idx
  | rhs : PairingsIV_Idx

inductive PairingsV_Idx : Type where
  | lhs : PairingsV_Idx
  | rhs1 : PairingsV_Idx
  | rhs2 : PairingsV_Idx

inductive SRS_Elements_Idx {n_stmt n_wit m d : ℕ} : Type where
  
  | EK_s_pow : Fin d -> SRS_Elements_Idx
  | EK_α_s_pow : Fin d -> SRS_Elements_Idx
  
  | EK_v : Fin n_wit -> SRS_Elements_Idx
  | EK_w : Fin m -> SRS_Elements_Idx
  | EK_α_v : Fin n_wit -> SRS_Elements_Idx
  | EK_α_w : Fin m -> SRS_Elements_Idx
  | EK_β_v : Fin n_wit -> SRS_Elements_Idx
  | EK_β_w : Fin m -> SRS_Elements_Idx
  
  | VK_1 : SRS_Elements_Idx
  | VK_α : SRS_Elements_Idx
  | VK_γ : SRS_Elements_Idx
  | VK_βv_γ : SRS_Elements_Idx
  | VK_βw_γ : SRS_Elements_Idx
  | VK_v_0 : SRS_Elements_Idx
  | VK_w_0 : SRS_Elements_Idx
  | VK_t : SRS_Elements_Idx
  | VK_v_stmt : Fin n_stmt -> SRS_Elements_Idx

noncomputable def GGPR
     
    {F : Type} [Field F]
     
    {n_stmt n_wit m d : ℕ}
    
    
    
    
    
     
    {v_stmt : Fin n_stmt → Polynomial F }
    {v_wit : Fin n_wit → Polynomial F }
    {w_wit : Fin m → Polynomial F }
    {v_0 : Polynomial F }
    {w_0 : Polynomial F }
     
    {r : Fin (n_wit) → F} :
    AGMProofSystemInstantiation F :=

   
  let t : Polynomial F := ∏ i : Fin n_wit in Finset.univ, (Polynomial.X - Polynomial.C (r i));
  { Stmt := Fin n_stmt → F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_Idx n_stmt n_wit m d
    ListSRSElements_G1 :=
      ((List.finRange d).map fun i => SRS_Elements_Idx.EK_s_pow i)
      ++ ((List.finRange d).map fun i => SRS_Elements_Idx.EK_α_s_pow i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_v i)
      ++ ((List.finRange m).map fun i => SRS_Elements_Idx.EK_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_v i)
      ++ ((List.finRange m).map fun i => SRS_Elements_Idx.EK_α_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_β_v i)
      ++ ((List.finRange m).map fun i => SRS_Elements_Idx.EK_β_w i)
      ++ [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ, SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t]
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_v_stmt i)
    
    SRSElements_G2 := @SRS_Elements_Idx n_stmt n_wit m d
    ListSRSElements_G2 :=
      ((List.finRange d).map fun i => SRS_Elements_Idx.EK_s_pow i)
      ++ ((List.finRange d).map fun i => SRS_Elements_Idx.EK_α_s_pow i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_v i)
      ++ ((List.finRange m).map fun i => SRS_Elements_Idx.EK_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_v i)
      ++ ((List.finRange m).map fun i => SRS_Elements_Idx.EK_α_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_β_v i)
      ++ ((List.finRange m).map fun i => SRS_Elements_Idx.EK_β_w i)
      ++ [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ, SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t]
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_v_stmt i)

    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.EK_s_pow i => poly_s ^ (i : ℕ)
      | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ (i : ℕ)
      | SRS_Elements_Idx.EK_v i => to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_w i => to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_α_v i => poly_α * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_α_w i => poly_α * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_β_v i => poly_β_v * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_β_w i => poly_β_w * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.VK_1 => 1
      | SRS_Elements_Idx.VK_α => poly_α
      | SRS_Elements_Idx.VK_γ => poly_γ
      | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
      | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
      | SRS_Elements_Idx.VK_v_0 => to_MvPolynomial_Option Vars v_0
      | SRS_Elements_Idx.VK_w_0 => to_MvPolynomial_Option Vars w_0
      | SRS_Elements_Idx.VK_t => to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.VK_v_stmt i => to_MvPolynomial_Option Vars (v_stmt i)

    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.EK_s_pow i => poly_s ^ (i : ℕ)
      | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ (i : ℕ)
      | SRS_Elements_Idx.EK_v i => to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_w i => to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_α_v i => poly_α * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_α_w i => poly_α * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.EK_β_v i => poly_β_v * to_MvPolynomial_Option Vars (v_wit i)
      | SRS_Elements_Idx.EK_β_w i => poly_β_w * to_MvPolynomial_Option Vars (w_wit i)
      | SRS_Elements_Idx.VK_1 => 1
      | SRS_Elements_Idx.VK_α => poly_α
      | SRS_Elements_Idx.VK_γ => poly_γ
      | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
      | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
      | SRS_Elements_Idx.VK_v_0 => to_MvPolynomial_Option Vars v_0
      | SRS_Elements_Idx.VK_w_0 => to_MvPolynomial_Option Vars w_0
      | SRS_Elements_Idx.VK_t => to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.VK_v_stmt i => to_MvPolynomial_Option Vars (v_stmt i)

    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H']
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H]
    EqualityChecks := ChecksIdx
    Pairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => PairingsI_Idx
      | ChecksIdx.CheckII => PairingsII_Idx
      | ChecksIdx.CheckIII => PairingsIII_Idx
      | ChecksIdx.CheckIV => PairingsIV_Idx
      | ChecksIdx.CheckV => PairingsV_Idx
    ListPairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
      | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
      | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
      | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
      | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2]
    
    
    
    
    
    
    verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_v_0 => 1
          | SRS_Elements_Idx.VK_v_stmt k => stmt k
          | _ => 0
        | PairingsI_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_t => 1
          | _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsII_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsIII_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α => 1
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsIV_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α => 1
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsV_Idx.rhs1 => match SRS_idx with
          | _ => 0
        | PairingsV_Idx.rhs2 => match SRS_idx with
          | SRS_Elements_Idx.VK_βw_γ => 1
          | _ => 0
    
    
    
    
    
    verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_w_0 => 1
          | _ => 0
        | PairingsI_Idx.rhs => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsII_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α => -1 
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsIII_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsIV_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_γ => 1
          | _ => 0
        | PairingsV_Idx.rhs1 => match SRS_idx with
          | SRS_Elements_Idx.VK_βv_γ => -1 
          | _ => 0
        | PairingsV_Idx.rhs2 => match SRS_idx with
          | _ => 0
    
    
    
    
    
    verificationPairingProof_G1 := fun stmt check_idx i pf_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
        | PairingsI_Idx.rhs => match pf_idx with
          | _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.V_mid' => 1
          | _ => 0
        | PairingsII_Idx.rhs => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.W' => 1
          | _ => 0
        | PairingsIII_Idx.rhs => match pf_idx with
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.H' => 1
          | _ => 0
        | PairingsIV_Idx.rhs => match pf_idx with
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.Y => 1
          | _ => 0
        | PairingsV_Idx.rhs1 => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
        | PairingsV_Idx.rhs2 => match pf_idx with
          | _ => 0
    
    
    
    
    
    verificationPairingProof_G2 := fun stmt check_idx i pf_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match pf_idx with
          | Proof_G2_Idx.W => 1
          | _ => 0
        | PairingsI_Idx.rhs => match pf_idx with
          | Proof_G2_Idx.H => -1 
          | _ => 0
      | ChecksIdx.CheckII => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match pf_idx with
          | _ => 0
        | PairingsIII_Idx.rhs => match pf_idx with
          | Proof_G2_Idx.W => -1 
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match pf_idx with
          | _ => 0
        | PairingsIV_Idx.rhs => match pf_idx with
          | Proof_G2_Idx.H => -1 
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match pf_idx with
          | _ => 0
        | PairingsV_Idx.rhs1 => match pf_idx with
          | _ => 0
        | PairingsV_Idx.rhs2 => match pf_idx with
          | Proof_G2_Idx.W => -1 
          | _ => 0
    Identified_Proof_Elems := []
  }

inductive Vars : Type where
  | α : Vars
  | β : Vars
  | γ : Vars
  | δ : Vars
deriving Repr, BEq

local notation "Vars_α" => some Vars.α
local notation "Vars_β" => some Vars.β
local notation "Vars_γ" => some Vars.γ
local notation "Vars_δ" => some Vars.δ
local notation "Vars_x" => none

inductive Proof_G1_Idx : Type where
  | A : Proof_G1_Idx
  | C : Proof_G1_Idx

inductive Proof_G2_Idx : Type where
  | B : Proof_G2_Idx

instance : Fintype Proof_G2_Idx :=
  ⟨⟨[Proof_G2_Idx.B], by admit /- proof elided -/
  ⟩, fun x => by admit /- proof elided -/
  ⟩

inductive PairingsIdx : Type where
  | ab : PairingsIdx
  | αβ : PairingsIdx
  | stmtγ : PairingsIdx
  | cδ : PairingsIdx

inductive SRS_Elements_G1_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | α : SRS_Elements_G1_Idx
  | β : SRS_Elements_G1_Idx
  | δ : SRS_Elements_G1_Idx
  | x_pow : Fin n_var → SRS_Elements_G1_Idx
  | x_pow_times_t : Fin (n_var - 1) → SRS_Elements_G1_Idx
  | y : Fin n_stmt → SRS_Elements_G1_Idx
  | q : Fin n_wit → SRS_Elements_G1_Idx

inductive SRS_Elements_G2_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | β : SRS_Elements_G2_Idx
  | γ : SRS_Elements_G2_Idx
  | δ : SRS_Elements_G2_Idx
  | x_pow : Fin n_var → SRS_Elements_G2_Idx

noncomputable def Groth16TypeIII
     
    {F : Type} [Field F]
     
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
     
    {r : Fin n_wit → F} :
    AGMProofSystemInstantiation F :=
  let t : Polynomial F :=
    ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
  {
    Stmt := Fin n_stmt -> F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_G1_Idx n_stmt n_wit n_var
    ListSRSElements_G1 :=
      [SRS_Elements_G1_Idx.α]
      ++ [SRS_Elements_G1_Idx.β]
      ++ [SRS_Elements_G1_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G1_Idx.x_pow i)
      ++ ((List.finRange (n_var - 1)).map fun i => SRS_Elements_G1_Idx.x_pow_times_t i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_G1_Idx.y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_G1_Idx.q i)
    SRSElements_G2 := @SRS_Elements_G2_Idx n_stmt n_wit n_var
    ListSRSElements_G2 :=
      [SRS_Elements_G2_Idx.β]
      ++ [SRS_Elements_G2_Idx.γ]
      ++ [SRS_Elements_G2_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G2_Idx.x_pow i)
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G1_Idx.α => X Vars_γ * X Vars_δ * X Vars_α
      | SRS_Elements_G1_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_G1_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_G1_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
      | SRS_Elements_G1_Idx.x_pow_times_t i => X Vars_γ
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_G1_Idx.y i => ((X Vars_β * X Vars_δ) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      (X Vars_α * X Vars_δ) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      X Vars_δ * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_G1_Idx.q i => (X Vars_β * X Vars_γ) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      (X Vars_α * X Vars_γ) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      X Vars_γ * to_MvPolynomial_Option Vars (w_wit i)
      
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G2_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_G2_Idx.γ => X Vars_γ * X Vars_δ * X Vars_γ
      | SRS_Elements_G2_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_G2_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.A, Proof_G1_Idx.C]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := [Proof_G2_Idx.B]
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.ab, PairingsIdx.αβ, PairingsIdx.stmtγ, PairingsIdx.cδ]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 1
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y i => stmt i
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q i => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 1
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 1
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 1
        | SRS_Elements_G2_Idx.x_pow _ => 0
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G1_Idx.A => 1
        | Proof_G1_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 1
    verificationPairingProof_G2 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G2_Idx.B => -1
      | PairingsIdx.αβ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G2_Idx.B => 0
  }

noncomputable def u_sum {F : Type} [Field F] {n_stmt n_wit : ℕ}
    (u_stmt : Fin n_stmt → (Polynomial F))
    (u_wit : Fin n_wit → (Polynomial F))
    (stmt : Fin n_stmt -> F)
    (wit : Fin n_wit -> F)
    : Polynomial F :=
  List.sum (List.map (fun j => Polynomial.C (stmt j) * (u_stmt j)) (List.finRange n_stmt))
  + List.sum (List.map (fun j => Polynomial.C (wit j) * (u_wit j)) (List.finRange n_wit))

noncomputable def v_sum {F : Type} [Field F] {n_stmt n_wit : ℕ}
    (v_stmt : Fin n_stmt → (Polynomial F))
    (v_wit : Fin n_wit → (Polynomial F))
    (stmt : Fin n_stmt -> F)
    (wit : Fin n_wit -> F)
    : Polynomial F :=
  List.sum (List.map (fun j => Polynomial.C (stmt j) * (v_stmt j)) (List.finRange n_stmt))
  + List.sum (List.map (fun j => Polynomial.C (wit j) * (v_wit j)) (List.finRange n_wit))

noncomputable def w_sum {F : Type} [Field F] {n_stmt n_wit : ℕ}
    (w_stmt : Fin n_stmt → (Polynomial F))
    (w_wit : Fin n_wit → (Polynomial F))
    (stmt : Fin n_stmt -> F)
    (wit : Fin n_wit -> F)
    : Polynomial F :=
  List.sum (List.map (fun j => Polynomial.C (stmt j) * (w_stmt j)) (List.finRange n_stmt))
  + List.sum (List.map (fun j => Polynomial.C (wit j) * (w_wit j)) (List.finRange n_wit))

noncomputable def wit_prover (F : Type) [Field F]
    (n_stmt n_wit n_var : ℕ)
    (u_stmt : Fin n_stmt → (Polynomial F)) (u_wit : Fin n_wit → (Polynomial F))
    (v_stmt : Fin n_stmt → (Polynomial F)) (v_wit : Fin n_wit → (Polynomial F))
    (w_stmt : Fin n_stmt → (Polynomial F)) (w_wit : Fin n_wit → (Polynomial F))
    (r : Fin n_wit → F)
    (stmt : Fin n_stmt -> F)
    (wit : Fin n_wit -> F) :
    (Groth16TypeIII
      (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
      (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
      (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r)).Prover where
        fst pf_elem srs_elem := match pf_elem with
          | Proof_G1_Idx.A => match srs_elem with
            | SRS_Elements_G1_Idx.α => 1
            | SRS_Elements_G1_Idx.β => 0
            | SRS_Elements_G1_Idx.δ => 0
            | SRS_Elements_G1_Idx.x_pow i => (u_sum u_stmt u_wit stmt wit).coeff i
            | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
            | SRS_Elements_G1_Idx.y i => 0
            | SRS_Elements_G1_Idx.q i => 0
          | Proof_G1_Idx.C =>
            match srs_elem with
            | SRS_Elements_G1_Idx.α => 0
            | SRS_Elements_G1_Idx.β => 0
            | SRS_Elements_G1_Idx.δ => 0
            | SRS_Elements_G1_Idx.x_pow _ => 0
            | SRS_Elements_G1_Idx.x_pow_times_t i =>
              let t : Polynomial F := ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
              (((u_sum u_stmt u_wit stmt wit) * (v_sum v_stmt v_wit stmt wit) - (w_sum w_stmt w_wit stmt wit)) /ₘ t).coeff i
            | SRS_Elements_G1_Idx.y i => 0
            | SRS_Elements_G1_Idx.q i => wit i
        snd pf_elem srs_elem := match pf_elem with
          | Proof_G2_Idx.B => match srs_elem with
            | SRS_Elements_G2_Idx.β => 1
            | SRS_Elements_G2_Idx.γ => 0
            | SRS_Elements_G2_Idx.δ => 0
            | SRS_Elements_G2_Idx.x_pow i => (v_sum v_stmt v_wit stmt wit).coeff i

def is_complete
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {r : Fin n_wit → F} :
    (completeness
      F
      (Groth16TypeIII
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        let t : Polynomial F :=
          ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit))))
            *
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * v_wit i) (List.finRange n_wit))))
            -
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * w_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * w_wit i) (List.finRange n_wit))))
            %ₘ t = 0
        )
      )
      (
        wit_prover
          (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
          (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
          (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r)
      )
    ) :=

def ElimApp.evalNames_add (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax)
    (numEqs := 0) (numGeneralized := 0) (toClear : Array FVarId := #[]) :
    TermElabM (Array MVarId) := do
  let mut names : List Syntax := withArg[1].getArgs |>.toList
  let mut subgoals := #[]
  for { name := altName, mvarId := g, .. } in alts do
    let numFields ← getAltNumFields elimInfo altName
    let (altVarNames, names') := names.splitAtD numFields (Unhygienic.run `(_))
    names := names'
    let (fvars, g) ← g.introN numFields <| altVarNames.map ((fun n => (Name.str n "foo")) ∘ (getNameOfIdent' ·[0]))
    let some (g, subst) ← Cases.unifyEqs? numEqs g {} | pure ()
    let (_, g) ← g.introNP numGeneralized
    let g ← liftM $ toClear.foldlM (·.tryClear) g
    for fvar in fvars, stx in altVarNames do
      g.withContext <| (subst.apply <| .fvar fvar).addLocalVarInfoForBinderIdent ⟨stx⟩
    subgoals := subgoals.push g
  pure subgoals

elab (name := new_name_cases) "new_name_cases " tgts:(Parser.Tactic.casesTarget,+) usingArg:((" using " ident)?)
  withArg:((" with" (ppSpace colGt binderIdent)+)?) : tactic => do
  let targets ← elabCasesTargets tgts.1.getSepArgs
  let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
  g.withContext do
    let elimInfo ← getElimNameInfo usingArg targets (induction := false)
    let targets ← addImplicitTargets elimInfo targets
    let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← g.getTag)
    let elimArgs := result.elimApp.getAppArgs
    let targets ← elimInfo.targetsPos.mapM (instantiateMVars elimArgs[·]!)
    let motive := elimArgs[elimInfo.motivePos]!
    let g ← generalizeTargetsEq g (← inferType motive) targets
    let (targetsNew, g) ← g.introN targets.size
    g.withContext do
      ElimApp.setMotiveArg g motive.mvarId! targetsNew
      g.assign result.elimApp
      let subgoals ← ElimApp.evalNames_add elimInfo result.alts withArg
         (numEqs := targets.size) (toClear := targetsNew)
      setGoals <| subgoals.toList ++ gs

inductive Vars : Type where
  | y : Vars
deriving Repr, BEq

local notation "Vars_y" => some Vars.y
local notation "Vars_x" => none

inductive Proof_G1_Idx : Type where
  | A : Proof_G1_Idx
  | C : Proof_G1_Idx

inductive Proof_G2_Idx : Type where
  | B : Proof_G2_Idx

instance : Fintype Proof_G2_Idx :=
  ⟨⟨[Proof_G2_Idx.B], by admit /- proof elided -/
  ⟩, fun x => by admit /- proof elided -/
  ⟩

inductive PairingsIdx : Type where
  | ab : PairingsIdx
  | αβ : PairingsIdx
  | stmtγ : PairingsIdx
  | cδ : PairingsIdx

inductive SRS_Elements_G1_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | α : SRS_Elements_G1_Idx
  | β : SRS_Elements_G1_Idx
  | δ : SRS_Elements_G1_Idx
  | x_pow : Fin n_var → SRS_Elements_G1_Idx
  | x_pow_times_t : Fin (n_var - 1) → SRS_Elements_G1_Idx
  | y : Fin n_stmt → SRS_Elements_G1_Idx
  | q : Fin n_wit → SRS_Elements_G1_Idx

inductive SRS_Elements_G2_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | β : SRS_Elements_G2_Idx
  | γ : SRS_Elements_G2_Idx
  | δ : SRS_Elements_G2_Idx
  | x_pow : Fin n_var → SRS_Elements_G2_Idx

noncomputable def Lipmaa
     
    {F : Type} [Field F]
     
    {n_stmt n_wit n_var : ℕ}
     
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
     
    {r : Fin n_wit → F} :
    AGMProofSystemInstantiation F :=
  let t : Polynomial F :=
    ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
  {
    Stmt := Fin n_stmt -> F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_G1_Idx n_stmt n_wit n_var
    ListSRSElements_G1 :=
      [SRS_Elements_G1_Idx.α]
      ++ [SRS_Elements_G1_Idx.β]
      ++ [SRS_Elements_G1_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G1_Idx.x_pow i)
      ++ ((List.finRange (n_var - 1)).map fun i => SRS_Elements_G1_Idx.x_pow_times_t i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_G1_Idx.y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_G1_Idx.q i)
    SRSElements_G2 := @SRS_Elements_G2_Idx n_stmt n_wit n_var
    ListSRSElements_G2 :=
      [SRS_Elements_G2_Idx.β]
      ++ [SRS_Elements_G2_Idx.γ]
      ++ [SRS_Elements_G2_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G2_Idx.x_pow i)
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G1_Idx.α => (X Vars_y ^ 5) * (X Vars_y ^ 1) * (X Vars_y ^ 75)
      | SRS_Elements_G1_Idx.β => (X Vars_y ^ 5) * (X Vars_y ^ 1) * (X Vars_y ^ 25)
      | SRS_Elements_G1_Idx.δ => (X Vars_y ^ 5) * (X Vars_y ^ 1) * (X Vars_y ^ 1)
      | SRS_Elements_G1_Idx.x_pow i => (X Vars_y ^ 5) * (X Vars_y ^ 1) * X Vars_x ^ (i : ℕ)
      | SRS_Elements_G1_Idx.x_pow_times_t i => (X Vars_y ^ 5)
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_G1_Idx.y i => (((X Vars_y ^ 25) * (X Vars_y ^ 1)) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      ((X Vars_y ^ 75) * (X Vars_y ^ 1)) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      (X Vars_y ^ 1) * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_G1_Idx.q i => ((X Vars_y ^ 25) * (X Vars_y ^ 5)) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      ((X Vars_y ^ 75) * (X Vars_y ^ 5)) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      (X Vars_y ^ 5) * to_MvPolynomial_Option Vars (w_wit i)
      
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G2_Idx.β => (X Vars_y ^ 5) * (X Vars_y ^ 1) * (X Vars_y ^ 25)
      | SRS_Elements_G2_Idx.γ => (X Vars_y ^ 5) * (X Vars_y ^ 1) * (X Vars_y ^ 5)
      | SRS_Elements_G2_Idx.δ => (X Vars_y ^ 5) * (X Vars_y ^ 1) * (X Vars_y ^ 1)
      | SRS_Elements_G2_Idx.x_pow i => (X Vars_y ^ 5) * (X Vars_y ^ 1) * X Vars_x ^ (i : ℕ)
    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.A, Proof_G1_Idx.C]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := [Proof_G2_Idx.B]
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.ab, PairingsIdx.αβ, PairingsIdx.stmtγ, PairingsIdx.cδ]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 1
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y i => stmt i
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q i => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 1
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 1
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 1
        | SRS_Elements_G2_Idx.x_pow _ => 0
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G1_Idx.A => 1
        | Proof_G1_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 1
    verificationPairingProof_G2 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G2_Idx.B => -1
      | PairingsIdx.αβ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G2_Idx.B => 0
  }

structure StraightforwardAGMProofSystem where
   
  Aux : Type
   
  Vars : Type
   
  degreeBound : Vars → ℕ

   
  nSRSComponents_G1 : ℕ
   
  SRSElements_G1_Lengths : Fin nSRSComponents_G1 -> ℕ -> ℕ -> Aux -> ℕ
   
  nSRSComponents_G2 : ℕ
  SRSElements_G2_Lengths : Fin nSRSComponents_G2 -> ℕ -> ℕ -> Aux -> ℕ

def compile_Fin_list (l : List ℕ) : List (Fin (l.length)) := sorry

def StraightforwardAGMProofSystem.toAGMProofSystem (F : Type) [Field F] (n_stmt n_wit : ℕ)
    (𝓟 : StraightforwardAGMProofSystem) (aux : 𝓟.Aux) : AGMProofSystemInstantiation F where
  Stmt := Fin n_stmt -> F
  Sample := Option 𝓟.Vars
  SRSElements_G1 := List.foldl Sum Empty ((𝓟.SRSElements_G1_Lengths n_stmt n_wit aux).map Fin)
  ListSRSElements_G1 := List.foldl List.append [] (_)
  SRSElements_G2 := _
  ListSRSElements_G2 := _
  SRSElementValue_G1 := _
  SRSElementValue_G2 := _
  Proof_G1 := _
  ListProof_G1 := _
  Proof_G2 := _
  ListProof_G2 := _
  EqualityChecks := _
  Pairings := _
  ListPairings := _
  verificationPairingSRS_G1 := _
  verificationPairingSRS_G2 := _
  verificationPairingProof_G1 := _
  verificationPairingProof_G2 := _

def StraightforwardAGMProofSystem.soundness (F : Type) [Field F] (n_stmt n_wit : ℕ)
    (𝓟 : StraightforwardAGMProofSystem F n_stmt n_wit) : Prop := sorry

noncomputable def to_MvPolynomial_Option {F : Type} [Field F] (V : Type) :
    Polynomial F →+* MvPolynomial (Option V) F
  where
    toFun p := Polynomial.eval₂ (MvPolynomial.C) (MvPolynomial.X none) p
    map_one' := by admit /- proof elided -/

structure AGMProofSystemInstantiation (F : Type) [Field F] where
   
  Stmt : Type
   
  Sample : Type
   
  SRSElements_G1 : Type
  [FintypeSRSElements_G1 : Fintype SRSElements_G1]
   
  SRSElements_G2 : Type
  [FintypeSRSElements_G2 : Fintype SRSElements_G2]

   
  SRSElementValue_G1 : (i : SRSElements_G1) → MvPolynomial (Sample) F
  SRSElementValue_G2 : (i : SRSElements_G2) → MvPolynomial (Sample) F

   
  Proof_G1 : Type
  [FintypeProof_G1 : Fintype Proof_G1]
  Proof_G2 : Type
  [FintypeProof_G2 : Fintype Proof_G2]

   
  EqualityChecks : Type

   
  Pairings : EqualityChecks → Type

  [FintypePairings : (k : EqualityChecks) → Fintype (Pairings k)]

   
  verificationPairingSRS_G1 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : SRSElements_G1) → F
   
  verificationPairingSRS_G2 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : SRSElements_G2) → F
   
  verificationPairingProof_G1 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : Proof_G1) → F
   
  verificationPairingProof_G2 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : Proof_G2) → F

def AGMProofSystemInstantiation.Prover (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) : Type :=
  (𝓟.Proof_G1 -> 𝓟.SRSElements_G1 -> F) × (𝓟.Proof_G2 -> 𝓟.SRSElements_G2 -> F)

def AGMProofSystemInstantiation.verify {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) : Prop :=
  ∀ check_idx : 𝓟.EqualityChecks,
    ∑ pairing : (𝓟.Pairings check_idx),
      ( 
        
        (
          ∑ pf_elem : 𝓟.FintypeProof_G1.elems, 
            C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) 
            *
            
            ∑ SRS_elem : 𝓟.FintypeSRSElements_G1.elems,
              C (prover.fst pf_elem SRS_elem) * (𝓟.SRSElementValue_G1 SRS_elem)
        )
        +
        ( 
          ∑ SRS_elem : 𝓟.FintypeSRSElements_G1.elems,
            C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue_G1 SRS_elem)
        )
      )
      *
      ( 
        
        (
          ∑ pf_elem : 𝓟.FintypeProof_G2.elems, 
            C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) 
            *
            
            ∑ SRS_elem : 𝓟.FintypeSRSElements_G2.elems,
              C (prover.snd pf_elem SRS_elem) * (𝓟.SRSElementValue_G2 SRS_elem)
        )
        +
        ( 
          ∑ SRS_elem : 𝓟.FintypeSRSElements_G2.elems,
            C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue_G2 SRS_elem)
        )
      )
    = 0

def AGMProofSystemInstantiation.soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

inductive Vars : Type where
  | α : Vars
  | β : Vars
  | γ : Vars
  | δ : Vars
deriving Repr, BEq

local notation "Vars_α" => some Vars.α
local notation "Vars_β" => some Vars.β
local notation "Vars_γ" => some Vars.γ
local notation "Vars_δ" => some Vars.δ
local notation "Vars_x" => none

inductive Proof_G1_Idx : Type where
  | A : Proof_G1_Idx
  | C : Proof_G1_Idx

inductive Proof_G2_Idx : Type where
  | B : Proof_G2_Idx

instance : Fintype Proof_G2_Idx :=
  ⟨⟨[Proof_G2_Idx.B], by admit /- proof elided -/
  ⟩, fun x => by admit /- proof elided -/
  ⟩

inductive PairingsIdx : Type where
  | ab : PairingsIdx
  | αβ : PairingsIdx
  | stmtγ : PairingsIdx
  | cδ : PairingsIdx

inductive SRS_Elements_G1_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | α : SRS_Elements_G1_Idx
  | β : SRS_Elements_G1_Idx
  | δ : SRS_Elements_G1_Idx
  | x_pow : Fin n_var → SRS_Elements_G1_Idx
  | x_pow_times_t : Fin (n_var - 1) → SRS_Elements_G1_Idx
  | y : Fin n_stmt → SRS_Elements_G1_Idx
  | q : Fin n_wit → SRS_Elements_G1_Idx

inductive SRS_Elements_G2_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | β : SRS_Elements_G2_Idx
  | γ : SRS_Elements_G2_Idx
  | δ : SRS_Elements_G2_Idx
  | x_pow : Fin n_var → SRS_Elements_G2_Idx

noncomputable def Groth16TypeIII
     
    {F : Type} [Field F]
     
    {n_stmt n_wit n_var : ℕ}
     
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
     
    {t : Polynomial F} :
    AGMProofSystemInstantiation F :=
  {
    Stmt := Fin n_stmt -> F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_G1_Idx n_stmt n_wit n_var
    ListSRSElements_G1 :=
      [SRS_Elements_G1_Idx.α]
      ++ [SRS_Elements_G1_Idx.β]
      ++ [SRS_Elements_G1_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G1_Idx.x_pow i)
      ++ ((List.finRange (n_var - 1)).map fun i => SRS_Elements_G1_Idx.x_pow_times_t i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_G1_Idx.y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_G1_Idx.q i)
    SRSElements_G2 := @SRS_Elements_G2_Idx n_stmt n_wit n_var
    ListSRSElements_G2 :=
      [SRS_Elements_G2_Idx.β]
      ++ [SRS_Elements_G2_Idx.γ]
      ++ [SRS_Elements_G2_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G2_Idx.x_pow i)
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G1_Idx.α => X Vars_γ * X Vars_δ * X Vars_α
      | SRS_Elements_G1_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_G1_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_G1_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
      | SRS_Elements_G1_Idx.x_pow_times_t i => X Vars_γ
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_G1_Idx.y i => ((X Vars_β * X Vars_δ) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      (X Vars_α * X Vars_δ) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      X Vars_δ * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_G1_Idx.q i => (X Vars_β * X Vars_γ) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      (X Vars_α * X Vars_γ) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      X Vars_γ * to_MvPolynomial_Option Vars (w_wit i)
      
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G2_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_G2_Idx.γ => X Vars_γ * X Vars_δ * X Vars_γ
      | SRS_Elements_G2_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_G2_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.A, Proof_G1_Idx.C]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := [Proof_G2_Idx.B]
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.ab, PairingsIdx.αβ, PairingsIdx.stmtγ, PairingsIdx.cδ]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 1
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y i => stmt i
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q i => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 1
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 1
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 1
        | SRS_Elements_G2_Idx.x_pow _ => 0
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G1_Idx.A => 1
        | Proof_G1_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 1
    verificationPairingProof_G2 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G2_Idx.B => -1
      | PairingsIdx.αβ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G2_Idx.B => 0
  }

noncomputable def changeExponent_G1 (𝓟 : AGMProofSystemInstantiation F) (sample : 𝓟.Sample)
    (d : ℕ) :
    AGMProofSystemInstantiation F where
      Stmt := 𝓟.Stmt
      Sample := 𝓟.Sample
      SRSElements_G1 := 𝓟.SRSElements_G1
      ListSRSElements_G1 := 𝓟.ListSRSElements_G1
      SRSElements_G2 := 𝓟.SRSElements_G2
      ListSRSElements_G2 := 𝓟.ListSRSElements_G2
      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i
      SRSElementValue_G2 := 𝓟.SRSElementValue_G2
      Proof_G1 := 𝓟.Proof_G1
      ListProof_G1 := 𝓟.ListProof_G1
      Proof_G2 := 𝓟.Proof_G2
      ListProof_G2 := 𝓟.ListProof_G2
      EqualityChecks := 𝓟.EqualityChecks
      Pairings := 𝓟.Pairings
      ListPairings := 𝓟.ListPairings
      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1
      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2
      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1
      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2
      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems
 := by admit /- proof elided -/

structure AGMProofSystemInstantiationFin (F : Type) [Field F] where
   
  nSample : ℕ
   
  nSRSElements_G1 : ℕ
   
  nSRSElements_G2 : ℕ

   
  SRSElementValue_G1 : (i : Fin nSRSElements_G1) → MvPolynomial (Fin nSample) F
  SRSElementValue_G2 : (i : Fin nSRSElements_G2) → MvPolynomial (Fin nSample) F

   
  nProof_G1 : ℕ
  nProof_G2 : ℕ

   
  nEqualityChecks : ℕ

   
  nPairings : Fin nEqualityChecks → ℕ

   
  verificationPairingSRS_G1 : (i : Fin nSRSElements_G1)
                                → (k : Fin nEqualityChecks) → (l : Fin (nPairings k)) → F
   
  verificationPairingSRS_G2 : (i : Fin nSRSElements_G2)
                                → (k : Fin nEqualityChecks) → (l : Fin (nPairings k)) → F
   
  verificationPairingProof_G1 : (i : Fin nProof_G1)
                                → (k : Fin nEqualityChecks) → (l : Fin (nPairings k)) → F
   
  verificationPairingProof_G2 : (i : Fin nProof_G2)
                                → (k : Fin nEqualityChecks) → (l : Fin (nPairings k)) → F

structure AGMProofSystemInstantiationIndexForm (F : Type) [Field F] where
   
  Stmt : Type
   
  Sample : Type
   
  SRSElements_G1 : Type
   
  SRSElements_G2 : Type

   
  SRSElementValue_G1 : (i : SRSElements_G1) → MvPolynomial (Sample) F
  SRSElementValue_G2 : (i : SRSElements_G2) → MvPolynomial (Sample) F

   
  Proof_G1 : Type
  Proof_G2 : Type

   
  EqualityChecks : Type

   
  Pairings : EqualityChecks → Type

   
  verificationPairingSRS_G1 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : SRSElements_G1) → F
   
  verificationPairingSRS_G2 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : SRSElements_G2) → F
   
  verificationPairingProof_G1 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : Proof_G1) → F
   
  verificationPairingProof_G2 : Stmt -> (k : EqualityChecks) → (l : (Pairings k)) → (i : Proof_G2) → F

noncomputable def changeExponent_G1 (𝓟 : AGMProofSystemInstantiation F) (sample : 𝓟.Sample)
    (d : ℕ) :
    AGMProofSystemInstantiation F where
      Stmt := 𝓟.Stmt
      Sample := 𝓟.Sample
      SRSElements_G1 := 𝓟.SRSElements_G1
      ListSRSElements_G1 := 𝓟.ListSRSElements_G1
      SRSElements_G2 := 𝓟.SRSElements_G2
      ListSRSElements_G2 := 𝓟.ListSRSElements_G2
      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i
      SRSElementValue_G2 := 𝓟.SRSElementValue_G2
      Proof_G1 := 𝓟.Proof_G1
      ListProof_G1 := 𝓟.ListProof_G1
      Proof_G2 := 𝓟.Proof_G2
      ListProof_G2 := 𝓟.ListProof_G2
      EqualityChecks := 𝓟.EqualityChecks
      Pairings := 𝓟.Pairings
      ListPairings := 𝓟.ListPairings
      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1
      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2
      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1
      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2
      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems

noncomputable def collapseSRSElement_G1 (𝓟 : AGMProofSystemInstantiation F)
    [DecidableEq 𝓟.SRSElements_G1] (twin1 twin2 : 𝓟.SRSElements_G1) :
    AGMProofSystemInstantiation F where
      Stmt := 𝓟.Stmt
      Sample := 𝓟.Sample
      SRSElements_G1 := 𝓟.SRSElements_G1
      ListSRSElements_G1 := 𝓟.ListSRSElements_G1
      SRSElements_G2 := 𝓟.SRSElements_G2
      ListSRSElements_G2 := 𝓟.ListSRSElements_G2
      SRSElementValue_G1 := fun srs => if srs = twin1
                                        then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs
      SRSElementValue_G2 := 𝓟.SRSElementValue_G2
      Proof_G1 := 𝓟.Proof_G1
      ListProof_G1 := 𝓟.ListProof_G1
      Proof_G2 := 𝓟.Proof_G2
      ListProof_G2 := 𝓟.ListProof_G2
      EqualityChecks := 𝓟.EqualityChecks
      Pairings := 𝓟.Pairings
      ListPairings := 𝓟.ListPairings
      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1
      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2
      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1
      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2
      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems

noncomputable def collapseToxicWaste (𝓟 : AGMProofSystemInstantiation F) (d : ℕ)
    [DecidableEq 𝓟.Sample]
    (sample_removed sample_target : 𝓟.Sample) :
    AGMProofSystemInstantiation F where
      Stmt := 𝓟.Stmt
      Sample := 𝓟.Sample
      SRSElements_G1 := 𝓟.SRSElements_G1
      ListSRSElements_G1 := 𝓟.ListSRSElements_G1
      SRSElements_G2 := 𝓟.SRSElements_G2
      ListSRSElements_G2 := 𝓟.ListSRSElements_G2
      SRSElementValue_G1 := fun elem => MvPolynomial.bind₁
                              ((fun x => (if x = sample_removed then MvPolynomial.X (R := F) sample_target ^ d else MvPolynomial.X x)))
                              (𝓟.SRSElementValue_G1 elem)
      SRSElementValue_G2 := fun elem => MvPolynomial.bind₁
                              ((fun x => (if x = sample_removed then MvPolynomial.X (R := F) sample_target ^ d else MvPolynomial.X x)))
                              (𝓟.SRSElementValue_G2 elem)
      Proof_G1 := 𝓟.Proof_G1
      ListProof_G1 := 𝓟.ListProof_G1
      Proof_G2 := 𝓟.Proof_G2
      ListProof_G2 := 𝓟.ListProof_G2
      EqualityChecks := 𝓟.EqualityChecks
      Pairings := 𝓟.Pairings
      ListPairings := 𝓟.ListPairings
      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1
      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2
      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1
      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2
      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems

partial def casesMatchingOr (matcher : Expr → MetaM Bool) (recursive := false) (allowSplit := true)
    (throwOnNoMatch := true) (g : MVarId) : MetaM (List MVarId) := do
  let result := (← go g).toList
  if throwOnNoMatch && result == [g] then
    throwError "no match"
  else
    return result
  where

def elabPatterns_Or (pats : Array Term) : TermElabM (Array AbstractMVarsResult) :=
  withTheReader Term.Context (fun ctx ↦ { ctx with ignoreTCFailures := true }) <|
  Term.withoutErrToSorry <|
  pats.mapM fun p ↦ Term.withoutModifyingElabMetaStateWithInfo do
    withRef p <| abstractMVars (← Term.elabTerm p none)

def matchPatterns_Or (pats : Array AbstractMVarsResult) (e : Expr) : MetaM Bool := do
  let e ← instantiateMVars e
  pats.anyM fun p ↦ return (← Conv.matchPattern? p e) matches some (_, #[])

inductive Vars : Type where
  | β : Vars
  | γ : Vars
deriving Repr, BEq

local notation "Vars_β" => some Vars.β
local notation "Vars_γ" => some Vars.γ
local notation "Vars_τ" => none

inductive Proof_Idx : Type where
  | H : Proof_Idx
  | V : Proof_Idx
  | B : Proof_Idx

inductive SRS_Elements_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | τ_pow : Fin n_var → SRS_Elements_Idx
  | γ : SRS_Elements_Idx
  | γβ : SRS_Elements_Idx
  | βu : Fin n_wit → SRS_Elements_Idx

inductive ChecksIdx : Type where
  | CheckI : ChecksIdx
  | CheckII : ChecksIdx

inductive PairingsI_Idx : Type where
  | ht : PairingsI_Idx
  | gg : PairingsI_Idx
  | vv : PairingsI_Idx

inductive PairingsII_Idx : Type where
  | bγ : PairingsII_Idx
  | γβv : PairingsII_Idx

noncomputable def BabySNARK
     
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
     
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {t : Polynomial F} :
    AGMProofSystemInstantiation F :=
  {
    Stmt := Fin n_stmt -> F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_Idx n_stmt n_wit n_var
    ListSRSElements_G1 :=
      ((List.finRange n_var).map fun i => SRS_Elements_Idx.τ_pow i)
      ++ [SRS_Elements_Idx.γ]
      ++ [SRS_Elements_Idx.γβ]
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.βu i)
    SRSElements_G2 := @SRS_Elements_Idx n_stmt n_wit n_var
    ListSRSElements_G2 :=
      ((List.finRange n_var).map fun i => SRS_Elements_Idx.τ_pow i)
      ++ [SRS_Elements_Idx.γ]
      ++ [SRS_Elements_Idx.γβ]
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.βu i)
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.τ_pow i => X Vars_τ ^ (i : ℕ)
      | SRS_Elements_Idx.γ => X Vars_β
      | SRS_Elements_Idx.γβ => X Vars_γ * X Vars_β
      | SRS_Elements_Idx.βu i => X Vars_β * to_MvPolynomial_Option Vars (u_wit i)
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.τ_pow i => X Vars_τ ^ (i : ℕ)
      | SRS_Elements_Idx.γ => X Vars_β
      | SRS_Elements_Idx.γβ => X Vars_γ * X Vars_β
      | SRS_Elements_Idx.βu i => X Vars_β * to_MvPolynomial_Option Vars (u_wit i)
    Proof_G1 := Proof_Idx
    ListProof_G1 := [Proof_Idx.H, Proof_Idx.V, Proof_Idx.B]
    Proof_G2 := Proof_Idx
    ListProof_G2 := [Proof_Idx.H, Proof_Idx.V, Proof_Idx.B]
    EqualityChecks := ChecksIdx
    Pairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => PairingsI_Idx
      | ChecksIdx.CheckII => PairingsII_Idx
    ListPairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => [PairingsI_Idx.ht, PairingsI_Idx.gg, PairingsI_Idx.vv]
      | ChecksIdx.CheckII => [PairingsII_Idx.bγ, PairingsII_Idx.γβv]
    verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.ht => match SRS_idx with
          | SRS_Elements_Idx.τ_pow i => t.coeff i
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
        | PairingsI_Idx.gg => match SRS_idx with
          | SRS_Elements_Idx.τ_pow i => if (i : ℕ) = 0 then 1 else 0
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
        | PairingsI_Idx.vv => match SRS_idx with
          | SRS_Elements_Idx.τ_pow i => List.sum (List.map (fun j => (stmt j) * (u_stmt j).coeff i) (List.finRange n_stmt))
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.bγ => match SRS_idx with
          | SRS_Elements_Idx.τ_pow _ => 0
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
        | PairingsII_Idx.γβv => match SRS_idx with
          | SRS_Elements_Idx.τ_pow _ => 0
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 1
          | SRS_Elements_Idx.βu _ => 0
    verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.ht => match SRS_idx with
          | SRS_Elements_Idx.τ_pow i => t.coeff i
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
        | PairingsI_Idx.gg => match SRS_idx with
          | SRS_Elements_Idx.τ_pow i => if (i : ℕ) = 0 then 1 else 0
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
        | PairingsI_Idx.vv => match SRS_idx with
          | SRS_Elements_Idx.τ_pow i => -List.sum (List.map (fun j => (stmt j) * (u_stmt j).coeff i) (List.finRange n_stmt))
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.bγ => match SRS_idx with
          | SRS_Elements_Idx.τ_pow _ => 0
          | SRS_Elements_Idx.γ => 1
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
        | PairingsII_Idx.γβv => match SRS_idx with
          | SRS_Elements_Idx.τ_pow _ => 0
          | SRS_Elements_Idx.γ => 0
          | SRS_Elements_Idx.γβ => 0
          | SRS_Elements_Idx.βu _ => 0
    verificationPairingProof_G1 := fun stmt check_idx i pf => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.ht => match pf with
          | Proof_Idx.H => 1
          | Proof_Idx.V => 0
          | Proof_Idx.B => 0
        | PairingsI_Idx.gg => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => 0
          | Proof_Idx.B => 0
        | PairingsI_Idx.vv => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => 1
          | Proof_Idx.B => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.bγ => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => 0
          | Proof_Idx.B => 1
        | PairingsII_Idx.γβv => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => 0
          | Proof_Idx.B => 0
    verificationPairingProof_G2 := fun stmt check_idx i pf => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.ht => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => 0
          | Proof_Idx.B => 0
        | PairingsI_Idx.gg => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => 0
          | Proof_Idx.B => 0
        | PairingsI_Idx.vv => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => -1
          | Proof_Idx.B => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.bγ => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => 0
          | Proof_Idx.B => 0
        | PairingsII_Idx.γβv => match pf with
          | Proof_Idx.H => 0
          | Proof_Idx.V => -1
          | Proof_Idx.B => 0
    Identified_Proof_Elems := [(Proof_Idx.H, Proof_Idx.H), (Proof_Idx.V, Proof_Idx.V), (Proof_Idx.B, Proof_Idx.B)]
  }

inductive Vars : Type where
  | α : Vars
  | β : Vars
deriving Repr, BEq

inductive StmtEntries : Type where
  | x : StmtEntries
  | y : StmtEntries
  | z : StmtEntries
deriving Repr, BEq

inductive WitEntries : Type where
  | A : WitEntries
  | B : WitEntries
deriving Repr, BEq

local notation "Vars_α" => some Vars.α
local notation "Vars_β" => some Vars.β
local notation "Vars_x" => none

inductive Proof_G1_Idx : Type where
  | Pf : Proof_G1_Idx

instance : Fintype Proof_G1_Idx :=
  ⟨⟨[Proof_G1_Idx.Pf], by admit /- proof elided -/
  ⟩, fun x => by admit /- proof elided -/
  ⟩

def Proof_G2_Idx : Type := Empty

instance : Fintype Proof_G2_Idx := inferInstanceAs (Fintype Empty)

inductive PairingsIdx : Type where
  | lhs : PairingsIdx
  | rhs : PairingsIdx

instance : Fintype PairingsIdx :=
  ⟨⟨[PairingsIdx.lhs, PairingsIdx.rhs], by admit /- proof elided -/
  ⟩,
    fun x => by admit /- proof elided -/
    ⟩

inductive SRS_Elements_G1_Idx : Type where
  | α : SRS_Elements_G1_Idx
  | β : SRS_Elements_G1_Idx

inductive SRS_Elements_G2_Idx : Type where
  | α : SRS_Elements_G2_Idx
  | β : SRS_Elements_G2_Idx

noncomputable def ToySnark
     
    {F : Type} [Field F] :
    AGMProofSystemInstantiation F :=
  {
    Stmt := StmtEntries -> F
    Sample := Option Vars
    SRSElements_G1 := SRS_Elements_G1_Idx
    ListSRSElements_G1 :=
      [.α, .β]
    SRSElements_G2 := SRS_Elements_G2_Idx
    ListSRSElements_G2 :=
      [.α, .β]
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G1_Idx.α => MvPolynomial.X Vars_α
      | SRS_Elements_G1_Idx.β => MvPolynomial.X Vars_β
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G2_Idx.α => MvPolynomial.X Vars_α
      | SRS_Elements_G2_Idx.β => MvPolynomial.X Vars_β
    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.Pf]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := []
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.lhs, PairingsIdx.rhs]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.lhs => 0
      | PairingsIdx.rhs => match SRS_idx with
        | SRS_Elements_G1_Idx.α => stmt StmtEntries.z
        | SRS_Elements_G1_Idx.β => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.lhs => match SRS_idx with
        | SRS_Elements_G2_Idx.α => stmt StmtEntries.x
        | SRS_Elements_G2_Idx.β => stmt StmtEntries.y
      | PairingsIdx.rhs => match SRS_idx with
        | SRS_Elements_G2_Idx.α => 0
        | SRS_Elements_G2_Idx.β => -1
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.lhs => match pf with
        | Proof_G1_Idx.Pf => 1
      | PairingsIdx.rhs => match pf with
        | Proof_G1_Idx.Pf => 0
    verificationPairingProof_G2 := fun stmt _ i pf => 0
  }

inductive Vars : Type where
  | α : Vars
  | β : Vars
  | γ : Vars
  | δ : Vars
deriving Repr, BEq

local notation "Vars_α" => some Vars.α
local notation "Vars_β" => some Vars.β
local notation "Vars_γ" => some Vars.γ
local notation "Vars_δ" => some Vars.δ
local notation "Vars_x" => none

inductive Proof_Idx : Type where
  | A : Proof_Idx
  | B : Proof_Idx
  | C : Proof_Idx

inductive PairingsIdx : Type where
  | ab : PairingsIdx
  | αβ : PairingsIdx
  | stmtγ : PairingsIdx
  | cδ : PairingsIdx

inductive SRS_Elements_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | α : SRS_Elements_Idx
  | β : SRS_Elements_Idx
  | δ : SRS_Elements_Idx
  | γ : SRS_Elements_Idx
  | x_pow : Fin n_var → SRS_Elements_Idx
  | x_pow_times_t : Fin (n_var - 1) → SRS_Elements_Idx
  | y : Fin n_stmt → SRS_Elements_Idx
  | q : Fin n_wit → SRS_Elements_Idx

noncomputable def Groth16TypeI
     
    {F : Type} [Field F]
     
    {n_stmt n_wit n_var : ℕ}
     
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
     
    {r : Fin n_wit → F} :
    AGMProofSystemInstantiation F :=
  let t : Polynomial F :=
    ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
  {
    Stmt := Fin n_stmt -> F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_Idx n_stmt n_wit n_var
    ListSRSElements_G1 :=
      [SRS_Elements_Idx.α]
      ++ [SRS_Elements_Idx.β]
      ++ [SRS_Elements_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_Idx.x_pow i)
      ++ ((List.finRange (n_var - 1)).map fun i => SRS_Elements_Idx.x_pow_times_t i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.q i)
    SRSElements_G2 := @SRS_Elements_Idx n_stmt n_wit n_var
    ListSRSElements_G2 :=
      [SRS_Elements_Idx.β]
      ++ [SRS_Elements_Idx.γ]
      ++ [SRS_Elements_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_Idx.x_pow i)
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.α => X Vars_γ * X Vars_δ * X Vars_α
      | SRS_Elements_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_Idx.γ => X Vars_γ * X Vars_δ * X Vars_γ
      | SRS_Elements_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
      | SRS_Elements_Idx.x_pow_times_t i => X Vars_γ
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.y i => ((X Vars_β * X Vars_δ) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      (X Vars_α * X Vars_δ) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      X Vars_δ * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_Idx.q i => (X Vars_β * X Vars_γ) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      (X Vars_α * X Vars_γ) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      X Vars_γ * to_MvPolynomial_Option Vars (w_wit i)
      
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.α => X Vars_γ * X Vars_δ * X Vars_α
      | SRS_Elements_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_Idx.γ => X Vars_γ * X Vars_δ * X Vars_γ
      | SRS_Elements_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
      | SRS_Elements_Idx.x_pow_times_t i => X Vars_γ
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.y i => ((X Vars_β * X Vars_δ) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      (X Vars_α * X Vars_δ) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      X Vars_δ * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_Idx.q i => (X Vars_β * X Vars_γ) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      (X Vars_α * X Vars_γ) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      X Vars_γ * to_MvPolynomial_Option Vars (w_wit i)
      
    Proof_G1 := Proof_Idx
    ListProof_G1 := [Proof_Idx.A, Proof_Idx.B, Proof_Idx.C]
    Proof_G2 := Proof_Idx
    ListProof_G2 := [Proof_Idx.A, Proof_Idx.B, Proof_Idx.C]
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.ab, PairingsIdx.αβ, PairingsIdx.stmtγ, PairingsIdx.cδ]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_Idx.α => 0
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y _ => 0
        | SRS_Elements_Idx.q _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_Idx.α => 1
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y _ => 0
        | SRS_Elements_Idx.q _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_Idx.α => 0
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y i => stmt i
        | SRS_Elements_Idx.q _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_Idx.α => 0
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y _ => 0
        | SRS_Elements_Idx.q i => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_Idx.β => 1
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 1
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 1
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_Idx.A => 1
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 1
    verificationPairingProof_G2 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => -1
        | Proof_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
    Identified_Proof_Elems := [(Proof_Idx.A, Proof_Idx.A), (Proof_Idx.B, Proof_Idx.B), (Proof_Idx.C, Proof_Idx.C)]
  }

structure AGMProofSystemInstantiation (F : Type) [Field F] where
   
  Stmt : Type
   
  Sample : Type
   
  SRSElements : Type
  ListSRSElements : List SRSElements

   
  SRSElementValue : SRSElements → MvPolynomial Sample F

   
  Proof : Type
  ListProof : List Proof

   
  EqualityChecks : Type

   
  Pairings : EqualityChecks → Type

  ListPairings : (k : EqualityChecks) → List (Pairings k)

   
  verificationPairingSRS_G1 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
   
  verificationPairingSRS_G2 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
   
  verificationPairingProof_G1 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F
   
  verificationPairingProof_G2 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F

def Prover (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) : Type :=
  (𝓟.Proof -> 𝓟.SRSElements -> F) × (𝓟.Proof -> 𝓟.SRSElements -> F)

noncomputable def proof_element_as_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (pf_elem : 𝓟.Proof) :
    MvPolynomial (𝓟.Sample) F :=
  (𝓟.ListSRSElements.map fun SRS_elem =>
          MvPolynomial.C (prover.fst pf_elem SRS_elem) * (𝓟.SRSElementValue SRS_elem)).sum

noncomputable def pairing_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx) :
    MvPolynomial 𝓟.Sample F :=
  (
    ( 
      
      (
        (𝓟.ListProof.map fun pf_elem => 
          C (𝓟.verificationPairingProof stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue SRS_elem)).sum
      )
    )
    *
    ( 
      
      (
        (𝓟.ListProof.map fun pf_elem => 
          C (𝓟.verificationPairingProof stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue SRS_elem)).sum
      )
    )
  )

noncomputable def check_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) :
    MvPolynomial 𝓟.Sample F :=
  (
  (𝓟.ListPairings check_idx).map fun pairing =>
    𝓟.pairing_poly prover stmt check_idx pairing
  ).sum

def verify {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) : Prop :=
  (
    ∀ check_idx : 𝓟.EqualityChecks, 𝓟.check_poly prover stmt check_idx = 0
  )
  ∧
  ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
    𝓟.proof_element_as_poly prover pfs.fst = 𝓟.proof_element_as_poly prover pfs.snd

def soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

def completeness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (Wit : Type)
    (relation : 𝓟.Stmt -> Wit -> Prop)
    (prover : 𝓟.Stmt -> Wit -> 𝓟.Prover) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ wit : Wit,
      relation stmt wit -> 𝓟.verify (prover stmt wit) stmt

structure AGMProofSystemInstantiation (F : Type) [Field F] where
  Stmt Sample SRSElements Proof EqualityChecks : Type

  ListSRSElements : List SRSElements
  SRSElementValue : SRSElements → MvPolynomial Sample F
  ListProof : List Proof
  Pairings : EqualityChecks → Type
  ListPairings : (k : EqualityChecks) → List (Pairings k)
  verificationPairingSRS_G1 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
  verificationPairingSRS_G2 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
  verificationPairingProof_G1 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F
  verificationPairingProof_G2 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F

def Prover (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) : Type :=
  (𝓟.Proof -> 𝓟.SRSElements -> F) × (𝓟.Proof -> 𝓟.SRSElements -> F)

def soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

Field in Mathlib.Algebra.Field.Defs

MvPolynomial in Mathlib.Algebra.MvPolynomial.Basic

MvPolynomial.C in Mathlib.Algebra.MvPolynomial.Basic

MvPolynomial.degreeOf in Mathlib.Algebra.MvPolynomial.Degrees

Nat in Init.Prelude

DecidableEq in Init.Prelude

MvPolynomial.X in Mathlib.Algebra.MvPolynomial.Basic

MvPolynomial.monomial in Mathlib.Algebra.MvPolynomial.Basic

Finset in Mathlib.Data.Finset.Defs

Finsupp in Mathlib.Data.Finsupp.Defs

MvPolynomial.coeff in Mathlib.Algebra.MvPolynomial.Basic

Int in Init.Data.Int.Basic

Finset.filter in Mathlib.Data.Finset.Filter

Finsupp.erase in Mathlib.Data.Finsupp.Single

Finsupp.single in Mathlib.Data.Finsupp.Single

MvPolynomial.support in Mathlib.Algebra.MvPolynomial.Basic

Finset.prod in Mathlib.Algebra.BigOperators.Group.Finset.Defs

MvPolynomial.bind₁ in Mathlib.Algebra.MvPolynomial.Monad

Finsupp.prod in Mathlib.Algebra.BigOperators.Finsupp.Basic

AlgHom in Mathlib.Algebra.Algebra.Hom

Algebra in Mathlib.Algebra.Algebra.Defs

CommSemiring in Mathlib.Algebra.Ring.Defs

List in Init.Prelude

List.sum in Init.Data.List.Basic

Semiring in Mathlib.Algebra.Ring.Defs

Option in Init.Prelude

Polynomial in Mathlib.Algebra.Polynomial.Basic

Finsupp.toFun in Mathlib.Data.Finsupp.Defs

Polynomial.eval₂ in Mathlib.Algebra.Polynomial.Eval.Defs

Polynomial.X in Mathlib.Algebra.Polynomial.Basic

Polynomial.C in Mathlib.Algebra.Polynomial.Basic

MvPolynomial.eval₂ in Mathlib.Algebra.MvPolynomial.Eval

algebraMap in Mathlib.Algebra.Algebra.Defs

RingHom in Mathlib.Algebra.Ring.Hom.Defs

RingHom.comp in Mathlib.Algebra.Ring.Hom.Defs

DFunLike in Mathlib.Data.FunLike.Basic

DFunLike.coe in Mathlib.Data.FunLike.Basic

MvPolynomial.optionEquivRight in Mathlib.Algebra.MvPolynomial.Equiv

AlgEquiv in Mathlib.Algebra.Algebra.Equiv

RingEquiv in Mathlib.Algebra.Ring.Equiv

CommRing in Mathlib.Algebra.Ring.Defs

Ideal in Mathlib.RingTheory.Ideal.Defs

Ideal.Quotient.mk in Mathlib.RingTheory.Ideal.Quotient.Defs

Ideal.span in Mathlib.RingTheory.Ideal.Span

BEq in Init.Prelude

Repr in Init.Data.Repr

Fintype in Mathlib.Data.Fintype.Defs

Fin in Init.Prelude

List.finRange in Init.Data.List.FinRange

Unit in Init.Prelude

Bool in Init.Prelude

Lean.Expr in Lean.Expr

Lean.MVarId in Lean.Expr

Lean.Meta.MetaM in Lean.Meta.Basic

Lean.throwError in Lean.Exception

Array in Init.Prelude

Lean.withRef in Init.Prelude

withTheReader in Init.Prelude

Lean.instantiateMVars in Lean.MetavarContext

Lean.Elab.Tactic.Context in Lean.Elab.Tactic.Basic

Lean.Elab.Tactic.State in Lean.Elab.Term.TermElabM

Lean.Elab.Term.Context in Lean.Elab.Term.TermElabM

Lean.Elab.Term.State in Lean.Elab.Term.TermElabM

Lean.Meta.Context in Lean.Meta.Basic

Lean.Meta.State in Lean.Meta.Basic

Lean.Elab.Tactic.TacticM in Lean.Elab.Tactic.Basic

IO in Init.System.IO

IO.mkRef in Init.System.IO

Zero in Init.Prelude

AddCommGroup in Mathlib.Algebra.Group.Defs

Lean.FVarId in Lean.Expr

Lean.Name.str in Init.Prelude

Lean.Syntax in Init.Prelude

Lean.Unhygienic.run in Lean.Hygiene

liftM in Init.Prelude

Empty in Init.Prelude

List.append in Init.Prelude

List.foldl in Init.Prelude

Sum in Init.Core

Finset.univ in Mathlib.Data.Fintype.Defs

inferInstanceAs in Init.Prelude

Function.comp in Init.Prelude

List.replace in Init.Data.List.Basic

List.map in Init.Prelude

EquivLike in Mathlib.Data.FunLike.Equiv
</all_available_defs>

<all_available_lemmas>
lemma zero_ne_succ (n : ℕ) : 0 ≠ nat.succ n

lemma Vars.finsupp_eq_ext (f g : Vars →₀ ℕ) : f = g ↔
    f Vars.r_v = g Vars.r_v
    ∧ f Vars.r_w = g Vars.r_w
    ∧ f Vars.α_v = g Vars.α_v
    ∧ f Vars.α_w = g Vars.α_w
    ∧ f Vars.α_y = g Vars.α_y
    ∧ f Vars.β = g Vars.β
    ∧ f Vars.γ = g Vars.γ

lemma soundness
    {F : Type} [Field F]
    {n_stmt n_wit d : ℕ}
    {v_stmt : Fin n_stmt → Polynomial F }
    {w_stmt : Fin n_stmt → Polynomial F }
    {y_stmt : Fin n_stmt → Polynomial F }
    {v_wit : Fin n_wit → Polynomial F }
    {w_wit : Fin n_wit → Polynomial F }
    {y_wit : Fin n_wit → Polynomial F }
    {v_0 : Polynomial F }
    {w_0 : Polynomial F }
    {y_0 : Polynomial F }
    /- t is the polynomial divisibility by which is used to verify satisfaction of the QAP -/
    {t : Polynomial F}
    (tMonic : t.Monic)
    -- t can also be expressed as follows, but this structure is not important for soundness
    -- {r : Fin (n_wit) → F}
    -- let t : Polynomial F

lemma Vars.finsupp_eq_ext (f g : Vars →₀ ℕ) : f = g ↔
    f Vars.α = g Vars.α
    ∧ f Vars.β_v = g Vars.β_v
    ∧ f Vars.β_w = g Vars.β_w
    ∧ f Vars.β_y = g Vars.β_y
    ∧ f Vars.γ = g Vars.γ

lemma soundness
    {F : Type} [Field F]
    {n_stmt n_wit m d : ℕ}
    {v_stmt : Fin n_stmt → Polynomial F }
    {v_wit : Fin n_wit → Polynomial F }
    {w_wit : Fin m → Polynomial F }
    {v_0 : Polynomial F }
    {w_0 : Polynomial F }
    {r : Fin (n_wit) → F} :
    (AGMProofSystemInstantiation.soundness
      F
      (@GGPR F _ n_stmt n_wit m d
        v_stmt
        v_wit w_wit
        v_0 w_0
        r)
      ((Fin n_wit → F) × (Fin m → F))
      (fun (stmt : Fin n_stmt → F) (wit : (Fin n_wit -> F) × (Fin m → F)) =>
        let t : Polynomial F := ∏ i : Fin n_wit in Finset.univ, (Polynomial.X - Polynomial.C (r i));
        (-- Definition 2 from GGPR
          (v_0
            + (List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit.fst i) * v_wit i) (List.finRange n_wit)))
          )
        *
          (w_0
            + (List.sum (List.map (fun i => Polynomial.C (wit.snd i) * w_wit i) (List.finRange m)))
          )
        )
          %ₘ t = 0)
        ( fun prover =>
           ⟨fun i => prover.snd Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i ) ,
            fun i => prover.snd Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i ) ⟩ )
    )

lemma Vars.finsupp_eq_ext (f g : Vars →₀ ℕ) : f = g ↔
    f Vars.y = g Vars.y

lemma to_MvPolynomial_Option_X {F V : Type} [Field F] :
    to_MvPolynomial_Option V (Polynomial.X) = MvPolynomial.X (R := F) none

lemma to_MvPolynomial_Option_C {F V : Type} [Field F] (r : F) :
    to_MvPolynomial_Option V (Polynomial.C r) = MvPolynomial.C r

@[simp]
theorem MvPolynomial.algHom_eval₂_algebraMap {σ R A B : Type*} [CommSemiring R] [CommSemiring A] [CommSemiring B]
    [Algebra R A] [Algebra R B] (p : MvPolynomial σ R) (f : A →ₐ[R] B) (a : σ -> A) :
    f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f ∘ a) p

theorem Polynomial.hom_congr_vars {R : Type u} {S : Type v}
    [CommSemiring R] [CommSemiring S]
    {f₁ : Polynomial R →+* S} {f₂ : Polynomial R →+* S}
    (hC : RingHom.comp f₁ Polynomial.C = RingHom.comp f₂ Polynomial.C)
    (hv : f₁ (Polynomial.X) = f₂ (Polynomial.X)) :
    f₁ = f₂

lemma optionEquivRight_comp_to_MvPolynomial_Option {F V : Type} [Field F] :
    RingHom.comp (MvPolynomial.optionEquivRight F V).toRingEquiv.toRingHom (to_MvPolynomial_Option (F := F) V) = C

lemma optionEquivRight_to_MvPolynomial_Option {F V : Type} [Field F] (p : Polynomial F) :
    (MvPolynomial.optionEquivRight F V) (to_MvPolynomial_Option V p) = C p

lemma MvPolynomial.sum_map_C {σ A R : Type} [CommSemiring R] (l : List A) (f : A → R) :
    (l.map (fun (x : A) => C (σ := σ) (f x))).sum = C ((l.map f).sum)

theorem AlgEquiv.list_map_sum {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂}
    [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂]
    (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ι → A₁) (l : List ι) :
    e (l.map (fun (x : ι) => f x)).sum = (l.map fun (x : ι) => e (f x)).sum

lemma Polynomial.mul_self_modByMonic {F : Type} [Field F] (t p : Polynomial F) (mt : t.Monic) : (t * p) %ₘ t = 0

lemma soundness
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {r : Fin n_wit → F} :
    (AGMProofSystemInstantiation.soundness
      F
      (Lipmaa
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        let t : Polynomial F :=
          ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit))))
            *
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * v_wit i) (List.finRange n_wit))))
            -
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * w_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * w_wit i) (List.finRange n_wit)))))
            %ₘ t = 0
      )
      (fun prover i => prover.fst Proof_G1_Idx.C (SRS_Elements_G1_Idx.q i))
    )

theorem MvPolynomial.degreeOf_C_mul {σ R : Type} [Field R] (j : σ)
    (c : R) (hc : c ≠ 0) (f : MvPolynomial σ R) :
    MvPolynomial.degreeOf j (MvPolynomial.C c * f) = MvPolynomial.degreeOf j f

lemma MvPolynomial.prod_neq_pow_eq_monomial_erase {σ F : Type} [Field F] [DecidableEq σ]
  (sample_removed : σ)
  (x : σ →₀ ℕ) :
    ((x.support.filter (fun y => ¬y = sample_removed)).prod fun x_1 => X x_1 ^ x x_1)
      =
    (monomial (x.erase sample_removed)) (1 : F)

@[simp]
lemma MvPolynomial.coeff_zero_of_not_mem_support {σ F : Type} [Field F]
    (p : MvPolynomial σ F)
    (m : σ →₀ ℕ)
    (h : m ∉ p.support) :
    coeff m p = 0

lemma mod_cast_eq_cast_mod (a b : ℕ) : ((a : ℤ) % (b : ℤ)) = ((a % b : ℕ): ℤ)

lemma Int.near_mods (a b c d : ℤ) (ha' : 0 ≤ a) (hb' : 0 ≤ b)
    (ha : a < d) (hb : b < d) (habcd : a = b + c * d) :
    c = 0

lemma near_mods (a b d : ℕ) (c : ℤ) (ha : a < d) (hb : b < d) (habcd : a = b + c * d) :
    c = 0

lemma MvPolynomial.bind_ite_filter_aux {σ F : Type} [Field F] [DecidableEq σ]
    (p : MvPolynomial σ F)
    (sample_removed sample_target : σ)
    (hsa : sample_target ≠ sample_removed)
    (d : ℕ) (hd : 0 < d)
    (hdegree: ∀ a ∈ support p, a sample_target < d)
    (m : σ →₀ ℕ)
    (m_sample_target_bound : m sample_target < d) :
    (Finset.filter
      (fun a : σ →₀ ℕ =>
        ((a sample_removed : ℕ) * d ≤ m sample_target + d * m sample_removed )∧
        (Finsupp.erase sample_removed a =
            (Finsupp.erase sample_removed m + Finsupp.single (sample_target) (d * m sample_removed)) -
              Finsupp.single sample_target (a sample_removed * d)))
      (support p))
      =
    (Finset.filter
      (fun a : σ →₀ ℕ => a = m)
      (support p))

lemma MvPolynomial.remove_ite_for_casing {σ F : Type} [Field F] [DecidableEq σ]
    (d : ℕ)
    (sample_removed sample_target : σ)
    (x : σ →₀ ℕ) :
    ((if x sample_removed = 0
      then
        (Finset.prod (Finset.filter (fun y => ¬y = sample_removed) x.support) fun x_1 => X x_1 ^ x x_1 : MvPolynomial σ F)
      else
        (X sample_target ^ d) ^ x sample_removed *
          Finset.prod (Finset.filter (fun x => ¬x = sample_removed) x.support) fun x_1 => X x_1 ^ x x_1)
      =
    ((X sample_target ^ d) ^ x sample_removed *
          Finset.prod (Finset.filter (fun x => ¬x = sample_removed) x.support) fun x_1 => X x_1 ^ x x_1)
    )

lemma MvPolynomial.bind₁_ite_pow_eq_zero_of {σ F : Type} [Field F] [DecidableEq σ]
    (p : MvPolynomial σ F)
    (d : ℕ)  (hd : 0 < d)
    (sample_removed sample_target : σ)
    (hsa : sample_target ≠ sample_removed)
    (h : MvPolynomial.bind₁
          ((fun x => (if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)))
          p = 0)
    (hdegree : p.degreeOf sample_target < d) :
    p = 0

lemma AlgHom.list_map_sum {R : Type u} {A : Type v} {B : Type w}
    [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
    (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : List ι) :
    φ (List.sum (s.map fun (x : ι) => f x)) = List.sum (s.map fun (x : ι) => φ (f x))

lemma is_sound
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {r : Fin n_wit → F} :
    (soundness
      F
      (Groth16TypeIII
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        let t : Polynomial F :=
          ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit))))
            *
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * v_wit i) (List.finRange n_wit))))
            -
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * w_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * w_wit i) (List.finRange n_wit)))))
            %ₘ t = 0
      )
      (fun prover i => prover.fst Proof_G1_Idx.C (SRS_Elements_G1_Idx.q i))
    )

lemma Polynomial.mul_self_modByMonic {F : Type} [Field F] (t p : Polynomial F) (mt : t.Monic) : (t * p) %ₘ t = 0

lemma is_sound_quotient_version
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {t : Polynomial F} :
    (soundness
      F
      (Groth16TypeIII
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (t := t))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit))))
            *
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * v_wit i) (List.finRange n_wit))))
            -
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * w_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * w_wit i) (List.finRange n_wit)))))
            %ₘ t = 0
      )
      (fun prover i => prover.fst Proof_G1_Idx.C (SRS_Elements_G1_Idx.q i))
    )

lemma changeExponent_soundness {𝓟 : AGMProofSystemInstantiation F} (sample : 𝓟.Sample) (d : ℕ)
    (hTypeIII : 𝓟.Identified_Proof_Elems = [])
    (Wit : Type)
    (relation : 𝓟.Stmt -> Wit -> Prop) (extractor : 𝓟.Prover -> Wit)
    (h_sound : 𝓟.soundness F Wit relation extractor ) :
    (changeExponent_G1 𝓟 sample d).soundness F Wit relation extractor

lemma collapseSRSElement_G1_soundness (𝓟 : AGMProofSystemInstantiation F)
    (hTypeIII : 𝓟.Identified_Proof_Elems = [])
    [DecidableEq 𝓟.SRSElements_G1] (twin1 twin2 : 𝓟.SRSElements_G1) (not_same : twin1 ≠ twin2)
    (hcount1 : 𝓟.ListSRSElements_G1.count twin1 = 1)
    (hcount2 : 𝓟.ListSRSElements_G1.count twin2 = 1)
    (interchangeable :
      ∀ (idx : 𝓟.Proof_G1)
        (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F),
        agm idx twin1 = agm idx twin2)
    (interchangeable' : ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),  𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2 )
    (Wit : Type)
    (relation : 𝓟.Stmt -> Wit -> Prop) (extractor : 𝓟.Prover -> Wit)
    (h_sound : 𝓟.soundness F Wit relation extractor) :
    (collapseSRSElement_G1 𝓟 twin1 twin2).soundness F Wit relation extractor

lemma Vars.finsupp_eq_ext (f g : Vars →₀ ℕ) : f = g ↔
    f Vars.β = g Vars.β
    ∧ f Vars.γ = g Vars.γ

lemma identified_proof_elems_def
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {t : Polynomial F} :
    (BabySNARK
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (t := t)).Identified_Proof_Elems = [(Proof_Idx.H, Proof_Idx.H), (Proof_Idx.V, Proof_Idx.V), (Proof_Idx.B, Proof_Idx.B)]

lemma is_sound
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {t : Polynomial F}
    (ht : List.sum (List.map (fun (x : Fin n_var) => Polynomial.C (Polynomial.coeff t (x : ℕ)) * Polynomial.X ^ (x : ℕ)) (List.finRange n_var)) = t)
    (ht0 : t.Monic) :
    (soundness
      F
      (BabySNARK
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (t := t))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit)))) ^ 2
          - 1
        )
            %ₘ t = 0
      )
      (fun prover i => prover.fst Proof_Idx.B (SRS_Elements_Idx.βu i))
    )

    )

lemma identified_proof_elems_def
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {r : Fin n_wit → F} :
    (Groth16TypeI
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r)).Identified_Proof_Elems = [(Proof_Idx.A, Proof_Idx.A), (Proof_Idx.B, Proof_Idx.B), (Proof_Idx.C, Proof_Idx.C)]

lemma is_sound
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {r : Fin n_wit → F} :
    (soundness
      F
      (Groth16TypeI
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        let t : Polynomial F :=
          ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit))))
            *
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * v_wit i) (List.finRange n_wit))))
            -
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * w_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * w_wit i) (List.finRange n_wit)))))
            %ₘ t = 0
      )
      (fun prover i => prover.fst Proof_Idx.C (SRS_Elements_Idx.q i))
    )

@[simp] lemma eq_zero_of_zero_eq (R : Type u) [Zero R] (r : R) : 0 = r ↔ r = 0

@[simp] lemma zero_sub_eq_iff (R : Type u) [AddCommGroup R] (a b : R) : 0 - a = b ↔ a + b = 0

@[simp]
lemma Polynomial.quotient_singleton_eq {R : Type*} [CommRing R] (p : Polynomial R) : (Ideal.Quotient.mk (Ideal.span {p})) p = 0

lemma RingHom.list_map_sum {A : Type v} {B : Type w}
    [Semiring A] [Semiring B]
    (φ : A →+* B) {ι : Type u_1} (f : ι → A) (s : List ι) :
    φ (List.sum (s.map fun (x : ι) => f x)) = List.sum (s.map fun (x : ι) => φ (f x))
</all_available_lemmas>

<local_ctx>
import FormalSnarksProject.Models.AGMProofSystemInstantiation

import Mathlib.Algebra.Polynomial.Div

import FormalSnarksProject.ToMathlib.OptionEquivRight

import Mathlib.Algebra.MvPolynomial.Equiv

import FormalSnarksProject.SoundnessTactic.SoundnessProver

open scoped BigOperators Classical

section ToySnark

open MvPolynomial Option List

namespace ToySnark

inductive Vars : Type where
  | α : Vars
  | β : Vars
deriving Repr, BEq

inductive StmtEntries : Type where
  | x : StmtEntries
  | y : StmtEntries
  | z : StmtEntries
deriving Repr, BEq

inductive WitEntries : Type where
  | A : WitEntries
  | B : WitEntries
deriving Repr, BEq

local notation "Vars_α" => some Vars.α
local notation "Vars_β" => some Vars.β
local notation "Vars_x" => none

inductive Proof_G1_Idx : Type where
  | Pf : Proof_G1_Idx

def Proof_G2_Idx : Type := Empty

inductive PairingsIdx : Type where
  | lhs : PairingsIdx
  | rhs : PairingsIdx

inductive SRS_Elements_G2_Idx : Type where
  | α : SRS_Elements_G2_Idx
  | β : SRS_Elements_G2_Idx

noncomputable def ToySnark
     
    {F : Type} [Field F] :
    AGMProofSystemInstantiation F :=
  {
    Stmt := StmtEntries -> F
    Sample := Option Vars
    SRSElements_G1 := SRS_Elements_G1_Idx
    ListSRSElements_G1 :=
      [.α, .β]
    SRSElements_G2 := SRS_Elements_G2_Idx
    ListSRSElements_G2 :=
      [.α, .β]
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G1_Idx.α => MvPolynomial.X Vars_α
      | SRS_Elements_G1_Idx.β => MvPolynomial.X Vars_β
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G2_Idx.α => MvPolynomial.X Vars_α
      | SRS_Elements_G2_Idx.β => MvPolynomial.X Vars_β
    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.Pf]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := []
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.lhs, PairingsIdx.rhs]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.lhs => 0
      | PairingsIdx.rhs => match SRS_idx with
        | SRS_Elements_G1_Idx.α => stmt StmtEntries.z
        | SRS_Elements_G1_Idx.β => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.lhs => match SRS_idx with
        | SRS_Elements_G2_Idx.α => stmt StmtEntries.x
        | SRS_Elements_G2_Idx.β => stmt StmtEntries.y
      | PairingsIdx.rhs => match SRS_idx with
        | SRS_Elements_G2_Idx.α => 0
        | SRS_Elements_G2_Idx.β => -1
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.lhs => match pf with
        | Proof_G1_Idx.Pf => 1
      | PairingsIdx.rhs => match pf with
        | Proof_G1_Idx.Pf => 0
    verificationPairingProof_G2 := fun stmt _ i pf => 0
  }

section soundness
</local_ctx>

<target_theorem>
lemma soundness
    {F : Type} [Field F] :
    (AGMProofSystemInstantiation.soundness
      F
      (ToySnark
        (F := F))
      (WitEntries -> F)
      (fun (stmt : StmtEntries → F) (wit : WitEntries -> F) =>
        wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z -- - wit WitEntries.I
        ∨
        wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z -- - wit WitEntries.I
      )
      (fun prover i => prover.fst Proof_G1_Idx.Pf (if i = WitEntries.A then .α else .β))

    ) :=
</target_theorem>

