## Stream: maths

### Topic: Icc_ssubset_Icc

#### 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,?

#### Adam Topaz (Dec 29 2020 at 03:07):

take a look at tactic#rintro

#### Floris van Doorn (Dec 29 2020 at 08:26):

Note: you can remove hypothesis hI₁

#### 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?

#### 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


#### 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?

#### Reid Barton (Jan 01 2021 at 00:38):

At least any docs#densely_ordered type

#### 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?

#### 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.

#### 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.

#### 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


#### 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.

#### 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

#### 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.

#### Mario Carneiro (Jan 04 2021 at 05:34):

The two endpoints lemma is more general in its conclusion

#### 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!

#### 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 :)

#### 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₂


#### Mohamed Al-Fahim (Jan 05 2021 at 02:42):

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

#### 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.

#### 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

#### 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


#### 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?

#### 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


#### 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!

#### 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.

#### 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.

invite sent!

#### 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))⟩


#### Mohamed Al-Fahim (Jan 05 2021 at 04:56):

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

#### 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


#### Alex J. Best (Jan 05 2021 at 04:59):

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

yes

#### 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?

#### Mohamed Al-Fahim (Jan 05 2021 at 05:18):

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

#### 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

#### 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.


#### Mohamed Al-Fahim (Jan 05 2021 at 05:26):

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

#### Mohamed Al-Fahim (Jan 05 2021 at 05:29):

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

#### 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?

I am on Mac OS

#### Mohamed Al-Fahim (Jan 05 2021 at 05:37):

I have no GitHub SSH keys

#### Johan Commelin (Jan 05 2021 at 05:38):

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

#### 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.

#### Mohamed Al-Fahim (Jan 05 2021 at 05:39):

I will take your suggestion of using SSH

#### Mohamed Al-Fahim (Jan 05 2021 at 05:39):

How do I generate one?

#### 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.

#### 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

#### 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)

#### 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?

#### Damiano Testa (Jan 05 2021 at 06:44):

Sure, no problem!

#### Mohamed Al-Fahim (Jan 05 2021 at 06:58):

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

#### Mohamed Al-Fahim (Jan 05 2021 at 06:58):

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

#### 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