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