Zulip Chat Archive

Stream: general

Topic: exists (X) (Y)


view this post on Zulip Kevin Buzzard (May 17 2018 at 17:54):

topological_space.is_topological_basis has, as part of its definition, ∃ (t₃ : set α) (H : t₃ ∈ s), x ∈ t₃ ∧ ..., that is, "there exists a set with some property such that..."

view this post on Zulip Kevin Buzzard (May 17 2018 at 17:54):

So I've just sat down to write some trivial thing and it's ended up like this:

view this post on Zulip Kevin Buzzard (May 17 2018 at 17:55):

import analysis.topology.topological_space
universe u

variables {X : Type u} [topological_space X] {B : set (set X)}

definition basis_nhds (HB : topological_space.is_topological_basis B) (x : X) := {U : set X // x  U  U  B}

noncomputable instance basis_nhds_has_so_called_sup (HB : topological_space.is_topological_basis B) (x : X) :
lattice.has_sup (basis_nhds HB x) := {
  sup := λ Us Vs, begin
    cases (classical.indefinite_description _ (HB.1 Us.1 Us.2.2 Vs.1 Vs.2.2 x Us.2.1,Vs.2.1))
      with W HW,
    cases (classical.indefinite_description _ HW) with HB HW,
    exact W,HW.1,HB⟩⟩
  end
}

view this post on Zulip Kevin Buzzard (May 17 2018 at 17:55):

[this is all your fault @Kenny Lau ]

view this post on Zulip Kevin Buzzard (May 17 2018 at 17:55):

I want to define a function "sup", so I need some classical stuff to pull out witnesses for the exists

view this post on Zulip Kevin Buzzard (May 17 2018 at 17:56):

and I have to run it twice because it's "exists this, such that exists that, such that..."

view this post on Zulip Kevin Buzzard (May 17 2018 at 17:57):

Based on the "it's trivial so write a one-liner in term mode" principle I'd ideally like to write a one-liner in term mode, but writing classical.indefinite_description twice fills up most of the line already :-/

view this post on Zulip Kevin Buzzard (May 17 2018 at 17:57):

Is there a trick I'm missing?

view this post on Zulip Reid Barton (May 17 2018 at 20:51):

This only saves one of your lines, but for ∃ (H : p), q where p is a Prop, check out Exists.fst and Exists.snd.
You can eliminate the second line and change the third to exact ⟨W,⟨HW.snd.1,HW.fst⟩⟩

view this post on Zulip Reid Barton (May 17 2018 at 20:55):

This little detail about how ∃ t₃∈s, ... means ∃ t₃, ∃ H : (t₃∈s), ... is a bit annoying in this case, but using .fst and .snd you can pretty much pretend it actually means ∃ t₃, t₃∈s ∧ ...

view this post on Zulip Kevin Buzzard (May 17 2018 at 21:17):

Here's a mathlib-free version of what I'm moaning about:

view this post on Zulip Kevin Buzzard (May 17 2018 at 21:17):

example (α : Type) (p q : α  Prop) (r : { x : α // p x  q x}  Type) (H :  (x : α) (H1 : p x), q x) : Type :=
begin
  cases (classical.indefinite_description _ H) with x H2,
  cases (classical.indefinite_description _ H2) with H3 H4,
  exact r x,H3,H4
end

view this post on Zulip Reid Barton (May 17 2018 at 21:21):

example (α : Type) (p q : α  Prop) (r : { x : α // p x  q x}  Type) (H :  (x : α) (H1 : p x), q x) : Type :=
begin
  cases (classical.indefinite_description _ H) with x H2,
  exact r x,H2.fst,H2.snd
end

view this post on Zulip Kevin Buzzard (May 17 2018 at 21:21):

Aah I see @Reid Barton -- thanks for these tips.

view this post on Zulip Kevin Buzzard (May 17 2018 at 21:21):

I hadn't really internalised why there were two exists, or the trick with "exists proof".

view this post on Zulip Reid Barton (May 17 2018 at 21:22):

or

let x,H2 := classical.indefinite_description _ H in r x,H2.fst,H2.snd

view this post on Zulip Kevin Buzzard (May 17 2018 at 21:22):

let cases := classical.indefinite_description _ :-/

view this post on Zulip Mario Carneiro (May 17 2018 at 22:52):

I would prefer to do the proof in two stages, first showing it's directed and then extracting the witness

section
variables {X : Type u} [topological_space X] {B : set (set X)}
variables (HB : topological_space.is_topological_basis B) (x : X)
include HB

definition basis_nhds := {U : set X // x ∈ U ∧ U ∈ B}

theorem basis_nhds_directed (U V : basis_nhds HB x) :
  ∃ W : basis_nhds HB x, W.1 ⊆ U.1 ∧ W.1 ⊆ V.1 :=
let ⟨W, h₁, h₂, h₃⟩ := HB.1 _ U.2.2 _ V.2.2 _ ⟨U.2.1, V.2.1⟩ in
⟨⟨W, h₂, h₁⟩, set.subset_inter_iff.1 h₃⟩

noncomputable instance basis_nhds_has_so_called_sup :
  lattice.has_sup (basis_nhds HB x) :=
{ sup := λ Us Vs, classical.some (basis_nhds_directed HB x Us Vs) }
end

You don't need indefinite_description here since you don't need the proof part for the definition

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:01):

Of course I need it the moment I want to prove le_sup_left, but I got distracted by all the function.comp shenannigans in the other thread and never got to this bit :-/

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:03):

This is a much better approach though -- my initial attempt ran into problems when I tried proving le_sup_left because my definition used tactics so wouldn't unfold definitionally when I wanted it to. This is a much better idea.

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:04):

So many tricks still to learn!

view this post on Zulip Mario Carneiro (May 17 2018 at 23:11):

section
variables {X : Type u} [topological_space X] {B : set (set X)}
variables (HB : topological_space.is_topological_basis B) (x : X)
include HB

definition basis_nhds := {U : set X // x ∈ U ∧ U ∈ B}

instance : partial_order (basis_nhds HB x) :=
{ le := λ u v, v.1 ⊆ u.1,
  le_refl := λ u, set.subset.refl u.1,
  le_trans := λ u v w uv vw, set.subset.trans vw uv,
  le_antisymm := λ u v vu uv, subtype.eq $ set.subset.antisymm uv vu }

theorem basis_nhds_directed (U V : basis_nhds HB x) :
  ∃ W : basis_nhds HB x, U ≤ W ∧ V ≤ W :=
let ⟨W, h₁, h₂, h₃⟩ := HB.1 _ U.2.2 _ V.2.2 _ ⟨U.2.1, V.2.1⟩ in
⟨⟨W, h₂, h₁⟩, set.subset_inter_iff.1 h₃⟩

noncomputable instance basis_nhds_has_so_called_sup :
  lattice.has_sup (basis_nhds HB x) :=
{ sup := λ Us Vs, classical.some (basis_nhds_directed HB x Us Vs) }

theorem sup_le_left (u v : basis_nhds HB x) : u ≤ u ⊔ v :=
(classical.some_spec (basis_nhds_directed HB x u v)).1

theorem sup_le_right (u v : basis_nhds HB x) : v ≤ u ⊔ v :=
(classical.some_spec (basis_nhds_directed HB x u v)).2

end

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:12):

Indeed

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:13):

You missed a trick with le_antisymm though

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:13):

Oh actually maybe you didn't

view this post on Zulip Mario Carneiro (May 17 2018 at 23:13):

I guess you can throw a function.swap in there if you want to be "point-free"

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:13):

Because the order is the other way

view this post on Zulip Mario Carneiro (May 17 2018 at 23:14):

but also that circ madness is limited in usefulness since it's nondependent

view this post on Zulip Mario Carneiro (May 17 2018 at 23:14):

so for example it wouldn't work in the definition of sup

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:16):

You mean the HB and x screw it up?

view this post on Zulip Mario Carneiro (May 17 2018 at 23:16):

no, the u and v do - the type of basis_nhds_directed HB x u v depends on them

view this post on Zulip Mario Carneiro (May 17 2018 at 23:17):

if it worked, it would look something like ((∘) ∘ (∘)) classical.some (basis_nhds_directed HB x)

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:17):

So now all I need is for that PR to be accepted :wink:

view this post on Zulip Mario Carneiro (May 17 2018 at 23:17):

There is a dcomp function which is dependent, but I don't think it has nice notation

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:18):

Unfortunately it looks like it might still need some work by someone who is in the middle of exams...

view this post on Zulip Mario Carneiro (May 17 2018 at 23:19):

hm, lean doesn't like ((∘') ∘' (∘'))

view this post on Zulip Kevin Buzzard (May 17 2018 at 23:20):

You're being sucked into the circ madness...

view this post on Zulip Kevin Buzzard (May 18 2018 at 08:26):

So thanks for writing that proof for me Mario. I was completely on top of everything after Reid's comment about this trick for Exists so I knew I could write it, so I did the optimal thing of just writing it all myself anyway and then comparing with what you wrote. I missed the trick with let ⟨W, h₁, h₂, h₃⟩ =... -- I did the expansion using the trick Reid explained later on. But I also didn't use include and I carried HB around with me as an input variable. Aah, I see -- this is why you have used a section; include plays two roles and I'd only appreciated one of them until now. It can be used to insert hypotheses into the context in a tactic proof, but also to include variables into defintions in a section. I'll remark that I just learnt this by searching the pdf of TPIL for include -- I find the sphinx search very disappointing in this regard -- if you search the online docs for include then you just get the unenlightening response that the word is mentioned in every section, and are told the first occurrence of the word in each section; I would in this case far rather see all occurrences so I can try and spot which ones are in code blocks.

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:31):

It tried to read this thread but I still don't understand how to use exists classical stuff. How do you tell Lean about example (X Y : Type) (f : X → Y) : (∀ y : Y, ∃ x : X, f x = y) → (∃ g : Y → X, f ∘ g = id)

view this post on Zulip Reid Barton (Jun 01 2018 at 16:32):

use axiom_of_choice on that hypothesis and then funext

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:50):

Thanks you very much.

example (X Y : Type) (f : X  Y) :  ( y : Y,  x : X, f x = y)  ( g : Y  X, f  g = id) :=
begin
  intro hyp,
  replace hyp := classical.axiom_of_choice hyp,
  cases hyp with g H,
  existsi g,
  funext y,
  exact H y
end

works. I still have questions: is it what you had in mind? is there a simpler solution? can we hide this to mathematicians? can we avoid frightening stuff like ∃ (f_1 : Π (x : Y), (λ (y : Y), X) x), ∀ (x : Y), (λ (y : Y) (x : X), f x = y) x (f_1 x) which is defeq to ∃ f_1 : Y → X, ∀ (x : Y), f (f_1 x) = x?

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:51):

the frightening is what you get from classical.axiom_of_choice hyp

view this post on Zulip Reid Barton (Jun 01 2018 at 16:51):

set_option pp.beta true should help

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:52):

perfect

view this post on Zulip Reid Barton (Jun 01 2018 at 16:52):

And yeah, that's pretty much what I had in mind (or you can write it more succinctly in term mode)

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:53):

Why is this pp.beta not true by default?

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:55):

Is there any way to merge the two lines replace hyp := classical.axiom_of_choice hyp, cases hyp with g H, into one I_really_mean hyp with g H?

view this post on Zulip Reid Barton (Jun 01 2018 at 16:55):

cases can take an expression, so you can inline the redefinition of hyp

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:55):

I tried that and couldn't succeed

view this post on Zulip Reid Barton (Jun 01 2018 at 16:56):

  intro hyp,
  cases classical.axiom_of_choice hyp with g H,
-- etc.

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:56):

Ok, Lean is afraid of you

view this post on Zulip Reid Barton (Jun 01 2018 at 16:56):

or

example (X Y : Type) (f : X  Y) :  ( y : Y,  x : X, f x = y)  ( g : Y  X, f  g = id) :=
assume hyp,
  let g, H := classical.axiom_of_choice hyp in
  g, funext H

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:57):

it didn't work with me before you wrote it

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:57):

I also tried various stuff involving let...

view this post on Zulip Reid Barton (Jun 01 2018 at 16:58):

just remember that everything in term mode is subtly different from the corresponding thing in tactic mode and you should be fine :simple_smile:

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:59):

it's a bit confusing that the funext tactic takes the variable name as argument while the term version takes the quantified equality

view this post on Zulip Patrick Massot (Jun 01 2018 at 17:00):

Anyway, I have to go back home now. Thank you very much Reid!

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 18:00):

Patrick I asked this very question here a month or two ago. Let me see if I can dig out the thread.

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 18:00):

All I remember is that I used the axiom of choice twice and Mario pointed out that I should only be using it once

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 18:02):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cases.20eliminating.20into.20type

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 18:02):

Maybe that will have some relevant material

view this post on Zulip Patrick Massot (Jun 01 2018 at 18:46):

I thought so, bu I found the wrong thread when I searched. Thank you

view this post on Zulip Patrick Massot (Jun 03 2018 at 21:31):

So, @Kevin Buzzard and @Mario Carneiro, should I PR something like:

namespace tactic
namespace interactive
open interactive interactive.types

/--
  `choice hyp with g H` takes an hypothesis `hyp` of the form
  `∀ (y : Y), ∃ (x : X), P x y` for some `P : X → Y → Prop` and outputs into
  context a function `g : Y → X` and a proposition `H` stating
  `∀ (y : Y), P (g y) y`. It presumably also works with dependent versions
  (see the actual type of `classical.axiom_of_choice`)
-/
meta def choice (e : parse cases_arg_p) (ids : parse with_ident_list) :=
do cases (e.1,``(classical.axiom_of_choice %%(e.2))) ids

end interactive
end tactic

example (X Y : Type) (P : X  Y  Prop) :  ( y : Y,  x : X, P x y)  ( g : Y  X,  y, P (g y) y) :=
begin
  intro hyp,
  choice hyp with g H,
  existsi g,
  exact H
end

I know this is purely cosmetic, but I think it would help mathematicians to have a nice interface to choice.

view this post on Zulip Patrick Massot (Jun 03 2018 at 21:32):

Of course this is a version of what Simon wrote in the other thread

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:42):

This is really nice and I want to be showing this to my 1st years.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:42):

It was on my todo list to get this into a xena library.

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:43):

Patrick -- can choice be used to replace cases everywhere?

view this post on Zulip Kevin Buzzard (Jun 03 2018 at 21:47):

@Mario Carneiro it's important we make a good interface for mathematicians, so they can learn more quickly.

view this post on Zulip Kenny Lau (Jun 03 2018 at 21:49):

Skolem normal form?


Last updated: May 12 2021 at 22:15 UTC