Zulip Chat Archive

Stream: maths

Topic: Icc_ssubset_Icc


view this post on Zulip Mohamed Al-Fahim (Dec 29 2020 at 03:04):

I am planning on making a pull request to add a lemma similar to the following lemma to mathlib's data.set.intervals.basic:

import data.real.basic


lemma Icc_ssubset_Icc (I₁_s I₁_e I₂_s I₂_e : ) (hI₁ : I₁_s < I₁_e) (hI₂ : I₂_s < I₂_e) : (I₂_s < I₁_s  I₁_e < I₂_e)  (set.Icc I₁_s I₁_e  set.Icc I₂_s I₂_e) :=
begin
  intro h, cases h with hs he,
  have hIcc : set.Icc I₁_s I₁_e  set.Icc I₂_s I₂_e := set.Icc_subset_Icc (by linarith) (by linarith),
  refine (set.ssubset_iff_of_subset hIcc).mpr  I₂_s,  _, by finish  ⟩,
  {
    rw set.left_mem_Icc,
    exact le_of_lt hI₂,
  },
end

But before I transform the lemma above to match the style and structure of the lemmas in data.set.intervals.basic, is there a way to simplify the intro h, cases h with hs he,?

view this post on Zulip Adam Topaz (Dec 29 2020 at 03:07):

take a look at tactic#rintro

view this post on Zulip Floris van Doorn (Dec 29 2020 at 08:26):

Note: you can remove hypothesis hI₁

view this post on Zulip Mohamed Al-Fahim (Dec 29 2020 at 22:37):

Floris van Doorn said:

Note: you can remove hypothesis hI₁

Is there a way to remove hypothesis hI₂ as well?

view this post on Zulip Damiano Testa (Dec 30 2020 at 11:52):

Below is a proof not using finish or linarith of a slightly tightened result. There are several other cases where there is a strict containment that are not taken into account by this lemma. Note that hypothesis hI₂ cannot simply be removed since otherwise there is the possibility that both intervals are empty and therefore the conclusion would be false.

lemma Icc_ssubset_Icc
  (I₁_s I₁_e I₂_s I₂_e : ) (hI₂ : I₂_s  I₂_e) (h : I₂_s < I₁_s  I₁_e  I₂_e) :
  (set.Icc I₁_s I₁_e  set.Icc I₂_s I₂_e) :=
begin
  refine (set.ssubset_iff_of_subset (λ a b, _)).mpr
     I₂_s, (set.left_mem_Icc.mpr hI₂), λ a, not_le.mpr h.1 a.1⟩,
  exact le_trans (le_of_lt h.1) b.1, le_trans b.2 h.2⟩,
end

view this post on Zulip Yury G. Kudryashov (Dec 31 2020 at 20:17):

Note that a lemma in data/set/intervals/basic should deal with any type, not just \R. Is there any reason to use in h instead of 2 assumptions?

view this post on Zulip Reid Barton (Jan 01 2021 at 00:38):

At least any docs#densely_ordered type

view this post on Zulip Yury G. Kudryashov (Jan 01 2021 at 01:44):

The proof uses nothing but the endpoints, so it should work without densely_ordered. Any preorder?

view this post on Zulip Yury G. Kudryashov (Jan 01 2021 at 01:45):

BTW, this proof is about the left endpoint; the PR should include a version about the right endpoint.

view this post on Zulip Mohamed Al-Fahim (Jan 04 2021 at 04:14):

Yury G. Kudryashov said:

Note that a lemma in data/set/intervals/basic should deal with any type, not just \R. Is there any reason to use in h instead of 2 assumptions?

I made the type in the lemma on purpose to make it minimal, but I will make sure to make the pull request version of the lemma work with any type.

view this post on Zulip Mohamed Al-Fahim (Jan 04 2021 at 04:21):

Here's a slightly improved version of the lemma after factoring-in many suggestions:

lemma Icc_ssubset_Icc
  (I₁_s I₁_e I₂_s I₂_e : ) (hI : I₂_s  I₂_e) (hs : I₂_s < I₁_s) (he : I₁_e  I₂_e) :
  (set.Icc I₁_s I₁_e  set.Icc I₂_s I₂_e) :=
begin
  refine (set.ssubset_iff_of_subset (λ a b, _)).mpr
     I₂_s, (set.left_mem_Icc.mpr hI), λ a, not_le.mpr hs a.1⟩,
  exact le_trans (le_of_lt hs) b.1, le_trans b.2 he⟩,
end

view this post on Zulip Mohamed Al-Fahim (Jan 04 2021 at 04:51):

I think there would need to be three lemmas: one for the left endpoint, one for the right endpoint, and one for both endpoints. I forgot that the original lemma was supposed to handle the both endpoints case rather than the left endpoint case.
Edit: The both endpoints lemma is not needed.

view this post on Zulip Mario Carneiro (Jan 04 2021 at 05:08):

The both endpoints lemma is not needed

what do you mean by this? It seems useful enough to me

view this post on Zulip Mohamed Al-Fahim (Jan 04 2021 at 05:09):

Mario Carneiro said:

The both endpoints lemma is not needed

what do you mean by this? It seems useful enough to me

I think the left endpoint lemma can be used wherever the both endpoints lemma can be used.

view this post on Zulip Mario Carneiro (Jan 04 2021 at 05:34):

The two endpoints lemma is more general in its conclusion

view this post on Zulip Damiano Testa (Jan 04 2021 at 07:55):

A different generalization of the case, would be strict containment of closed balls in a metric space. Those lemmas might also be useful, unless they are already in mathlib!

view this post on Zulip Ruben Van de Velde (Jan 04 2021 at 13:02):

Your slightly improved version looks like it's one step away from a term-mode proof, so you might as well go there :)

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 02:38):

I have partially transformed the lemma to match the lemmas in data.set.intervals.basic:

lemma Icc_ssubset_Icc_left
  (hI : a₂  b₂) (ha : a₂ < a₁) (hb : b₁  b₂) :
  (set.Icc a₁ b₁  set.Icc a₂ b₂) :=
begin
  refine (set.ssubset_iff_of_subset (λ m n, _)).mpr
     a₂, (set.left_mem_Icc.mpr hI), λ m, not_le.mpr ha m.1 ⟩,
  exact le_trans (le_of_lt ha) n.1, le_trans n.2 hb⟩,
end

and put it between Ico_subset_Ici_self and Icc_subset_Icc_iff. But for some reason, the line:

 a₂, (set.left_mem_Icc.mpr hI), λ m, not_le.mpr ha m.1 ⟩,

is causing the error:

type mismatch at application
  not_le.mpr ha
term
  ha
has type
  a₂ < a₁
but is expected to have type
  ?m_3 < ?m_4
state:
α : Type u,
_inst_1 : preorder α,
a₁ a₂ b₁ b₂ : α,
hI : a₂ ≤ b₂,
ha : a₂ < a₁,
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 02:42):

Otherwise, replacing not_le.mpr ha m.1 with sorry causes no further errors.

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 03:26):

I managed to prove the lemma with a completely different proof:

lemma Icc_ssubset_Icc_left
  (hI : a₂  b₂) (ha : a₂ < a₁) (hb : b₁  b₂) :
  set.Icc a₁ b₁  set.Icc a₂ b₂ :=
begin
  have h : set.Icc a₁ b₁  set.Icc a₂ b₂ := Icc_subset_Icc (le_of_lt ha) hb,
  refine (ssubset_iff_of_subset h).mpr _,
  use a₂,
  rw mem_Icc,
  rw mem_Icc,
  split,
  {
    tauto,
  },
  {
    have hs : ¬(a₁  a₂) := not_le_of_gt ha,
    tauto,
  },
end

I will now try to make it smaller.

view this post on Zulip Alex J. Best (Jan 05 2021 at 03:35):

Nice, I'd write refine (ssubset_iff_of_subset h).mpr _, as rw ssubset_iff_of_subset h

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 03:52):

lemma Icc_ssubset_Icc_left
  (hI : a₂  b₂) (ha : a₂ < a₁) (hb : b₁  b₂) :
  set.Icc a₁ b₁  set.Icc a₂ b₂ :=
begin
  have h : set.Icc a₁ b₁  set.Icc a₂ b₂ := Icc_subset_Icc (le_of_lt ha) hb,
  rw ssubset_iff_of_subset h,
  use a₂,
  rw [mem_Icc, mem_Icc],
  have h₂ : ¬(a₁  a₂) := not_le_of_gt ha,
  tauto,
end

lemma Icc_ssubset_Icc_right
  (hI : a₂  b₂) (ha : a₂  a₁) (hb : b₁ < b₂) :
  set.Icc a₁ b₁  set.Icc a₂ b₂ :=
begin
  have h : set.Icc a₁ b₁  set.Icc a₂ b₂ := Icc_subset_Icc ha (le_of_lt hb),
  rw ssubset_iff_of_subset h,
  use b₂,
  rw [mem_Icc, mem_Icc],
  have h₂ : ¬(b₂  b₁) := not_le_of_gt hb,
  tauto,
end

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 04:25):

@Alex J. Best @Floris van Doorn Would you be okay if I added you as co-authors of the PR's commit?

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 04:26):

The final version of the code is:

lemma Icc_ssubset_Icc_left (hI : a₂  b₂) (ha : a₂ < a₁) (hb : b₁  b₂) :
  Icc a₁ b₁  Icc a₂ b₂ :=
begin
  have h : Icc a₁ b₁  Icc a₂ b₂ := Icc_subset_Icc (le_of_lt ha) hb,
  rw ssubset_iff_of_subset h,
  use a₂,
  rw [mem_Icc, mem_Icc],
  have h₂ : ¬(a₁  a₂) := not_le_of_gt ha,
  tauto,
end

lemma Icc_ssubset_Icc_right (hI : a₂  b₂) (ha : a₂  a₁) (hb : b₁ < b₂) :
  Icc a₁ b₁  Icc a₂ b₂ :=
begin
  have h : Icc a₁ b₁  Icc a₂ b₂ := Icc_subset_Icc ha (le_of_lt hb),
  rw ssubset_iff_of_subset h,
  use b₂,
  rw [mem_Icc, mem_Icc],
  have h₂ : ¬(b₂  b₁) := not_le_of_gt hb,
  tauto,
end

view this post on Zulip Alex J. Best (Jan 05 2021 at 04:35):

Mohamed Al-Fahim said:

Alex J. Best Floris van Doorn Would you be okay if I added you as co-authors of the PR's commit?

If you want to thats fine with me, but I don't mind if you don't as I didn't contribute much to your work at all, it was mostly your proof still!

view this post on Zulip Floris van Doorn (Jan 05 2021 at 04:42):

Yeah, I have the same thought. Feel free to either include me or not include me.

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 04:44):

In that case, the commit message will be:

feat(data/set/intervals): add 2 Icc ssubset lemmas

Add two strict subset lemmas for Icc, discussed in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Icc_ssubset_Icc.

@maintainers May I have push permission? My GitHub username is MohamedAlFahim.

view this post on Zulip Floris van Doorn (Jan 05 2021 at 04:49):

invite sent!

view this post on Zulip Damiano Testa (Jan 05 2021 at 04:49):

There are term mode versions of your proofs!

import data.set.intervals.basic

variables {R : Type*} [preorder R] {a₂ b₂ a₁ b₁ : R}
open set

lemma Icc_ssubset_Icc_left (hI : a₂  b₂) (ha : a₂ < a₁) (hb : b₁  b₂) :
  Icc a₁ b₁  Icc a₂ b₂ :=
(ssubset_iff_of_subset (Icc_subset_Icc (le_of_lt ha) hb)).mpr
  a₂, left_mem_Icc.mpr hI, not_and.mpr (λ f g, lt_irrefl a₂ (lt_of_lt_of_le ha f))⟩

lemma Icc_ssubset_Icc_right (hI : a₂  b₂) (ha : a₂  a₁) (hb : b₁ < b₂) :
  Icc a₁ b₁  Icc a₂ b₂ :=
(ssubset_iff_of_subset (Icc_subset_Icc ha (le_of_lt hb))).mpr
  b₂, right_mem_Icc.mpr hI, (λ f, lt_irrefl b₁ (lt_of_lt_of_le hb f.2))⟩

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 04:56):

@Damiano Testa I will make sure to add your version in the next commit

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 04:58):

@Floris van Doorn Running git push --set-upstream origin interval_ssubset (I named the branch interval_ssubset) gives:

remote: Permission to leanprover-community/mathlib.git denied to MohamedAlFahim.
fatal: unable to access 'https://github.com/leanprover-community/mathlib.git/': The requested URL returned error: 403

view this post on Zulip Alex J. Best (Jan 05 2021 at 04:59):

Did you visit https://github.com/leanprover-community/mathlib/invitations and accept?

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 04:59):

yes

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:02):

I will install the GitHub Pull Requests and Issues extension then try again to see if that would fix it.
Edit: It didn't fix it, and the extension won't even let me sign in to GitHub. Is there a workaround I can use, besides using the GitHub UI to edit the files?

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:18):

I will try pushing to a fork instead, then make a PR

view this post on Zulip Alex J. Best (Jan 05 2021 at 05:20):

I'm guessing something is up with your permissions on github, do you have the right ssh keys for the computer you are on added to github? You could try to configure git to use the git protocol rather than https with git remote set-url origin git@github.com:leanprover-community/mathlib.git

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:26):

The error message now after running git push --set-upstream origin interval_ssubset is

git@github.com: Permission denied (publickey).
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:26):

I think the GitHub UI is my only option at this point :sweat_smile:

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:29):

@Alex J. Best I really appreciate your kind effort!

view this post on Zulip Johan Commelin (Jan 05 2021 at 05:35):

Mohamed Al-Fahim said:

Floris van Doorn Running git push --set-upstream origin interval_ssubset (I named the branch interval_ssubset) gives:

remote: Permission to leanprover-community/mathlib.git denied to MohamedAlFahim.
fatal: unable to access 'https://github.com/leanprover-community/mathlib.git/': The requested URL returned error: 403

@Mohamed Al-Fahim what system are you on? Linux/Mac/Windows? Do you have ssh keys on Github?

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:36):

I am on Mac OS

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:37):

I have no GitHub SSH keys

view this post on Zulip Johan Commelin (Jan 05 2021 at 05:38):

Aha... you might want to have those anyways. They will make your life a lot easier.

view this post on Zulip Floris van Doorn (Jan 05 2021 at 05:38):

I personally authenticate with SSH, and you seem to authenticate with HTTPS. So I'm not too familiar with what the problem could be.
You did enter your Github login info before/after pushing?

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:39):

I will take your suggestion of using SSH

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 05:39):

How do I generate one?

view this post on Zulip Floris van Doorn (Jan 05 2021 at 05:39):

SSH takes a little bit to setup (but Github has detailed guides on how to do it). The advantage is that after you have set it up you can authenticate yourself once with ssh-add and then fetch/push an unlimited number of times.

view this post on Zulip Floris van Doorn (Jan 05 2021 at 05:40):

https://docs.github.com/en/free-pro-team@latest/github/authenticating-to-github/connecting-to-github-with-ssh

view this post on Zulip Floris van Doorn (Jan 05 2021 at 05:41):

You will also have to run (in your mathlib dir) git remote set-url origin git@github.com:leanprover-community/mathlib.git at some point (this tells git to connect to mathlib via SSH) (this URL can be found on https://github.com/leanprover-community/mathlib under downloading code > SSH)

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 06:37):

Damiano Testa said:

There are term mode versions of your proofs!

import data.set.intervals.basic

variables {R : Type*} [preorder R] {a₂ b₂ a₁ b₁ : R}
open set

lemma Icc_ssubset_Icc_left (hI : a₂  b₂) (ha : a₂ < a₁) (hb : b₁  b₂) :
  Icc a₁ b₁  Icc a₂ b₂ :=
(ssubset_iff_of_subset (Icc_subset_Icc (le_of_lt ha) hb)).mpr
  a₂, left_mem_Icc.mpr hI, not_and.mpr (λ f g, lt_irrefl a₂ (lt_of_lt_of_le ha f))⟩

lemma Icc_ssubset_Icc_right (hI : a₂  b₂) (ha : a₂  a₁) (hb : b₁ < b₂) :
  Icc a₁ b₁  Icc a₂ b₂ :=
(ssubset_iff_of_subset (Icc_subset_Icc ha (le_of_lt hb))).mpr
  b₂, right_mem_Icc.mpr hI, (λ f, lt_irrefl b₁ (lt_of_lt_of_le hb f.2))⟩

Would you be fine if I added you as a co-author to a commit?

view this post on Zulip Damiano Testa (Jan 05 2021 at 06:44):

Sure, no problem!

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 06:58):

@Floris van Doorn SSH solved the problem. Thank you!

view this post on Zulip Mohamed Al-Fahim (Jan 05 2021 at 06:58):

Here's the Pull Request: https://github.com/leanprover-community/mathlib/pull/5617.

view this post on Zulip Alex J. Best (Jan 05 2021 at 09:12):

Mohamed Al-Fahim said:

Here's the Pull Request: https://github.com/leanprover-community/mathlib/pull/5617.

If you'd like people to review it, you should tag the PR with "awaiting-review" otherwise people may not see it.


Last updated: May 11 2021 at 00:31 UTC