Zulip Chat Archive

Stream: general

Topic: proof


Jane (Feb 24 2020 at 20:26):

Does anyone know how to write the proof of (∩ i, D i) ∪ (∩ i, E i) ⊆ ∩ i, (D i ∪ E i) in lean??

Kenny Lau (Feb 24 2020 at 20:28):

can you write the theorem in lean and use sorry for the proof and then post the code here?

Jane (Feb 24 2020 at 20:29):

I am in a math class of this lol

Jane (Feb 24 2020 at 20:30):

This is the first time I use this chat room, nice to meet you btw. How can I post it here?
like this?
example : (∩ i, D i) ∪ (∩ i, E i) ⊆ ∩ i, (D i ∪ E i) :=
sorry

Kenny Lau (Feb 24 2020 at 20:33):

that would be closer, but it wouldn't compile because you have not specified the types of D and E

Patrick Massot (Feb 24 2020 at 20:33):

You need to surround your code with ```lean  and ``` 

Jane (Feb 24 2020 at 20:34):

variables {U I : Type}
variables D E : I  set U
example : ( i, D i)  ( i, E i)   i, (D i  E i) :=
    assume x,
    assume h: x  ( i, D i)  ( i, E i),
    or.elim h (sorry)(sorry)

This is what I got so far.

Patrick Massot (Feb 24 2020 at 20:36):

Is that accepted by Lean?

Patrick Massot (Feb 24 2020 at 20:36):

The intersection symbols don't look right.

Sebastien Gouezel (Feb 24 2020 at 20:36):

Non-pedagogic answer:

open set

lemma zou (C D : E  set F) :
  ( i, C i)  ( i, D i)  ( i, C i  D i) :=
union_subset (Inter_subset_Inter (λ i, subset_union_left _ _)) (Inter_subset_Inter (λ i, subset_union_right _ _))

Patrick Massot (Feb 24 2020 at 20:36):

Sébastien intersections look right.

Jane (Feb 24 2020 at 20:37):

I have no clue. our teacher uses cocalc

Mario Carneiro (Feb 24 2020 at 20:37):

use copy paste

Patrick Massot (Feb 24 2020 at 20:38):

Sébastien, do you mean this lemma is not in mathlib?

Mario Carneiro (Feb 24 2020 at 20:38):

are you using cocalc, or do you have a local installation? In either case, lean should give you an error if you use the wrong intersection symbol

Patrick Massot (Feb 24 2020 at 20:38):

This is shocking

Mario Carneiro (Feb 24 2020 at 20:38):

I'm not that shocked that this lemma is not available, but it wouldn't hurt to add it

Mario Carneiro (Feb 24 2020 at 20:38):

probably finish can handle it

Jane (Feb 24 2020 at 20:39):

It says "unexpected token" what does that suppose to mean?

Mario Carneiro (Feb 24 2020 at 20:39):

that means you used the wrong symbol

Jane (Feb 24 2020 at 20:40):

oh, but I copy the lemma you post here, I am so frustrated

Mario Carneiro (Feb 24 2020 at 20:40):

The problem is that is the binary intersection symbol, and is the "big" intersection

Mario Carneiro (Feb 24 2020 at 20:40):

which is for doing indexed intersection

Patrick Massot (Feb 24 2020 at 20:40):

example (U : Type) (I : Type) (D E : I  set U) :
 ( i, D i)  ( i, E i)   i, (D i  E i) :=
begin
  intros x,
  finish
end

does work

Kenny Lau (Feb 24 2020 at 20:40):

non-pedagogical answer 2:

import data.set.lattice

variables {U I : Type}
variables D E : I  set U
example : ( i, D i)  ( i, E i)   i, (D i  E i) :=
by rintros x (hx | hx) _ i, rfl⟩; [left, right]; exact hx _ i, rfl

Patrick Massot (Feb 24 2020 at 20:41):

It's a bit unfortunate that broken syntax highlighting flags that big intersection symbol

Johan Commelin (Feb 24 2020 at 20:41):

@Jane Aside: Who is the teacher?

Sebastien Gouezel (Feb 24 2020 at 20:41):

finish does not kill it. Is is not in mathlib (at least, it is not found by library_search). And I am not really surprised it is not there, as it is not that common or useful -- I mean, if it is not in mathlib it means that noone has needed it until now.

Jane (Feb 24 2020 at 20:41):

Paige N? I am in the Ohio State

Mario Carneiro (Feb 24 2020 at 20:41):

oh hey, my alma mater

Mario Carneiro (Feb 24 2020 at 20:41):

they are doing lean now?

Patrick Massot (Feb 24 2020 at 20:41):

finish kills it after intro x

Sebastien Gouezel (Feb 24 2020 at 20:42):

Yes indeed.

Jane (Feb 24 2020 at 20:42):

whaaaaaat is going on now?? I am so lost.

Patrick Massot (Feb 24 2020 at 20:43):

Let me try a semi-pedagogical one:

import data.set

set_option pp.beta true

example (U : Type) (I : Type) (D E : I  set U) :
 ( i, D i)  ( i, E i)   i, (D i  E i) :=
begin
  intros x h,
  rintro _ i, rfl,
  cases h with hl hr,
  left,
  finish,
  right,
  finish,
end

Patrick Massot (Feb 24 2020 at 20:43):

At least you can follow the main steps of the proof.

Patrick Massot (Feb 24 2020 at 20:43):

but I guess the rintro line looks pretty mysterious

Mario Carneiro (Feb 24 2020 at 20:44):

maybe use simp there

Kenny Lau (Feb 24 2020 at 20:44):

non-pedagogical one 3:

import data.set.lattice

open lattice

variables {U I : Type}
variables D E : I  set U
example : ( i, D i)  ( i, E i)   i, (D i  E i) :=
show ( i, D i)  ( i, E i)   i, (D i  E i),
from le_infi $ λ i, sup_le_sup (infi_le D i) (infi_le E i)

Patrick Massot (Feb 24 2020 at 20:44):

Yes, simp, intro i is better than rintro dark magic

Kenny Lau (Feb 24 2020 at 20:45):

I don't see what's wrong with Sébastien's proof

Patrick Massot (Feb 24 2020 at 20:45):

Where is that "lattices for the win" emoji again?

Kenny Lau (Feb 24 2020 at 20:45):

it's perfectly reasonable and it flows from the theorem

Mario Carneiro (Feb 24 2020 at 20:45):

I think your proof 3 is the same as Sebastien's first proof

Kenny Lau (Feb 24 2020 at 20:45):

all proofs are equal

Patrick Massot (Feb 24 2020 at 20:46):

It's the same after recasting in lattices terms

Mario Carneiro (Feb 24 2020 at 20:46):

do you actually need the show?

Patrick Massot (Feb 24 2020 at 20:47):

Probably not.

Jane (Feb 24 2020 at 20:47):

OMG thank you guys very much although I am confused about it

Mario Carneiro (Feb 24 2020 at 20:47):

lol there are too many non pedagogical proofs floating around now

Patrick Massot (Feb 24 2020 at 20:47):

Sorry it turned into an expert discussion pretty quickly

Jane (Feb 24 2020 at 20:47):

Just being curious, where do people use lean??

Mario Carneiro (Feb 24 2020 at 20:48):

on their computers?

Jane (Feb 24 2020 at 20:48):

like in which area??

Jane (Feb 24 2020 at 20:48):

pure math?

Mario Carneiro (Feb 24 2020 at 20:49):

what area are you in?

Jane (Feb 24 2020 at 20:49):

Biology lol

Kenny Lau (Feb 24 2020 at 20:49):

finally, in the style of Jane's attempt:

import data.set.lattice

variables {U I : Type}
variables D E : I  set U
example : ( i, D i)  ( i, E i)   i, (D i  E i) :=
assume x : U,
assume h : x  ( i, D i)  ( i, E i),
or.elim h
  (assume hd : x   i, D i,
    set.mem_Inter_of_mem $ assume i : I, or.inl (set.mem_Inter.1 hd i))
  (assume he : x   i, E i,
    set.mem_Inter_of_mem $ assume i : I, or.inr (set.mem_Inter.1 he i))

Mario Carneiro (Feb 24 2020 at 20:49):

formal math sits somewhere between pure math, computer science and logic

Kenny Lau (Feb 24 2020 at 20:49):

and biology

Mario Carneiro (Feb 24 2020 at 20:51):

that's a nice pedagogical proof kenny

Jane (Feb 24 2020 at 20:51):

Thank you guys so much

Mario Carneiro (Feb 24 2020 at 20:51):

although maybe the tactic folks won't like it

Jane (Feb 24 2020 at 20:54):

do any of you know Dr. Paige North??

Mario Carneiro (Feb 24 2020 at 20:56):

I don't think she has appeared here, and I don't think I met her in undergrad either. Is she in biology?

Patrick Massot (Feb 24 2020 at 20:56):

https://paigenorth.github.io/

Patrick Massot (Feb 24 2020 at 20:57):

Doesn't sounds like biology to me

Jane (Feb 24 2020 at 20:58):

I am in math-bio track and ecology double major now.

Mario Carneiro (Feb 24 2020 at 20:59):

Oh, she does HoTT

Jane (Feb 25 2020 at 03:14):

Hey sorry to bother you guys' Monday night, here comes another problem. I really don't know how to do this.

variables A B C : set U
variables D E F: I  set U
variable u : U
example : (A  B)  (powerset A)  (powerset B) :=
sorry

this looks so obvious but none of my friends know how to do it....

Johan Commelin (Feb 25 2020 at 07:35):

@Jane I would start with

begin
  split,
  { intros h s hs,
    sorry },
  { intros h x hx,
    sorry }
end

Johan Commelin (Feb 25 2020 at 07:35):

See if that helps...


Last updated: Dec 20 2023 at 11:08 UTC