Sets

Stream: new members

[Brandon Brown]

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]

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]

@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]

Thanks!

[Johan Commelin]

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]

Also, if you don't like dec_trivial, you could use a combination of or.inl, or.inr and rfl.

[Bryan Gin-ge Chen]

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

[Brandon Brown]

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]

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

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

[Mario Carneiro]

or.inl _ would expect a proof of 1 = 1 at the location of the _

[Johan Commelin]

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

[Bryan Gin-ge Chen]

Let p := 1=1, q := false and h := rfl.

[Mario Carneiro]

and rfl is a proof of 1 = 1

[Brandon Brown]

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]

rfl is short for eq.refl _

[Johan Commelin]

rfl is a smart kid (-;

[Kevin Buzzard]

refl is a powerful tactic!

[Kenny Lau]

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]

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]

(thanks, squeeze_simp)

[Bryan Gin-ge Chen]

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

[Kenny Lau]

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]

if \a is anything concrete (like \N) then it will work

[Bryan Gin-ge Chen]

Oh, right. The type class is a variable so there's no actual definition.

[Kenny Lau]

yeah that also confused me for a while :P

[Chemla]

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]

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]

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]

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]

Can you read #backticks and edit your post accordingly?

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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]

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

[Chemla]

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]

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

[Johan Commelin]

@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]

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

[Chemla]

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]

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]

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]

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]

Thank you. Good evening.

[Kyle Miller]

@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]

(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]

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]

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]

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.