Theorem: Lipmaa.soundness
Proof state before:
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
Tactic:
polyrith
Proof state after:
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