Being stuck -> MWE

Stream: general

[Kevin Buzzard]

I am stuck on a proof. I'm in the middle of a begin-end block in a work in progress in a medium size project but I don't need all the crap around me because my problem is simply this:

a b c d x: ℝ
h: a ≤ b
h_1: ¬d ≤ c
h1: a ≤ d
h_2: c ≤ d
h_3: ¬b ≤ a
h2: c ≤ b
h_4: ¬a ≤ c
h3: c ≤ x
h_5: d ≤ b
h4: x < b
h5: x < b
⊢ x ∈ {x : ℝ | a ≤ x ∧ x < b} ∪ {x : ℝ | c ≤ x ∧ x < d}

I want to efficiently turn this into a MWE so I can e.g. talk to people about it on Zulip. The bad news is that I have managed to get myself to this goal by doing something called "programming", a subject which I know sod all about, and hence whenever I press a key I then have to wait for about 20 seconds before Lean says anything.
Is there a tactic which I can run which would turn the infoview output, or the current goal, into an explicit term of type Prop?
PS (see edit history) why are my variables coaslecing above when I cut and paste from a Lean infoview?

[Kenny Lau]

if your proof takes 20 seconds then you're doing it wrong?

[Kenny Lau]

cf the interval arithmetic

[Kevin Buzzard]

yes i know I'm doing it wrong

[Kevin Buzzard]

import tactic
import data.real.basic

open set

lemma Ico_union_Ico {a b c d : ℝ}
  (h1 : min a b ≤ max c d) (h2 : min c d ≤ max a b) :
  Ico a b ∪ Ico c d = Ico (min a c) (max b d) :=
begin
  ext x,
  split,
  all_goals {intro h},
  all_goals {try {cases h with h3 h4}},
  all_goals {unfold min max Ico at *},
  -- split_ifs at * leads to a weird state with multiple copies of variables :-(
  all_goals {try {split_ifs at h1}},
  all_goals {try {split_ifs at h2}},
  all_goals {try {split_ifs at h3}},
  all_goals {try {split_ifs at h4}},
  all_goals {try {split_ifs}},
  all_goals {try {split}},
  -- 144 goals at this point
  all_goals {try {cases h3}},
  all_goals {try {cases h4}},
  all_goals {try {linarith}},
  all_goals {try {left, split; linarith}},
  all_goals {try {right, split; linarith}},
  -- two left
  all_goals {by_cases h5 : x < b},
  all_goals {try {left, split; linarith}},
  all_goals {try {right, split; linarith}},
  /-
  abcdx: ℝ
h: a ≤ b
h_1: c ≤ d
h1: a ≤ d
h_2: c ≤ d
h2: c ≤ b
h_3: ¬a ≤ c
h3: c ≤ x
h_4: ¬b ≤ d
h4: x < b
h5: x < b
⊢ x ∈ {x : ℝ | a ≤ x ∧ x < b} ∪ {x : ℝ | c ≤ x ∧ x < d}
-/
  sorry
end

[Utensil Song]

tactic#extract_goal ?

[Kevin Buzzard]

I searched through tactics tagged debugging and I did not find this! Can we add the debugging tag to extract_goal?

[Kevin Buzzard]

@Kenny Lau I want to understand why I got lost in this maze

[Kevin Buzzard]

and whether I can find my way out.

[Kenny Lau]

did you look at my answer to the previous interval arithmetic question?

[Kevin Buzzard]

I think pretty much every move is reversible except when I went left or right

[Kevin Buzzard]

show me!

[Kevin Buzzard]

MWE!

import tactic
import data.real.basic

open set
example {a b c d : ℝ} (x : ℝ)
  (h : a ≤ b)
  (h_1 : ¬d ≤ c)
  (h1 : a ≤ d)
  (h_2 : c ≤ d)
  (h_3 : ¬b ≤ a)
  (h2 : c ≤ b)
  (h_4 : ¬a ≤ c)
  (h3 : c ≤ x)
  (h_5 : d ≤ b)
  (h4 : x < b)
  (h5 : x < b) :
  x ∈ {x : ℝ | a ≤ x ∧ x < b} ∪ {x : ℝ | c ≤ x ∧ x < d} :=
begin
  admit,
end

[Kenny Lau]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/golfing.20.60Ico.60.20union/near/205047162

[Kenny Lau]

I used set.subset.antisymm and interval arithmetic

[Kenny Lau]

specifically, Ico a b subset Ico a c U Ico c b

[Kenny Lau]

so in this case (Ico a b ∪ Ico c d = Ico (min a c) (max b d)) the forward direction is trivial, and for the backward direction I suspect we decompose LHS into (Ico a (max a c) U Ico (max a c) (min b d) U Ico (min b d) b) U etc. and RHS into Ico (min a c) (max a c) U Ico (max a c) (min b d) U Ico (min b d) (max b d)

[Kenny Lau]

basically partition at max a c and min b d

[Kenny Lau]

the first term Ico (min a c) (max a c) will be equal to Ico a (max a c) or Ico c (max a c) (I can't think of a solution that avoids equality and/or casing)

[Kenny Lau]

the second term Ico (max a c) (min b d) is contained in Ico a b

[Kenny Lau]

the third term is similar to the first term

[Kenny Lau]

wait @Kevin Buzzard are your hypotheses correct?

[Kevin Buzzard]

I don't know.

[Kevin Buzzard]

I was just experimenting with this kind of stuff.

[Utensil Song]

Kevin Buzzard said:

I searched through tactics tagged debugging and I did not find this! Can we add the debugging tag to extract_goal?

I first PRed this: leanprover-community/leanprover-community.github.io#105 to improve #mwe, will also add debugging tag to extract_goal later.

[Kevin Buzzard]

Hey would a counterexample-finder be able to find a counterexample for me?

[Kenny Lau]

oh I can't partition the LHS when I'm proving the backward direction

[Kenny Lau]

but I think my partition of the RHS into Ico (min a c) (max a c) U Ico (max a c) (min b d) U Ico (min b d) (max b d) is fine

[Kenny Lau]

@Kevin Buzzard I think the hypothesis should be a <= d and c <= b?

[Kenny Lau]

to rule out the picture [a,b) U [c,d) we need c <= b; to rule out the picture [c,d) U [a,b) we need a <= d

[Kevin Buzzard]

but now I want you to prove \not what I wrote.

[Kevin Buzzard]

is there a tactic which does that?

[Kevin Buzzard]

I'm not interested in pictures

[Eric Wieser]

So essentially you want a tactic which produces a hypothesis h : false?

[Eric Wieser]

I assume something dumb like have h : false := by finish doesn't work, but might be a general tactic for "I think my goal might be false after all"

[Kevin Buzzard]

right. It's clear that there are basically $4!$ cases, so try all orders.

[Kenny Lau]

I remember seeing some PR about a tactic finding contradiction

[Kenny Lau]

but I forgot the name

[Kenny Lau]

because I remember that the name was somewhat convoluted

[Kevin Buzzard]

Hey I could negate my goal by reverting a b c d and using extract_goal.

import tactic

open set
universe u
example {α : Type u}
  [decidable_linear_order α] :
¬  (∀ {a b c d : α},
    min a b ≤ max c d →
    min c d ≤ max a b → Ico a b ∪ Ico c d = Ico (min a c) (max b d)) :=
begin
  finish -- fails,
end

[Kevin Buzzard]

Kenny has tried to solve this using pen and paper, and I just want it resolved because I can see it's just "check 24 cases"

[Kenny Lau]

import tactic
import data.real.basic

open set

meta def unions' : tactic unit :=
`[try { refl' <|> { apply subset_union_of_subset_left, unions' } <|> { apply subset_union_of_subset_right, unions' }}]

meta def unions : tactic unit :=
`[{ apply union_subset; unions } <|> unions']

lemma Ico_subset_of {α : Type*} [linear_order α] {x z : α} (y : α) {s : set α}
  (h1 : Ico x y ⊆ s) (h2 : Ico y z ⊆ s) : Ico x z ⊆ s :=
subset.trans Ico_subset_Ico_union_Ico $ union_subset h1 h2

lemma Ico_union_Ico {a b c d : ℝ} (had : a ≤ d) (hcb : c ≤ b) :
  Ico a b ∪ Ico c d = Ico (min a c) (max b d) :=
begin
  refine subset.antisymm
    (union_subset
      (Ico_subset_Ico (min_le_left a c) (le_max_left b d))
      (Ico_subset_Ico (min_le_right a c) (le_max_right b d)))
    (Ico_subset_of (max a c) _ $ Ico_subset_of (min b d) _ _),
  { show Ico (min a c) (max a c) ⊆ Ico a b ∪ Ico c d,
    cases le_total a c with hac hca,
    { rw [min_eq_left hac, max_eq_right hac, ← Ico_union_Ico_eq_Ico hac hcb], unions' },
    { rw [min_eq_right hca, max_eq_left hca, ← Ico_union_Ico_eq_Ico hca had], unions' } },
  { show Ico (max a c) (min b d) ⊆ Ico a b ∪ Ico c d,
    exact subset_union_of_subset_left (Ico_subset_Ico (le_max_left a c) (min_le_left b d)) _, },
  { show Ico (min b d) (max b d) ⊆ Ico a b ∪ Ico c d,
    cases le_total b d with hbd hdb,
    { rw [min_eq_left hbd, max_eq_right hbd, ← Ico_union_Ico_eq_Ico hcb hbd], unions' },
    { rw [min_eq_right hdb, max_eq_left hdb, ← Ico_union_Ico_eq_Ico had hdb], unions' } }
end

[Kenny Lau]

@Kevin Buzzard there you go

[Kenny Lau]

Kevin Buzzard said:

Kenny has tried to solve this using pen and paper, and I just want it resolved because I can see it's just "check 24 cases"

and my point, as is the same as in the previous question, is that there is a better proof than just checking 24 cases

[Kevin Buzzard]

hey look what I found

[Kenny Lau]

nice

[Kevin Buzzard]

@Gabriel Ebner I can prove these questions are decidable so can you decide them for me please?

[Gabriel Ebner]

I thought we decided that somebody should implement auto.

[Kenny Lau]

@Gabriel Ebner do you remember what's the tactic being PR'ed that finds counter-examples?

[Kenny Lau]

or PR'ed

[Gabriel Ebner]

slimcheck slim_check

[Gabriel Ebner]

#2080

[Kenny Lau]

yes that's it

[Kenny Lau]

no way I can remember the name

[Kenny Lau]

@Kevin Buzzard even better, can we prove (using tactics) that this statement reduces to a statement over fin 4?

[Kenny Lau]

is there a mathematical proof using model theory?

[Kenny Lau]

I claim that fin n reflects every sentence in the theory of linear orders involving n quantifiers?

[Kenny Lau]

i.e. if $\varphi$ is a sentence in the theory of linear orders with $n$ quantifiers then $(\vdash \varphi) \iff (\mathsf{fin}~n \vDash \varphi)$

[Gabriel Ebner]

How about $\exists x_1 \cdots \exists x_n (x_1 < \cdots < x_n)$?

[Kenny Lau]

right

[Kenny Lau]

hmm I don't know how to fix my statement

[Kenny Lau]

maybe have it be $n$ universal quantifiers followed by a quantifier-less formula

[Mario Carneiro]

maybe n+1 quantifiers?

[Mario Carneiro]

or rather, the statement may be true with n quantifiers in fin (n+1)

[Mario Carneiro]

ah, that doesn't work either, $\forall x,\exists y_1\dots\exists y_n, (x<y_1<\dots<y_n)\lor (x>y_1>\dots>y_n)$ is true only if the domain has at least 2n+1 elements

[Mario Carneiro]

and you can surely iterate it to get exponential size, although the quantifier complexity grows

[Utensil Song]

Utensil Song said:

Kevin Buzzard said:

I searched through tactics tagged debugging and I did not find this! Can we add the debugging tag to extract_goal?

I first PRed this: leanprover-community/leanprover-community.github.io#105 to improve #mwe, will also add debugging tag to extract_goal later.

#3708

[Peter Jipsen]

import tactic
import data.real.basic

example {a b c d : ℝ} (x : ℝ)
  (h : a ≤ b)
  (h_1 : ¬d ≤ c)
  (h1 : a ≤ d)
  (h_2 : c ≤ d)
  (h_3 : ¬b ≤ a)
  (h2 : c ≤ b)
  (h_4 : ¬a ≤ c)
  (h3 : c ≤ x)
  (h_5 : d ≤ b)
  (h4 : x < b)
  (h5 : x < b) :
  (a ≤ x ∧ x < b) ∨ (c ≤ x ∧ x < d) :=
begin
  finish
end

This works, so is the issue to find an explicit proof? I'm probably misunderstanding something...

[Kevin Buzzard]

Oh no, I didn't know finish did this. I am not very good with finish.

[Kevin Buzzard]

Thanks!

[Alex J. Best]

Sorry not up to date on this thread and not at my computer but. Does linarith work on or statements? Alternatively does linarith work if you apply (\not P \to Q) \to P\or Q first?

[Jalex Stark]

huh. This proof doesn't work,

import tactic
import data.real.basic
example {a b c d : ℝ} (x : ℝ)
  (h : a ≤ b)(h_1 : ¬d ≤ c)  (h1 : a ≤ d)  (h_2 : c ≤ d)  (h_3 : ¬b ≤ a)  (h2 : c ≤ b)  (h_4 : ¬a ≤ c)  (h3 : c ≤ x)  (h_5 : d ≤ b)  (h4 : x < b)  (h5 : x < b) :
  (a ≤ x ∧ x < b) ∨ (c ≤ x ∧ x < d) :=
begin
  rw classical.or_iff_not_imp_left,
  push_neg,
  finish,
end

even though this one does

begin
  rw classical.or_iff_not_imp_left,
  finish,
end