# Zulip Chat Archive

## 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 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 (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 `lt`

on 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 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 (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 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 (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):

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

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

Which one would suggest to use ?

#### Kevin Buzzard (Mar 22 2020 at 11:25):

Use vector

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

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`

#### Kevin Buzzard (Mar 23 2020 at 12:49):

(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