internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f.h.e_a
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ ∏ x_1 ∈ x.support, f ((fun n e => a n ^ e) x_1 (x x_1)) = ∏ a_1 ∈ x.support, (fun n e => f (a n) ^ e) a_1 (x a_1)
Tactic:
congr
Proof state after:
case e_f.h.e_a.e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (fun x_1 => f ((fun n e => a n ^ e) x_1 (x x_1))) = fun a_1 => (fun n e => f (a n) ^ e) a_1 (x a_1)
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f.h.e_a.e_f
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
⊢ (fun x_1 => f ((fun n e => a n ^ e) x_1 (x x_1))) = fun a_1 => (fun n e => f (a n) ^ e) a_1 (x a_1)
Tactic:
ext x1
Proof state after:
case e_f.h.e_a.e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
x1 : σ
⊢ f ((fun n e => a n ^ e) x1 (x x1)) = (fun n e => f (a n) ^ e) x1 (x x1)
Theorem: MvPolynomial.algHom_eval₂_algebraMap
Proof state before:
case e_f.h.e_a.e_f.h
σ : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : MvPolynomial σ R
f : A →ₐ[R] B
a : σ → A
x : σ →₀ ℕ
x1 : σ
⊢ f ((fun n e => a n ^ e) x1 (x x1)) = (fun n e => f (a n) ^ e) x1 (x x1)
Tactic:
simp
Proof state after:
no goals
Theorem: Polynomial.hom_congr_vars
Proof state before:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ = f₂
Tactic:
ext p
Proof state after:
case h₁.a
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
p : R
⊢ (f₁.comp C) p = (f₂.comp C) p

case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X
Theorem: Polynomial.hom_congr_vars
Proof state before:
case h₁.a
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
p : R
⊢ (f₁.comp C) p = (f₂.comp C) p

case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X
Tactic:
exact congrFun (congrArg DFunLike.coe hC) p
Proof state after:
case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X
Theorem: Polynomial.hom_congr_vars
Proof state before:
case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X
Tactic:
exact hv
Proof state after:
no goals
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V) = C
Tactic:
apply Polynomial.hom_congr_vars
Proof state after:
case hC
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C

case hv
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) Polynomial.X = C Polynomial.X
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hC
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom]
Proof state after:
case hC
F V : Type
inst✝ : Field F
⊢ ((↑(optionEquivRight F V)).comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hC
F V : Type
inst✝ : Field F
⊢ ((↑(optionEquivRight F V)).comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C
Tactic:
rw [RingHom.comp_assoc]
Proof state after:
case hC
F V : Type
inst✝ : Field F
⊢ (↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C) = C.comp Polynomial.C
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hC
F V : Type
inst✝ : Field F
⊢ (↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C) = C.comp Polynomial.C
Tactic:
rw [@RingHom.ext_iff]
Proof state after:
case hC
F V : Type
inst✝ : Field F
⊢ ∀ (x : F), ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hC
F V : Type
inst✝ : Field F
⊢ ∀ (x : F), ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x
Tactic:
intro x
Proof state after:
case hC
F V : Type
inst✝ : Field F
x : F
⊢ ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hC
F V : Type
inst✝ : Field F
x : F
⊢ ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x
Tactic:
simp [to_MvPolynomial_Option_C]
Proof state after:
no goals
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hv
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) Polynomial.X = C Polynomial.X
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe,
  AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]
Proof state after:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) Polynomial.X) = C Polynomial.X
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) Polynomial.X) = C Polynomial.X
Tactic:
rw [to_MvPolynomial_Option_X]
Proof state after:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) (X none) = C Polynomial.X
Theorem: optionEquivRight_comp_to_MvPolynomial_Option
Proof state before:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) (X none) = C Polynomial.X
Tactic:
simp only [MvPolynomial.optionEquivRight_X_none]
Proof state after:
no goals
Theorem: optionEquivRight_to_MvPolynomial_Option
Proof state before:
F V : Type
inst✝ : Field F
p : Polynomial F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) p) = C p
Tactic:
rw [<-DFunLike.congr_fun optionEquivRight_comp_to_MvPolynomial_Option p]
Proof state after:
F V : Type
inst✝ : Field F
p : Polynomial F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) p) =
    ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) p
Theorem: optionEquivRight_to_MvPolynomial_Option
Proof state before:
F V : Type
inst✝ : Field F
p : Polynomial F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) p) =
    ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) p
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.sum_map_C
Proof state before:
σ A R : Type
inst✝ : CommSemiring R
l : List A
f : A → R
⊢ (List.map (fun x => C (f x)) l).sum = C (List.map f l).sum
Tactic:
induction l with
| nil => simp
| cons hd tl ih => simp [ih]
Proof state after:
no goals
Theorem: MvPolynomial.sum_map_C
Proof state before:
case nil
σ A R : Type
inst✝ : CommSemiring R
f : A → R
⊢ (List.map (fun x => C (f x)) []).sum = C (List.map f []).sum
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.sum_map_C
Proof state before:
case cons
σ A R : Type
inst✝ : CommSemiring R
f : A → R
hd : A
tl : List A
ih : (List.map (fun x => C (f x)) tl).sum = C (List.map f tl).sum
⊢ (List.map (fun x => C (f x)) (hd :: tl)).sum = C (List.map f (hd :: tl)).sum
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: AlgEquiv.list_map_sum
Proof state before:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
f : ι → A₁
l : List ι
⊢ e (List.map (fun x => f x) l).sum = (List.map (fun x => e (f x)) l).sum
Tactic:
induction l with
| nil => simp
| cons hd tl ih => simp [ih]
Proof state after:
no goals
Theorem: AlgEquiv.list_map_sum
Proof state before:
case nil
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
f : ι → A₁
⊢ e (List.map (fun x => f x) []).sum = (List.map (fun x => e (f x)) []).sum
Tactic:
simp
Proof state after:
no goals
Theorem: AlgEquiv.list_map_sum
Proof state before:
case cons
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
f : ι → A₁
hd : ι
tl : List ι
ih : e (List.map (fun x => f x) tl).sum = (List.map (fun x => e (f x)) tl).sum
⊢ e (List.map (fun x => f x) (hd :: tl)).sum = (List.map (fun x => e (f x)) (hd :: tl)).sum
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: ToySnark.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ f = g ↔ f α = g α ∧ f β = g β
Tactic:
rw [DFunLike.ext_iff]
Proof state after:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f α = g α ∧ f β = g β
Theorem: ToySnark.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f α = g α ∧ f β = g β
Tactic:
constructor
Proof state after:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β = g β

case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β → ∀ (x : Vars), f x = g x
Theorem: ToySnark.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β = g β
Tactic:
intro h
Proof state after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β = g β
Theorem: ToySnark.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β = g β
Tactic:
simp_rw [h]
Proof state after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True
Theorem: ToySnark.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True
Tactic:
simp only [and_self]
Proof state after:
no goals
Theorem: ToySnark.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β → ∀ (x : Vars), f x = g x
Tactic:
intro h x
Proof state after:
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β = g β
x : Vars
⊢ f x = g x
Theorem: ToySnark.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β = g β
x : Vars
⊢ f x = g x
Tactic:
cases x <;> tauto
Proof state after:
no goals
Theorem: ToySnark.soundness
Proof state before:
F : Type
inst✝ : Field F
⊢ AGMProofSystemInstantiation.soundness F ToySnark (WitEntries → F)
    (fun stmt wit =>
      wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
        wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
    fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β)
Tactic:
unfold AGMProofSystemInstantiation.soundness AGMProofSystemInstantiation.verify AGMProofSystemInstantiation.proof_element_G1_as_poly AGMProofSystemInstantiation.proof_element_G2_as_poly
Proof state after:
F : Type
inst✝ : Field F
⊢ ∀ (stmt : ToySnark.Stmt) (prover : AGMProofSystemInstantiation.Prover F ToySnark),
    ((∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
                ToySnark.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
                ToySnark.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
            wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
        stmt
        ((fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover)
Theorem: ToySnark.soundness
Proof state before:
F : Type
inst✝ : Field F
⊢ ∀ (stmt : ToySnark.Stmt) (prover : AGMProofSystemInstantiation.Prover F ToySnark),
    ((∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
                ToySnark.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
                ToySnark.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
            wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
        stmt
        ((fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover)
Tactic:
intros stmt prover eqns'
Proof state after:
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns' :
  (∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
    ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
      (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
            ToySnark.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
            ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Theorem: ToySnark.soundness
Proof state before:
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns' :
  (∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
    ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
      (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
            ToySnark.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
            ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
rcases eqns' with ⟨eqns, null⟩
Proof state after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Theorem: ToySnark.soundness
Proof state before:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
have eqn := eqns ()
Proof state after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Theorem: ToySnark.soundness
Proof state before:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
clear eqns null
Proof state after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Theorem: ToySnark.soundness
Proof state before:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
simp_rw [ToySnark] at eqn
Proof state after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqn :
  { Stmt := StmtEntries → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_G1_Idx,
          ListSRSElements_G1 := [SRS_Elements_G1_Idx.α, SRS_Elements_G1_Idx.β], SRSElements_G2 := SRS_Elements_G2_Idx,
          ListSRSElements_G2 := [SRS_Elements_G2_Idx.α, SRS_Elements_G2_Idx.β],
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_G1_Idx.α => X Vars_α
            | SRS_Elements_G1_Idx.β => X Vars_β,
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_G2_Idx.α => X Vars_α
            | SRS_Elements_G2_Idx.β => X Vars_β,
          Proof_G1 := Proof_G1_Idx, ListProof_G1 := [Proof_G1_Idx.Pf], Proof_G2 := Proof_G2_Idx, ListProof_G2 := [],
          EqualityChecks := Unit, Pairings := fun x => PairingsIdx,
          ListPairings := fun x => [PairingsIdx.lhs, PairingsIdx.rhs],
          verificationPairingSRS_G1 := fun stmt x 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 x 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 x i pf =>
            match i with
            | PairingsIdx.lhs => 1
            | PairingsIdx.rhs => 0,
          verificationPairingProof_G2 := fun stmt x i pf => 0, Identified_Proof_Elems := [] }.check_poly
      prover stmt () =
    0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Theorem: Lipmaa.Polynomial.mul_self_modByMonic
Proof state before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ (t * p).modByMonic t = 0
Tactic:
rw [Polynomial.dvd_iff_modByMonic_eq_zero]
Proof state after:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t ∣ t * p

F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic