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