Theorem: Lipmaa.soundness
Proof state before:
case intro
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
r : Fin n_wit → F
stmt : Lipmaa.Stmt
prover : Prover F Lipmaa
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
sum_C_x_t sum_C_w_wit sum_C_v_wit sum_C_u_wit C_3 C_2 C_1 sum_B_x B_3 B_2 B_1 sum_A_x_t sum_A_w_wit : Polynomial F
h0021 : -(sum_A_x_t * sum_B_x) + -(sum_A_w_wit * sum_B_x) = 0
sum_A_v_wit : Polynomial F
h1121 : -(sum_A_v_wit * B_1) = 0
sum_A_u_wit : Polynomial F
h0221 : -(sum_A_u_wit * B_1) = 0
h0121 : -(sum_A_u_wit * sum_B_x) + (-(sum_A_x_t * B_1) + -(sum_A_w_wit * B_1)) = 0
sum_A_w_stmt : Polynomial F
h0012 : -(sum_A_w_stmt * sum_B_x) = 0
sum_A_v_stmt : Polynomial F
h1112 : -(sum_A_v_stmt * B_1) = 0
sum_A_u_stmt : Polynomial F
h0212 : -(sum_A_u_stmt * B_1) = 0
h0112 : -(sum_A_u_stmt * sum_B_x) + -(sum_A_w_stmt * B_1) = 0
sum_A_x A_3 A_2 : Polynomial F
h0222 : -(A_2 * B_1) = 0
A_1 : Polynomial F
h1122 : -(A_1 * B_1) + 1 = 0
sum_w_stmt : Polynomial F
h0022 :
  -(sum_A_x * sum_B_x) + (-(sum_A_x_t * B_3) + -(sum_A_w_wit * B_3)) + -(sum_A_w_stmt * B_2) +
      (sum_w_stmt + (sum_C_x_t + sum_C_w_wit)) =
    0
sum_v_stmt : Polynomial F
h1022 : -(A_1 * sum_B_x) + -(sum_A_v_wit * B_3) + -(sum_A_v_stmt * B_2) + (sum_v_stmt + sum_C_v_wit) = 0
sum_u_stmt : Polynomial F
h0122 :
  -(A_2 * sum_B_x) + -(sum_A_u_wit * B_3) + -(sum_A_u_stmt * B_2) + -(sum_A_x * B_1) + (sum_u_stmt + sum_C_u_wit) = 0
⊢ (sum_u_stmt + sum_C_u_wit) * (sum_v_stmt + sum_C_v_wit) = sum_w_stmt + sum_C_w_wit + sum_C_x_t
Tactic:
integral_domain_tactic
Proof state after:
case intro.inl.inl.inl.inl.inl.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
r : Fin n_wit → F
stmt : Lipmaa.Stmt
prover : Prover F Lipmaa
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
sum_C_x_t sum_C_w_wit sum_C_v_wit sum_C_u_wit C_3 C_2 C_1 sum_B_x B_3 B_2 B_1 sum_A_x_t sum_A_w_wit sum_A_v_wit sum_A_u_wit sum_A_w_stmt sum_A_v_stmt sum_A_u_stmt sum_A_x A_3 A_2 A_1 sum_w_stmt sum_v_stmt sum_u_stmt :
  Polynomial F
h0021 : -(sum_A_x_t * sum_B_x) = - -(sum_A_w_wit * sum_B_x)
h0121 : -(sum_A_x_t * B_1) = - -(sum_A_w_wit * B_1)
h1122 : -(A_1 * B_1) = -1
h0022 : -(sum_A_x * sum_B_x) + (-(sum_A_x_t * B_3) + -(sum_A_w_wit * B_3)) = -(sum_w_stmt + (sum_C_x_t + sum_C_w_wit))
h1022 : -(A_1 * sum_B_x) = -(sum_v_stmt + sum_C_v_wit)
h0122 : -(sum_A_x * B_1) = -(sum_u_stmt + sum_C_u_wit)
h1121 : sum_A_v_wit = 0
h0221 : sum_A_u_wit = 0
h0012 : sum_A_w_stmt = 0
h1112 : sum_A_v_stmt = 0
h0212 : sum_A_u_stmt = 0
h0222 : A_2 = 0
⊢ (sum_u_stmt + sum_C_u_wit) * (sum_v_stmt + sum_C_v_wit) = sum_w_stmt + sum_C_w_wit + sum_C_x_t

case intro.inl.inl.inr.inl.inl.inl.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
r : Fin n_wit → F
stmt : Lipmaa.Stmt
prover : Prover F Lipmaa
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
sum_C_x_t sum_C_w_wit sum_C_v_wit sum_C_u_wit C_3 C_2 C_1 sum_B_x B_3 B_2 B_1 sum_A_x_t sum_A_w_wit sum_A_v_wit sum_A_u_wit sum_A_w_stmt sum_A_v_stmt sum_A_u_stmt sum_A_x A_3 A_2 A_1 sum_w_stmt sum_v_stmt sum_u_stmt :
  Polynomial F
h0121 : -(sum_A_x_t * B_1) = - -(sum_A_w_wit * B_1)
h1122 : -(A_1 * B_1) = -1
h0022 : -(sum_A_x_t * B_3) + -(sum_A_w_wit * B_3) = -(sum_w_stmt + (sum_C_x_t + sum_C_w_wit))
h1022 : sum_v_stmt = -sum_C_v_wit
h0122 : -(sum_A_x * B_1) = -(sum_u_stmt + sum_C_u_wit)
h1121 : sum_A_v_wit = 0
h0221 : sum_A_u_wit = 0
h0012 : sum_B_x = 0
h1112 : sum_A_v_stmt = 0
h0212 : sum_A_u_stmt = 0
h0112 : sum_A_w_stmt = 0
h0222 : A_2 = 0
⊢ (sum_u_stmt + sum_C_u_wit) * (-sum_C_v_wit + sum_C_v_wit) = sum_w_stmt + sum_C_w_wit + sum_C_x_t