Zulip Chat Archive
Stream: general
Topic: fun with intervals
Patrick Massot (Jul 28 2020 at 17:43):
Are there people here that think the following is a nice game to play?
example {α : Type*} [linear_order α] {a b : α} (h : a < b) :
Icc a b \ Ioo a b = {a, b} :=
sorry
Johan Commelin (Jul 28 2020 at 17:46):
don't know how to synthesize placeholder
context:
α : Type ?,
_inst_1 : linear_order α,
a b : α,
h : a < b,
x : α
⊢ Type ?
after
import data.set.intervals.basic
open set
Patrick Massot (Jul 28 2020 at 17:47):
I'm sorry, Johan, I can't reproduce that.
Patrick Massot (Jul 28 2020 at 17:48):
And I'm also sorry for not including the import and open.
Sebastien Gouezel (Jul 28 2020 at 17:48):
Same as Johan.
Patrick Massot (Jul 28 2020 at 17:48):
import data.set.intervals.basic
open set
example {α : Type*} [linear_order α] {a b : α} (h : a < b) :
Icc a b \ Ioo a b = {a, b} :=
begin
sorry
end
Patrick Massot (Jul 28 2020 at 17:48):
This works here.
Patrick Massot (Jul 28 2020 at 17:49):
On mathlib 9e841c81756b12d797f96baed2158ad12233e414
Johan Commelin (Jul 28 2020 at 17:50):
Putting a type ascription on the RHS solves it for me
Sebastien Gouezel (Jul 28 2020 at 17:55):
lemma foo {α : Type*} [linear_order α] {a b : α} (h : a < b) (x : α) :
(x ∈ Icc a b \ Ioo a b) ↔ x ∈ ({a, b} : set α) :=
begin
by_cases h' : a < x,
{ simp [h', ne_of_gt h'],
split;
simp [le_antisymm_iff, le_of_lt h'] {contextual := tt} },
{ push_neg at h',
simp [h', ne_of_lt (lt_of_le_of_lt h' h), le_trans h' (le_of_lt h)],
simp [le_antisymm_iff, h'] }
end
Patrick Massot (Jul 28 2020 at 17:56):
Thank you very much Sébastien. It's very depressing to see, but helpful.
Johan Commelin (Jul 28 2020 at 17:58):
example {α : Type*} [linear_order α] {a b : α} (h : a < b) (x : α) :
x ∈ Icc a b \ Ioo a b ↔ x ∈ ({a, b} : set α) :=
begin
classical, -- because, duh
-- tidy says:
simp at *, fsplit, work_on_goal 0 { intros a_1, cases a_1, cases a_1_left }, work_on_goal 1 { intros a_1, cases a_1, work_on_goal 0 { induction a_1, simp at *, fsplit, work_on_goal 0 { refl } }, work_on_goal 1 { induction a_1, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { refl } }, work_on_goal 1 { intros a_1, refl } } },
{ rw or_iff_not_imp_left,
intros a_1, -- tidy says: -- :sad:
have : a < x, refine lt_of_le_of_ne a_1_left_left (ne.symm a_1), -- library_search
-- tidy says: no progress
apply le_antisymm,
{ assumption, }, -- tidy
{ -- tidy takes a looooong time
solve_by_elim, }, },
{ refine le_of_lt h, }, -- library_search
{ refine le_of_lt h, }, -- library_search
end
Johan Commelin (Jul 28 2020 at 18:00):
Out of curiousity... is there a reason for double spacing the assumptions?
Sebastien Gouezel (Jul 28 2020 at 18:00):
I have a much better proof:
lemma auto_is_strong:
fixes a b x::"'a::linorder"
assumes "a < b"
shows "(x ∈ ({a .. b} - {a <..< b})) ⟷ (x ∈ {a, b})"
using ‹a < b› by auto
Johan Commelin (Jul 28 2020 at 18:01):
Is auto not just relying on a lemma that is already in the library?
Sebastien Gouezel (Jul 28 2020 at 18:02):
All the interval lemmas in Isabelle library are proved by auto like this, and none of them is marked simp or whatever.
Johan Commelin (Jul 28 2020 at 18:04):
It's a bit sad that solve_by_elim [le_antisymm]
failed after my have
statement
Patrick Massot (Jul 28 2020 at 18:05):
I almost asked the Isabelle question explicitly but I thought it was clear. I means there is hope.
Patrick Massot (Jul 28 2020 at 18:06):
I understand why all those Isabelle people at the CICM conference are laughing at us. But we can hope that Lean will improve in this direction whereas they have no hope to get rid of their foundational issues, so let's wait.
Johan Commelin (Jul 28 2020 at 18:06):
Slightly "better" version:
example {α : Type*} [linear_order α] {a b : α} (h : a < b) (x : α) :
x ∈ Icc a b \ Ioo a b ↔ x ∈ ({a, b} : set α) :=
begin
classical, -- because, duh
-- tidy says:
simp at *, fsplit, work_on_goal 0 { intros a_1, cases a_1, cases a_1_left }, work_on_goal 1 { intros a_1, cases a_1, work_on_goal 0 { induction a_1, simp at *, fsplit, work_on_goal 0 { refl } }, work_on_goal 1 { induction a_1, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { refl } }, work_on_goal 1 { intros a_1, refl } } },
{ rw or_iff_not_imp_left,
intros a_1, -- tidy -- :sad:
apply le_antisymm,
{ solve_by_elim, },
{ -- solve_by_elim fails
apply_assumption,
refine lt_of_le_of_ne a_1_left_left (ne.symm a_1), -- library_search
}, },
{ refine le_of_lt h, }, -- library_search
{ refine le_of_lt h, }, -- library_search
end
Patrick Massot (Jul 28 2020 at 18:08):
I'm sorry, trying to put that lemma in the proper place in mathlib, I realized it's already there :sad:. So it's again automation failure. The point is my inequality is too strong, a less or equal is enough.
Patrick Massot (Jul 28 2020 at 18:09):
And also set.intervals.basic
is missing a lot of simp
attributes.
Kenny Lau (Jul 29 2020 at 01:11):
import data.set.intervals.basic
open set
example {α : Type*} [linear_order α] {a b : α} (h : a < b) :
Icc a b \ Ioo a b = {a, b} :=
Icc_diff_Ioo_same $ le_of_lt h
Last updated: Dec 20 2023 at 11:08 UTC