## Stream: new members

### Topic: Schnorr Group

#### Mukesh Tiwari (Mar 22 2020 at 03:40):

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

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 (Mar 22 2020 at 04:59):

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 (Mar 22 2020 at 05:00):

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

#### Alex J. Best (Mar 22 2020 at 05:01):

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 (Mar 22 2020 at 05:04):

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

#### Alex J. Best (Mar 22 2020 at 05:06):

Spoilers below:

import data.zmod.basic data.nat.prime

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 (Mar 22 2020 at 07:05):

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 (Mar 22 2020 at 07:14):

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 (Mar 22 2020 at 07:14):

import data.zmod.basic data.nat.prime

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 (Mar 22 2020 at 07:27):

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 (Mar 22 2020 at 07:54):

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

#### Mukesh Tiwari (Mar 22 2020 at 07:58):

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 (Mar 22 2020 at 09:19):

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

#### Mukesh Tiwari (Mar 22 2020 at 09:34):

Updated the code.

#### Alex J. Best (Mar 22 2020 at 09:47):

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 (Mar 22 2020 at 09:47):

You need g nonzero

#### Alex J. Best (Mar 22 2020 at 09:48):

For which you need h nonzero

#### Mukesh Tiwari (Mar 22 2020 at 11:13):

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

#### Mukesh Tiwari (Mar 22 2020 at 11:14):

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

#### Mukesh Tiwari (Mar 22 2020 at 11:16):

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

#### Mukesh Tiwari (Mar 22 2020 at 11:16):

Which one would suggest to use ?

Use vector

Thanks Kevin.

#### Mukesh Tiwari (Mar 22 2020 at 11:40):

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 (Mar 22 2020 at 12:58):

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

#### Scott Morrison (Mar 22 2020 at 22:55):

We really should give #find some additional love.

#### Mukesh Tiwari (Mar 23 2020 at 00:55):

@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 (Mar 23 2020 at 07:35):

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 (Mar 23 2020 at 07:47):

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 (Mar 23 2020 at 11:21):

@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 (Mar 23 2020 at 12:49):

#print

(deleted)

#### Mukesh Tiwari (Mar 23 2020 at 21:37):

#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 (Mar 23 2020 at 21:40):

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

#### Mukesh Tiwari (Mar 23 2020 at 22:06):

@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 (Mar 23 2020 at 23:00):

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 (Mar 23 2020 at 23:13):

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 (Mar 24 2020 at 01:25):

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 .

Last updated: May 13 2021 at 23:16 UTC