Schnorr Group

Stream: new members

[Mukesh Tiwari]

Hi everyone, I am trying to prove a simple theorem about Schnorr group ( https://en.wikipedia.org/wiki/Schnorr_group ), but getting some typeclass synthesis error for hypothesis Hh1 Hh2 Hg.

import data.zmod.basic data.nat.prime
  data.zmod.quadratic_reciprocity

namespace ElGamal

/-
A Schnorr group is a large prime-order subgroup of ℤ∗𝑝,
the multiplicative group of integers modulo 𝑝.
To generate such a group, we find 𝑝=𝑞𝑟+1 such that 𝑝 and 𝑞
are prime. Then, we choose any ℎ
in the range 1<ℎ<𝑝 such that ℎ^r ≠ 1 (mod𝑝)
The value 𝑔=ℎ^𝑟(mod𝑝) is a generator of a subgroup ℤ∗𝑝 of order 𝑞.
By Fermat's little theorem
g^q = h^(rq) = h^(p-1) = 1 (mod p)
-/

variables
  (p : ℕ) (q : ℕ) (r : ℕ+)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hh₁ : 1 < h < p)
  (Hh₂ : h^r ≠ 1)
  (g : zmodp p Hp) /- generator of a subgroup of ℤ⋆p of order q -/
  (Hg : g = h^r)

include p q r Hp Hq Hdiv h Hh₁ Hh₂ Hg
theorem generate_proof : g ^ q = 1 :=
begin
  /-
   rewrite Hg,
   associativity would turn the goal
   (h ^ r) ^ q = 1  into h ^ (r * q).
   r * q = p - 1.
   Use Fermat little theorem from
   fermat little to prove it -/

end







end ElGamal

[Alex J. Best]

The typeclass is has_lt (zmodp p Hp) so lean is telling you it doesn't know what < means for zmodp which makes sense, there is no nice notion of lton integers modulo a prime .

[Alex J. Best]

The sentiment you are trying to express with Hh1 is really just that the residue class h is not 0.

[Alex J. Best]

The second one is has_pow (zmodp p Hp) ℕ+which is telling you that lean can't take a positive natural power of an element of this type, you could argue that this is an oversight. But the easiest fix is to take h^r.val instead.

[Alex J. Best]

You could also take r of type nat instead. That might be less work in the long run.

[Alex J. Best]

Spoilers below:

import data.zmod.basic data.nat.prime
  data.zmod.quadratic_reciprocity

namespace ElGamal

/-
A Schnorr group is a large prime-order subgroup of ℤ∗𝑝,
the multiplicative group of integers modulo 𝑝.
To generate such a group, we find 𝑝=𝑞𝑟+1 such that 𝑝 and 𝑞
are prime. Then, we choose any ℎ
in the range 1<ℎ<𝑝 such that ℎ^r ≠ 1 (mod𝑝)
The value 𝑔=ℎ^𝑟(mod𝑝) is a generator of a subgroup ℤ∗𝑝 of order 𝑞.
By Fermat's little theorem
g^q = h^(rq) = h^(p-1) = 1 (mod p)
-/

variables
  (p : ℕ) (q : ℕ) (r : ℕ)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hh₁ : h ≠ 0)
  (Hh₂ : h^r ≠ 1)
  (g : zmodp p Hp) /- generator of a subgroup of ℤ⋆p of order q -/
  (Hg : g = h^r)

#check Hh₁
include p q r Hp Hq Hdiv h Hh₁ Hh₂ Hg
theorem generate_proof : g ^ q = 1 :=
begin
   rewrite Hg,
   rw ← pow_mul,
   rw mul_comm,
   have : p - 1 = q * r := nat.pred_eq_of_eq_succ Hdiv,
   rw ← this,
   exact zmodp.fermat_little Hp Hh₁,
end







end ElGamal

[Mukesh Tiwari]

Thanks for the answer @Alex J. Best . Now, I am wondering about the error.
If I comment the proof 'generator_proof', then the error goes way.

variables
  (p : ℕ) (q : ℕ) (r : ℕ)
  (Hr : 2 ≤ r)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hh₁ : h ≠ 0)
  (Hh₂ : h^r ≠ 1)
  (g : zmodp p Hp) /- generator of a subgroup of ℤ⋆p of order q -/
  (Hg : g = h^r)


include Hg
theorem generator_proof : g ^ q = 1 :=
begin
  rw [Hg, <- pow_mul, mul_comm],
  have Ht : p - 1 = q * r := nat.pred_eq_of_eq_succ Hdiv,
  rw <- Ht, exact zmodp.fermat_little Hp Hh₁
end

variables
  (prikey : zmodp q Hq) /- private key -/
  (pubkey : zmodp p Hp) /- public key -/
  (Hrel : pubkey = g^prikey.val)

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * h^r.val)

kernel failed to type check declaration 'elgamal_enc' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  Π (p q : ℕ) (Hp : nat.prime p) (Hq : nat.prime q) (h g : zmodp p Hp),
    g = h ^ r → ℕ → zmodp p Hp → zmodp q Hq → zmodp p Hp × zmodp p Hp
elaborated value:
  λ (p q : ℕ) (Hp : nat.prime p) (Hq : nat.prime q) (h g : zmodp p Hp) (Hg : g = h ^ r) (r : ℕ) (m : zmodp p Hp)
  (r : zmodp q Hq), (g ^ r.val, g ^ m.val * h ^ r.val)
nested exception message:
failed to add declaration to environment, it contains local constants

[Alex J. Best]

This goes away for me if I wrap the previous declaration and preceding include in section ... end it seems lean doesn't like including these extra hypotheses.

[Alex J. Best]

import data.zmod.basic data.nat.prime
  data.zmod.quadratic_reciprocity

variables
  (p : ℕ) (q : ℕ) (r : ℕ)
  (Hr : 2 ≤ r)
  (Hp : nat.prime p)
  (Hq : nat.prime q)
  (Hdiv : p = q * r + 1)
  (h : zmodp p Hp)
  (Hh₁ : h ≠ 0)
  (Hh₂ : h^r ≠ 1)
  (g : zmodp p Hp) /- generator of a subgroup of ℤ⋆p of order q -/
  (Hg : g = h^r)

section
include Hg Hdiv Hh₁
theorem generator_proof : g ^ q = 1 :=
begin
  rw [Hg, <- pow_mul, mul_comm],
  have Ht : p - 1 = q * r := nat.pred_eq_of_eq_succ Hdiv,
  rw <- Ht, exact zmodp.fermat_little Hp Hh₁
end
end

variables
  (prikey : zmodp q Hq) /- private key -/
  (pubkey : zmodp p Hp) /- public key -/
  (Hrel : pubkey = g^prikey.val)

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * h^r.val)
#check elgamal_enc

works

[Mukesh Tiwari]

Alex J. Best said:

This goes away for me if I wrap the previous declaration and preceding include in section ... end it seems lean doesn't like including these extra hypotheses.

I tried to move all the variable declared after the proof 'generator_proof' before it, but the error is still the same.
Anyway, your solution is working, so it's fine.

[Alex J. Best]

Right the issue is the include line which adds the unneeded hypotheses (for elgamal_enc) Hg Hdiv Hh₁ to all following declarations.

[Mukesh Tiwari]

Why does this find is not returning any lemma? I want to prove Ht1.

#find (_ ^ _ ≠ 0)

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * pubkey^r.val)

def elgamal_dec (c : zmodp p Hp ×  zmodp p Hp) :=
  c.2 * (c.1^prikey.val)⁻¹

include Hrel
lemma elgama_enc_dec_identity :
∀ m r, elgamal_dec p q Hp Hq prikey
      (elgamal_enc p q Hp Hq g pubkey m r) = g^m.val :=
begin
  unfold elgamal_enc elgamal_dec,
  intros, simp, rw [Hrel, <- pow_mul, <- pow_mul],
  have Ht₁ : g ^ (prikey.val * r.val) ≠ 0 :=
    sorry,
  have Ht₂ : r.val * prikey.val = prikey.val * r.val :=
       mul_comm r.val prikey.val,
  rw [Ht₂, mul_assoc, mul_inv_cancel Ht₁], ring
end

[Alex J. Best]

What is elgamal_dec? You might find the tactic library_search more useful than find

[Mukesh Tiwari]

Updated the code.

[Alex J. Best]

def elgamal_enc (m : zmodp p Hp) (r : zmodp q Hq) :=
  (g^r.val, g^m.val * pubkey^r.val)

def elgamal_dec (c : zmodp p Hp ×  zmodp p Hp) :=
  c.2 * (c.1^prikey.val)⁻¹

include Hrel Hg Hh₁
lemma elgama_enc_dec_identity :
∀ m t, elgamal_dec p q Hp Hq prikey
      (elgamal_enc p q Hp Hq g pubkey m t) = g^m.val :=
begin
  unfold elgamal_enc elgamal_dec,
  intros, simp, rw [Hrel, <- pow_mul, <- pow_mul],
  have : g ≠ 0 := begin rw Hg, exact pow_ne_zero r Hh₁, end,
  have Ht₁ : g ^ (prikey.val * t.val) ≠ 0 := pow_ne_zero (prikey.val * t.val) this,
  have Ht₂ : t.val * prikey.val = prikey.val * t.val :=
       mul_comm t.val prikey.val,
  rw [Ht₂, mul_assoc, mul_inv_cancel Ht₁], ring
end

[Alex J. Best]

You need g nonzero

[Alex J. Best]

For which you need h nonzero

[Mukesh Tiwari]

Thanks Alex. I am looking for a vector library, and I see two vector library in mathlib, vector2 and vector3.

[Mukesh Tiwari]

https://github.com/leanprover-community/mathlib/blob/78ffbae077c50ed8ee060b3ac544f6f1d4359f39/src/number_theory/dioph.lean#L109

[Mukesh Tiwari]

https://github.com/leanprover-community/mathlib/blob/c718a22925872db4cb5f64c36ed6e6a07bdf647c/src/data/vector2.lean

[Mukesh Tiwari]

Which one would suggest to use ?

[Kevin Buzzard]

Use vector

[Mukesh Tiwari]

Thanks Kevin.

[Mukesh Tiwari]

By the way Coq has a nice extraction facility, and you can extract any Coq program into Haskell, OCaml, or Scheme. I am wondering if there is something like this in Lean?

[Kevin Buzzard]

In lean 4 you should be able to extract to...umm...C? I don't have a clue about this stuff

[Scott Morrison]

We really should give #find some additional love.

[Mukesh Tiwari]

@Scott Morrison That would make the life easier for new comers used to Coq's search pattern. I found linear_search quite nice because it just gives me some lemma from the remote corners of the mathlib library.

[Mukesh Tiwari]

I am looking for a lemma to prove that

ms : list (zmodp p Hp),
_x : list.length ms = n,
rs : list (zmodp q Hq),
_x : list.length rs = n
⊢ list.length (list.zip_with f  ms rs) = n

I could find anything using find or library_search

[Kevin Buzzard]

I agree that list.zip_with doesn't seem to have been given much love in mathlib! It's defined in core, and for some of these things data.list.basic just makes an API, but apparently not here. I think it might be a hole in the library, although I would imagine it's not hard to prove by induction on n?

[Mukesh Tiwari]

@Kevin Buzzard If, say, my goal is to prove equality x = x, then I can use tactic or write the exact terms. I am wondering how can I see the terms build using the tactics ?

[Kevin Buzzard]

#print

[Kevin Buzzard]

(deleted)

[Mukesh Tiwari]

#print is just printing the type signature. For this code

def vector_ciphertext_mult {n : ℕ} :
  vector (zmodp p Hp × zmodp p Hp) n -> vector (zmodp p Hp × zmodp p Hp) n ->
  vector (zmodp p Hp × zmodp p Hp) n
  | ⟨cs₁ , Hc₁⟩  ⟨cs₂, Hc₂⟩ :=
    ⟨list.zip_with (ciphertext_mult p Hp) cs₁  cs₂,
    begin
      have Ht : list.length cs₁ = list.length cs₂ :=
      begin rw [Hc₁, Hc₂] end,
      rw <- Hc₁, apply zip_with_len_l, exact Ht,
    end ⟩

The output of #print vector_ciphertext_mult

def ElGamal.vector_ciphertext_mult : Π (p : ℕ) (Hp : nat.prime p) {n : ℕ},
  vector (zmodp p Hp × zmodp p Hp) n → vector (zmodp p Hp × zmodp p Hp) n → vector (zmodp p Hp × zmodp p Hp) n :=
λ (p : ℕ) (Hp : nat.prime p) {n : ℕ}, vector_ciphertext_mult._main p Hp

But I want to see the CIC terms build by tactics.

[Bryan Gin-ge Chen]

The proof term is there, it's everything after the :=.

[Mukesh Tiwari]

@Bryan Gin-ge Chen Seems like something I misunderstood about Lean, so let me give a similar analogy from Coq. In Coq, when you write tactic to solve some goal, under the hood it is constructing a Gallina (CIC) term (which you could have written manually, but no one does this because it is very cumbersome). Now at any point of the time, if you want to see the CIC (Gallina) terms, then you simply write 'Show Proof', and it will print all the Gallina (CIC) terms constructed so far.

In my 'vector_ciphertext_mult' program, there are two things: a list (which I believe is in CIC) and a proof (but written in tactic mode). I want to see how the proof terms appears in CIC (or core language) because I don't think tactics are part of core language in Lean.

[Bryan Gin-ge Chen]

Sorry, I guess I was a bit unclear, I meant the part after := in the output of #print vector_ciphertext_mult, namely: λ (p : ℕ) (Hp : nat.prime p) {n : ℕ}, vector_ciphertext_mult._main p Hp.

That is a term, not a tactic. I don't know if you would consider that in the "core" language of Lean since you can also export something even lower level. I've never played around with that though.

[Kevin Buzzard]

I think you just have to keep digging. Can you see that your definition is essentially vector_ciphertext_mult._main? Why don't you #print that, and then keep printing stuff?

Hey -- do you know about set_option pp.all true? Try that before a #print statement, it gives you much more information.

[Mukesh Tiwari]

Sorry for the confusion. Some how I missed the ._main part in the vector_ciphertext_mult._main p Hp . Thanks again @Kevin Buzzard @Bryan Gin-ge Chen .