internlm/Lean-Github huggingface dataset:
Theorem: collapseSRSElement_G1_soundness
Proof state before:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
null :
  ∀ pfs ∈ (collapseSRSElement_G1 𝓟 twin1 twin2).Identified_Proof_Elems,
    (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G1_as_poly agm pfs.1 =
      (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Tactic:
clear h_sound null
Proof state after:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
⊢ 𝓟.verify agm stmt
Theorem: collapseSRSElement_G1_soundness
Proof state before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum
Tactic:
replace interchangeable := interchangeable proof_elem agm.1
Proof state after:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum
Theorem: collapseSRSElement_G1_soundness
Proof state before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (agm.1 proof_elem twin2) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
        MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
ring
Proof state after:
no goals
Theorem: collapseSRSElement_G1_soundness
Proof state before:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin1 +
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2 -
        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
ring
Proof state after:
no goals
Theorem: collapseToxicWaste_check_poly
Proof state before:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
⊢ ∀ (agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target))
    (stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt)
    (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
      (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
        (𝓟.check_poly agm stmt check_idx)
Tactic:
intros agm stmt check_idx
Proof state after:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks
⊢ (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
Theorem: collapseToxicWaste_soundness
Proof state before:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
⊢ AGMProofSystemInstantiation.soundness F (collapseToxicWaste 𝓟 d sample_removed sample_target) Wit relation extractor
Tactic:
intros stmt agm checks_pass
Proof state after:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).verify agm stmt
⊢ relation stmt (extractor agm)
Theorem: collapseToxicWaste_soundness
Proof state before:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).verify agm stmt
⊢ relation stmt (extractor agm)
Tactic:
rcases checks_pass with ⟨poly_checks_pass, proof_elem_checks_pass⟩
Proof state after:
case intro
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)
Theorem: collapseToxicWaste_soundness
Proof state before:
case intro
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)
Tactic:
apply h_sound
Proof state after:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Theorem: collapseToxicWaste_soundness
Proof state before:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Tactic:
clear h_sound proof_elem_checks_pass
Proof state after:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ 𝓟.verify agm stmt
Theorem: collapseToxicWaste_soundness
Proof state before:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ 𝓟.verify agm stmt
Tactic:
unfold AGMProofSystemInstantiation.verify
Proof state after:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ (∀ (check_idx : 𝓟.EqualityChecks), 𝓟.check_poly agm stmt check_idx = 0) ∧
    ∀ pfs ∈ 𝓟.Identified_Proof_Elems, 𝓟.proof_element_G1_as_poly agm pfs.1 = 𝓟.proof_element_G2_as_poly agm pfs.2
Theorem: collapseToxicWaste_soundness
Proof state before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ ∀ (check_idx : 𝓟.EqualityChecks), 𝓟.check_poly agm stmt check_idx = 0
Tactic:
intro check_idx
Proof state after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
check_idx : 𝓟.EqualityChecks
⊢ 𝓟.check_poly agm stmt check_idx = 0