Icc_ssubset_Icc

Stream: maths

[Mohamed Al-Fahim]

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]

take a look at tactic#rintro

[Floris van Doorn]

Note: you can remove hypothesis hI₁

[Mohamed Al-Fahim]

Floris van Doorn said:

Note: you can remove hypothesis hI₁

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

[Damiano Testa]

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]

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]

At least any docs#densely_ordered type

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Mohamed Al-Fahim]

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]

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]

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]

The both endpoints lemma is not needed

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

[Mohamed Al-Fahim]

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]

The two endpoints lemma is more general in its conclusion

[Damiano Testa]

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]

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]

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]

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

[Mohamed Al-Fahim]

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]

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

[Mohamed Al-Fahim]

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]

@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]

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]

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]

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

[Mohamed Al-Fahim]

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.

[Floris van Doorn]

invite sent!

[Damiano Testa]

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]

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

[Mohamed Al-Fahim]

@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]

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

[Mohamed Al-Fahim]

yes

[Mohamed Al-Fahim]

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]

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

[Alex J. Best]

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]

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]

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

[Mohamed Al-Fahim]

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

[Johan Commelin]

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?

[Mohamed Al-Fahim]

I am on Mac OS

[Mohamed Al-Fahim]

I have no GitHub SSH keys

[Johan Commelin]

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

[Floris van Doorn]

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?

[Mohamed Al-Fahim]

I will take your suggestion of using SSH

[Mohamed Al-Fahim]

How do I generate one?

[Floris van Doorn]

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]

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

[Floris van Doorn]

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]

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]

Sure, no problem!

[Mohamed Al-Fahim]

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

[Mohamed Al-Fahim]

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

[Alex J. Best]

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.