# Zulip Chat Archive

## Stream: new members

### Topic: Sets

#### Brandon Brown (May 15 2020 at 03:53):

How do I do something as trivial as proving set membership?

```
import data.finset
def x1 : finset ℕ := {1,2,3}
#reduce 1 ∈ x1 --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false
example : 1 ∈ x1 := sorry
```

#### Bryan Gin-ge Chen (May 15 2020 at 03:57):

In this case you can use `dec_trivial`

:

```
import data.finset
def x1 : finset ℕ := {1,2,3}
#reduce 1 ∈ x1 --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false
example : 1 ∈ x1 := dec_trivial
```

#### Johan Commelin (May 15 2020 at 03:58):

@Brandon Brown If you've got a very explicit set, like in your example, then it's `dec_trivial`

, like Bryan said. If you have a set if the form `finset.range n`

or `finset.filter foo bar`

, then there will be lemmas `finset.mem_range`

and `finset.mem_filter`

etc... that help you proving this.

#### Brandon Brown (May 15 2020 at 03:59):

Thanks!

#### Johan Commelin (May 15 2020 at 04:00):

Brandon Brown said:

`#reduce 1 ∈ x1 --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false`

Note that this is about to change to

```
#reduce 1 ∈ x1 --1 = 1 ∨ 1 = 2 ∨ 1 = 3
```

which I think is a big improvement (-;

#### Johan Commelin (May 15 2020 at 04:01):

Also, if you don't like `dec_trivial`

, you could use a combination of `or.inl`

, `or.inr`

and `rfl`

.

#### Bryan Gin-ge Chen (May 15 2020 at 04:02):

This reminds me a lot of one of my early threads here.

#### Brandon Brown (May 15 2020 at 04:17):

I have a more basic question. I understand constructions of the form

```
variables (p q : Prop)
example (h : p) : p ∨ q := or.inl h
```

Because I'm injecting h

#### Brandon Brown (May 15 2020 at 04:18):

But I don't really understand what's going on under the hood with

```
example : (1 = 1) ∨ false := or.inl (rfl)
```

#### Mario Carneiro (May 15 2020 at 04:18):

`or.inl _`

would expect a proof of `1 = 1`

at the location of the `_`

#### Johan Commelin (May 15 2020 at 04:18):

Well, you need to inject a proof of `1 = 1`

#### Bryan Gin-ge Chen (May 15 2020 at 04:18):

Let `p := 1=1`

, `q := false`

and `h := rfl`

.

#### Mario Carneiro (May 15 2020 at 04:18):

and `rfl`

is a proof of `1 = 1`

#### Brandon Brown (May 15 2020 at 04:22):

Ahh right I see

```
variable p : (1 = 1)
example : (1 = 1) ∨ false := or.inl p
```

So using rfl is inferring this since what else could it be

#### Mario Carneiro (May 15 2020 at 04:23):

`rfl`

is short for `eq.refl _`

#### Johan Commelin (May 15 2020 at 04:23):

rfl is a smart kid (-;

#### Kevin Buzzard (May 15 2020 at 05:59):

`refl`

is a powerful tactic!

#### Kenny Lau (May 15 2020 at 06:54):

the correct way, much as I hate it, is `by simp`

:

```
import data.finset
def x1 : finset ℕ := {1,2,3}
example : 1 ∈ x1 := by simp [x1]
variables {α : Type*} [has_one α] [has_add α] [decidable_eq α]
def x2 : finset α := {1,2,3}
example : (1 : α) ∈ (x2 : finset α) := dec_trivial -- fails
example : (1 : α) ∈ (x2 : finset α) := by simp [x2] -- works
```

#### Kenny Lau (May 15 2020 at 06:58):

the last line is equivalent to `simp only [x2, eq_self_iff_true, or_true, finset.mem_insert, finset.mem_singleton, finset.singleton_eq_singleton]`

#### Kenny Lau (May 15 2020 at 06:58):

(thanks, `squeeze_simp`

)

#### Bryan Gin-ge Chen (May 15 2020 at 07:01):

That's surprising to me. Are there some missing decidability instances somewhere?

#### Kenny Lau (May 15 2020 at 07:03):

no, it's just that asserting `\a`

has decidable_eq does not actually give an algorithm to decide whether two terms of `\a`

are equal

#### Kenny Lau (May 15 2020 at 07:03):

if `\a`

is anything concrete (like `\N`

) then it will work

#### Bryan Gin-ge Chen (May 15 2020 at 07:07):

Oh, right. The type class is a `variable`

so there's no actual definition.

#### Kenny Lau (May 15 2020 at 07:19):

yeah that also confused me for a while :P

#### Chemla (May 25 2022 at 11:32):

Hi, First, please excuse my private message if you received one from me, I didn't know how to begin and someone comprehensive told me to post in new members : I am completely new in Lean proving. I need help to define sets, to formalize in Lean a simple proof yet written mathematically (by others than me). Could you help me to do that. I put the definition of sets here : http://denise.vella.chemla.free.fr/defsets.png and the failure of my definition of sets here http://denise.vella.chemla.free.fr/ratage1.png Thank you for your help. The proof to be tested in Lean is here http://denise.vella.chemla.free.fr/jade1.pdf

#### Eric Wieser (May 25 2022 at 11:37):

Hi, thanks for moving your posts here; Zulip can be confusing if you're new!

Would you be able to produce a #mwe showing what you have so far? There look to be lots of errors in that screenshot, and it's not clear which one you're asking about. You can post code on Zulip in #backticks so that we can copy-paste it to try to help you.

#### Chemla (May 25 2022 at 11:59):

Thank you for answering. Until line 72, that's all things I copied from the tutorial I believed I would need (modulo for integers, and logical and found somewhere). As I don't know how to make a #mwe, I put my code here http://denise.vella.chemla.free.fr/tentecglean1.lean

#### Chemla (May 25 2022 at 12:00):

OK, here it is (only from 72 and seq.) :

def Fp (n : nat, p : nat) : nat :=

begin

intro m,

have (mod_equiv 2 m 1) ∧ (3 ≤ m ≤ n/2)

∧ (not mod_equiv p m 0) ∧ (not mod_equiv p m n)

end

def D (n : nat) : nat :=

intro m,

have (∀ p, nat.prime p, 3 ≤ p ≤ sqrt(n)) ∧ (m in Fp(n,p))

lemma lem1 : ∀ m, ((mod_equiv 2 m 1) ∧

((∀ p, (p : nat, p ≤ sqrt(n) ∧ nat.prime p

implies not mod_equiv p n 0)))

implies nat.prime m :=

begin

sorry ;

end

lemma lem2 : ∀x, x in D(n) := nat.prime x

begin

sorry ;

end

lemma lem3 : ∀x, n-x in D(n) := nat.prime x

begin

sorry ;

end

lemma lem4 : intro n, mod_equiv 2 n 0, n ≥ 6, D(n) != emptyset implies

exists p, exists q, nat.prime p, nat.prime q, n = p+q

begin

sorry ;

end

#### Eric Wieser (May 25 2022 at 12:35):

Can you read #backticks and edit your post accordingly?

#### Eric Wieser (May 25 2022 at 12:39):

Chemla said:

As I don't know how to make a #mwe, I put my code here http://denise.vella.chemla.free.fr/tentecglean1.lean

Unfortunately your webserver is not configured to send `.lean`

files as `charset=utf-8`

, so that file is hard to read in a browser.

#### Chemla (May 25 2022 at 13:37):

Eric Wieser said:

Chemla said:

As I don't know how to make a #mwe, I put my code here http://denise.vella.chemla.free.fr/tentecglean1.lean

Unfortunately your webserver is not configured to send

`.lean`

files as`charset=utf-8`

, so that file is hard to read in a browser.`import data.int.basic import data.nat.prime import tactic.linarith open nat namespace int def dvd (m n : ℤ) : Prop := ∃ k, n = m * k instance : has_dvd int := ⟨int.dvd⟩ @[simp] theorem dvd_zero (n : ℤ) : n ∣ 0 := ⟨0, by simp⟩ theorem dvd_intro {m n : ℤ} (k : ℤ) (h : n = m * k) : m ∣ n := ⟨k, h⟩ end int open int section mod_m parameter (m : ℤ) variables (a b c : ℤ) definition mod_equiv (m a b : ℤ) := (m ∣ b - a) theorem mod_refl : mod_equiv m a a := show m ∣ a - a, by simp theorem mod_symm (h : mod_equiv m a b) : mod_equiv m b a := by cases h with c hc; apply dvd_intro (-c); simp [eq.symm hc] local attribute [simp] add_assoc add_comm add_left_comm theorem mod_trans (h₁ : mod_equiv m a b) (h₂ : mod_equiv m b c) : mod_equiv m a c := begin cases h₁ with d hd, cases h₂ with e he, apply dvd_intro (d + e), simp [mul_add, eq.symm hd, eq.symm he, sub_eq_add_neg] end end mod_m #check (mod_refl : ∀ m : ℤ, ∀ a : ℤ, mod_equiv m a a) #check (mod_symm : ∀ m : ℤ, ∀ a : ℤ, ∀ b : ℤ, mod_equiv m a b → mod_equiv m b a) #check (mod_trans : ∀ m : ℤ, ∀ a : ℤ, ∀ b : ℤ, ∀ c : ℤ, mod_equiv m a b → mod_equiv m b c → mod_equiv m a c) theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := assume hpq : p ∧ q, have hp : p, from and.left hpq, have hq : q, from and.right hpq, show q ∧ p, from and.intro hq hp def double (x : ℕ) : ℕ := x + x #print double #check double 3 #reduce double 3 -- 6 def square (x : ℕ) := x * x #print square #check square 3 #reduce square 3 -- 9 def do_twice (f : ℕ → ℕ) (x : ℕ) : ℕ := f (f x) #reduce do_twice double 2 -- 8 def Fp (n : nat, p : nat) : nat := begin intro m, have (mod_equiv 2 m 1) ∧ (3 ≤ m ≤ n/2) ∧ (not mod_equiv p m 0) ∧ (not mod_equiv p m n) end def D (n : nat) : nat := intro m, have (∀ p, nat.prime p, 3 ≤ p ≤ sqrt(n)) ∧ (m in Fp(n,p)) lemma lem1 : ∀ m, ((mod_equiv 2 m 1) ∧ ((∀ p, (p : nat, p ≤ sqrt(n) ∧ nat.prime p implies not mod_equiv p n 0))) implies nat.prime m := begin sorry ; end lemma lem2 : ∀x, x in D(n) := nat.prime x begin sorry ; end lemma lem3 : ∀x, n-x in D(n) := nat.prime x begin sorry ; end lemma lem4 : intro n, mod_equiv 2 n 0, n ≥ 6, D(n) != emptyset implies exists p, exists q, nat.prime p, nat.prime q, n = p+q begin sorry ; end`

#### Eric Wieser (May 25 2022 at 13:48):

Note you can edit your previous message rather than posting a new one

#### Eric Wieser (May 25 2022 at 13:51):

Regarding your actual question: lean is telling you that this is a syntax error on line 72

```
def Fp (n : nat, p : nat) : nat :=
```

as it should be spelt

```
def Fp (n : nat) (p : nat) : nat :=
```

When lean gives you error messages, you have to solve them in order, because after the first one Lean can get very confused

#### Patrick Massot (May 25 2022 at 13:53):

or `def Fp (n p : nat) : nat :=`

#### Chemla (May 25 2022 at 14:20):

Thank you very much for this help. But as you can see in the images png I posted in my first message, my question was in other words : "there are no sets in Lean, it seems to me, so my sets must be defined using functions, is it all right or must I define sets, like in page 158 I think, of the tutorial, and define intersection, and all that ?". Thank you very much.

#### Chemla (May 25 2022 at 14:22):

Not in page 158, but in page 155, § 11.3, there is a definition of set...

#### Johan Commelin (May 25 2022 at 14:31):

@Chemla Most of mathematics can be very naturally translated from set theory to type theory. Unless you are doing hardcore set theory in the logic sense, you should probably just use types.

#### Johan Commelin (May 25 2022 at 14:31):

Number theory, topology, algebra, geometry... everything just uses types.

#### Chemla (May 25 2022 at 15:07):

Thank you Johan. Sincerely (I hope this word exists in english), it is not natural for me to reason with types : I am an old computer scientist (this means that I was not used to use object oriented languages - they seem to correspond to types with attributes associated to objects) but only functions. Perhaps, your answer makes me understand that I should rather use a characteristic function instead of a set. This translation of an existing paper demonstration, all the more I had not been able to write it, is presumably too headlock for me. Thank you.

#### Patrick Johnson (May 25 2022 at 15:18):

This is how I would translate that paper to Lean

(I may have made some mistake, please double-check it yourself):

```
import data.nat.prime
def F (n p : ℕ) : set ℕ :=
{m : ℕ | odd m ∧ 3 ≤ m ∧ m ≤ n / 2 ∧ m % p ≠ 0 ∧ m % p ≠ n}
def D (n : ℕ) : set ℕ :=
⋂ (p : {p : ℕ // prime p ∧ 3 ≤ p ∧ p ≤ n.sqrt}), F n p
lemma lem₁ {m : ℕ} (h₁ : m ≠ 1) (h₂ : odd m)
(h₃ : ∀ (p : ℕ), prime p ∧ 3 ≤ p ∧ p ≤ m.sqrt → m % p ≠ 0) : prime m :=
begin
sorry
end
lemma lem₂ {n : ℕ} : D n ⊆ prime :=
begin
sorry
end
lemma lem₃ {n : ℕ} : (λ (m : ℕ), n - m) '' D n ⊆ prime :=
begin
sorry
end
lemma lem₄ {n : ℕ} (h₁ : ∃ (m : ℕ), n = m * 2 + 6) (h₂ : (D n).nonempty) :
∃ (p q : ℕ), prime p ∧ prime q ∧ n = p + q :=
begin
sorry
end
```

#### Chemla (May 25 2022 at 15:24):

Thank you very much, Patrick. I'll look to this very carefully.

Ma last question : I found this page sets in lean typing "sets in Lean" in google but the page in question is not accessible in the page of current (?) tutorial here last ? tutorial v 3.23.0that one advised me. Is there a reason for this ? Thank you

#### Eric Wieser (May 25 2022 at 15:46):

Your first link is from https://github.com/leanprover/logic_and_proof which is (was?) a CMU undergraduate course, while the second is from https://github.com/leanprover/theorem_proving_in_lean. I don't know what the link between the two websites is, beyond being written by similar groups of people

#### Chemla (May 25 2022 at 16:04):

Thank you. Good evening.

#### Kyle Miller (May 25 2022 at 16:05):

@Chemla Here is the definition of sets in Lean: docs#set (and click "Source")

```
def set (α : Type u) := α → Prop
```

Lean sets are characteristic functions that are accompanied by familiar set-like notation.

#### Kyle Miller (May 25 2022 at 16:07):

(They are characteristic functions on a type, where the type can be thought of as being the universe for the elements of the set.)

#### Chemla (May 25 2022 at 18:57):

Thank you Kyle, I will try, but I really think it's too much difficult for me, even if the three first lemma have yet been formally demonstrated.

#### Kyle Miller (May 25 2022 at 19:28):

What I was meaning by that was a response to your comment:

Perhaps, your answer makes me understand that I should rather use a characteristic function instead of a set.

It turns out that Lean sets are characteristic functions on types already, if that helps clarify anything.

The fact that `set α`

is defined to be `α → Prop`

means that for each term `x : α`

a set `s : set α`

gives either true or false, which we interpret to mean whether or not `x`

is an element of `s`

. In fact, the notation `x ∈ s`

is defined to be `s x`

.

#### Chemla (May 31 2022 at 15:03):

Thank you Kyle and excuse the time I took to thank : I make all those researches on my free time, and I don't have so much such time. Last week I translated in french the synthesis text of Buzzard (the one he will present at IMU 2022 online conference perhaps) : the paper is on free access in arxiv and I translated it to familiarize a little to the subject (and I made the same with another paper concerning adeles and ideles because I believed it would help me to understand a bit more about those objects but it was not the case).

I will dip (or drown) in the exercize of trying to verify "my" 3 lemmas in two weeks I hope. If I succeed (hum...), I will post.

Last updated: Dec 20 2023 at 11:08 UTC