internlm/Lean-Github huggingface dataset:
Theorem: Lipmaa.Polynomial.mul_self_modByMonic
Proof state before:
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
Tactic:
apply dvd_mul_right
Proof state after:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Theorem: Lipmaa.Polynomial.mul_self_modByMonic
Proof state before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Tactic:
exact mt
Proof state after:
no goals
Theorem: Lipmaa.soundness
Proof state before:
case mt.hs
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))
eqn :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    C (Lipmaa.verificationPairingProof_G1 stmt () pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.1 pf_elem SRS_elem) * Lipmaa.SRSElementValue_G1 SRS_elem)
                          Lipmaa.ListSRSElements_G1).sum)
                  Lipmaa.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    C (Lipmaa.verificationPairingSRS_G1 stmt () pairing SRS_elem) * Lipmaa.SRSElementValue_G1 SRS_elem)
                  Lipmaa.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    C (Lipmaa.verificationPairingProof_G2 stmt () pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.2 pf_elem SRS_elem) * Lipmaa.SRSElementValue_G2 SRS_elem)
                          Lipmaa.ListSRSElements_G2).sum)
                  Lipmaa.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    C (Lipmaa.verificationPairingSRS_G2 stmt () pairing SRS_elem) * Lipmaa.SRSElementValue_G2 SRS_elem)
                  Lipmaa.ListSRSElements_G2).sum))
        (Lipmaa.ListPairings ())).sum =
    0
i : Fin n_wit
hi : i ∈ Finset.univ
⊢ (Polynomial.X - Polynomial.C (r i)).Monic
Tactic:
exact Polynomial.monic_X_sub_C (r i)
Proof state after:
no goals
Theorem: Groth16TypeI.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ f = g ↔ f α = g α ∧ 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 β ∧ f γ = g γ ∧ f δ = g δ
Theorem: Groth16TypeI.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
Tactic:
constructor
Proof state after:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ

case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ → ∀ (x : Vars), f x = g x
Theorem: Groth16TypeI.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β = g β ∧ 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 β ∧ f γ = g γ ∧ f δ = g δ
Theorem: Groth16TypeI.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β = g β ∧ 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 ∧ True ∧ True
Theorem: Groth16TypeI.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True ∧ True ∧ True
Tactic:
simp only [and_self]
Proof state after:
no goals
Theorem: Groth16TypeI.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β ∧ 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 β ∧ f γ = g γ ∧ f δ = g δ
x : Vars
⊢ f x = g x
Theorem: Groth16TypeI.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
x : Vars
⊢ f x = g x
Tactic:
cases x <;> tauto
Proof state after:
no goals
Theorem: eq_zero_of_zero_eq
Proof state before:
R : Type u
inst✝ : Zero R
r : R
⊢ 0 = r ↔ r = 0
Tactic:
exact eq_comm
Proof state after:
no goals
Theorem: zero_sub_eq_iff
Proof state before:
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ 0 - a = b ↔ a + b = 0
Tactic:
constructor
Proof state after:
case mp
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ 0 - a = b → a + b = 0

case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ a + b = 0 → 0 - a = b
Theorem: zero_sub_eq_iff
Proof state before:
case mp
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ 0 - a = b → a + b = 0
Tactic:
aesop?
Proof state after:
no goals
Theorem: zero_sub_eq_iff
Proof state before:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ a + b = 0 → 0 - a = b
Tactic:
intro h
Proof state after:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ 0 - a = b
Theorem: zero_sub_eq_iff
Proof state before:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ 0 - a = b
Tactic:
rw [← add_right_inj a]
Proof state after:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ a + (0 - a) = a + b
Theorem: zero_sub_eq_iff
Proof state before:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ a + (0 - a) = a + b
Tactic:
simp [h]
Proof state after:
no goals
Theorem: BabySNARK.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: BabySNARK.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: BabySNARK.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: BabySNARK.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: BabySNARK.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: BabySNARK.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: BabySNARK.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: Groth16TypeIII.is_sound
Proof state before:
case hq.hs
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 : Groth16TypeIII.Stmt
prover : Prover F Groth16TypeIII
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqn :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    C (Groth16TypeIII.verificationPairingProof_G1 stmt () pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => C (prover.1 pf_elem SRS_elem) * Groth16TypeIII.SRSElementValue_G1 SRS_elem)
                          Groth16TypeIII.ListSRSElements_G1).sum)
                  Groth16TypeIII.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    C (Groth16TypeIII.verificationPairingSRS_G1 stmt () pairing SRS_elem) *
                      Groth16TypeIII.SRSElementValue_G1 SRS_elem)
                  Groth16TypeIII.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    C (Groth16TypeIII.verificationPairingProof_G2 stmt () pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => C (prover.2 pf_elem SRS_elem) * Groth16TypeIII.SRSElementValue_G2 SRS_elem)
                          Groth16TypeIII.ListSRSElements_G2).sum)
                  Groth16TypeIII.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    C (Groth16TypeIII.verificationPairingSRS_G2 stmt () pairing SRS_elem) *
                      Groth16TypeIII.SRSElementValue_G2 SRS_elem)
                  Groth16TypeIII.ListSRSElements_G2).sum))
        (Groth16TypeIII.ListPairings ())).sum =
    0
i : Fin n_wit
hi : i ∈ Finset.univ
⊢ (Polynomial.X - Polynomial.C (r i)).Monic
Tactic:
exact Polynomial.monic_X_sub_C (r i)
Proof state after:
no goals
Theorem: changeExponent_soundness
Proof state before:
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
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 (changeExponent_G1 𝓟 sample d) Wit relation extractor
Tactic:
intros stmt agm checks_pass
Proof state after:
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
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 : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
checks_pass : (changeExponent_G1 𝓟 sample d).verify agm stmt
⊢ relation stmt (extractor agm)
Theorem: changeExponent_soundness
Proof state before:
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
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 : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
checks_pass : (changeExponent_G1 𝓟 sample d).verify agm stmt
⊢ relation stmt (extractor agm)
Tactic:
rcases checks_pass with ⟨poly_checks_pass, _⟩
Proof state after:
case intro
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
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 : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)
Theorem: changeExponent_soundness
Proof state before:
case intro
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
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 : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).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
sample : 𝓟.Sample
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 : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Theorem: changeExponent_soundness
Proof state before:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
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 : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Tactic:
clear h_sound
Proof state after:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Theorem: changeExponent_soundness
Proof state before:
case intro.a.left.inl
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass : MvPolynomial.X sample ^ d = 0
⊢ False
Tactic:
simp only [pow_eq_zero_iff', MvPolynomial.X_ne_zero, ne_eq, false_and] at poly_checks_pass
Proof state after:
no goals
Theorem: collapseSRSElement_G1_soundness
Proof state before:
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
⊢ AGMProofSystemInstantiation.soundness F (collapseSRSElement_G1 𝓟 twin1 twin2) Wit relation extractor
Tactic:
intros stmt agm checks_pass
Proof state after:
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)
checks_pass : (collapseSRSElement_G1 𝓟 twin1 twin2).verify agm stmt
⊢ relation stmt (extractor agm)
Theorem: collapseSRSElement_G1_soundness
Proof state before:
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)
checks_pass : (collapseSRSElement_G1 𝓟 twin1 twin2).verify agm stmt
⊢ relation stmt (extractor agm)
Tactic:
rcases checks_pass with ⟨poly_checks_pass, null⟩
Proof state after:
case intro
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
⊢ relation stmt (extractor agm)
Theorem: collapseSRSElement_G1_soundness
Proof state before:
case intro
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
⊢ relation stmt (extractor agm)
Tactic:
apply h_sound
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
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