Theorem: BabySNARK.is_sound
Proof state before:
case intro.intro.intro.inr
F : Type
inst✝ : 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
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
ht : (List.map (fun x => Polynomial.C (Polynomial.coeff 0 ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = 0
ht0 : Polynomial.Monic 0
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    -(-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)))
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hII_22 : Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_11 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ)
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_11 : Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hI_10 :
  -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) =
    -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum +
        (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum)
hV_00 : sum_V_1_τ_pow = 0
hI_00 :
  (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
      (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum =
    -((List.map
            (fun x =>
              Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                Polynomial.X ^ ↑x)
            (List.finRange n_var)).sum *
        (List.map
            (fun x =>
              -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x))
            (List.finRange n_var)).sum)
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
hI_11 : t = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    0
Tactic:
simp [ht, Polynomial.Monic.ne_zero ht0] at *
Proof state after:
no goals