Theorem: BabySNARK.is_sound
Proof state before:
case intro.intro.intro.inl
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
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
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
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.γβ) = 0
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 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -(-((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 :
  sum_H_2_τ_pow * t + t * t =
    -((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 : Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ) = 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 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
Tactic:
simp [ht, Polynomial.Monic.ne_zero ht0] at *
Proof state after:
case intro.intro.intro.inl
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
ht0 : t.Monic
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
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
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
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
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
hV_00 : sum_V_1_τ_pow = 0
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
ht : True
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) =
    (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.γ) +
      Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    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
hII_22 : prover.2 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hH_11 : prover.1 Proof_Idx.H SRS_Elements_Idx.γβ = 0
hV_11 : 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 =
    0
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    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
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -((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) +
        -(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 (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.γ) +
        (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)
hI_00 :
  sum_H_2_τ_pow * t + t * t =
    -((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) +
      -((List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum *
          (List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum)
hI_11 : prover.2 Proof_Idx.H SRS_Elements_Idx.γβ = 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 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum