## Stream: general

### Topic: Being stuck -> MWE

#### Kevin Buzzard (Aug 06 2020 at 10:29):

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 (Aug 06 2020 at 10:31):

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

#### Kenny Lau (Aug 06 2020 at 10:31):

cf the interval arithmetic

#### Kevin Buzzard (Aug 06 2020 at 10:32):

yes i know I'm doing it wrong

#### Kevin Buzzard (Aug 06 2020 at 10:32):

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


#### Kevin Buzzard (Aug 06 2020 at 10:34):

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

#### Kevin Buzzard (Aug 06 2020 at 10:35):

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

#### Kevin Buzzard (Aug 06 2020 at 10:35):

and whether I can find my way out.

#### Kenny Lau (Aug 06 2020 at 10:35):

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

#### Kevin Buzzard (Aug 06 2020 at 10:36):

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

show me!

#### Kevin Buzzard (Aug 06 2020 at 10:37):

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
end


#### Kenny Lau (Aug 06 2020 at 10:38):

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

#### Kenny Lau (Aug 06 2020 at 10:38):

I used set.subset.antisymm and interval arithmetic

#### Kenny Lau (Aug 06 2020 at 10:38):

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

#### Kenny Lau (Aug 06 2020 at 10:47):

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 (Aug 06 2020 at 10:47):

basically partition at max a c and min b d

#### Kenny Lau (Aug 06 2020 at 10:48):

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 (Aug 06 2020 at 10:50):

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

#### Kenny Lau (Aug 06 2020 at 10:50):

the third term is similar to the first term

#### Kenny Lau (Aug 06 2020 at 10:52):

wait @Kevin Buzzard are your hypotheses correct?

I don't know.

#### Kevin Buzzard (Aug 06 2020 at 10:53):

I was just experimenting with this kind of stuff.

#### Utensil Song (Aug 06 2020 at 10:53):

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 (Aug 06 2020 at 10:54):

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

#### Kenny Lau (Aug 06 2020 at 10:55):

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

#### Kenny Lau (Aug 06 2020 at 10:55):

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 (Aug 06 2020 at 10:55):

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

#### Kenny Lau (Aug 06 2020 at 10:56):

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 (Aug 06 2020 at 10:57):

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

#### Kevin Buzzard (Aug 06 2020 at 10:57):

is there a tactic which does that?

#### Kevin Buzzard (Aug 06 2020 at 10:57):

I'm not interested in pictures

#### Eric Wieser (Aug 06 2020 at 10:59):

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

#### Eric Wieser (Aug 06 2020 at 11:00):

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 (Aug 06 2020 at 11:00):

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

#### Kenny Lau (Aug 06 2020 at 11:02):

but I forgot the name

#### Kenny Lau (Aug 06 2020 at 11:02):

because I remember that the name was somewhat convoluted

#### Kevin Buzzard (Aug 06 2020 at 11:05):

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 (Aug 06 2020 at 11:06):

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 (Aug 06 2020 at 11:07):

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 (Aug 06 2020 at 11:08):

@Kevin Buzzard there you go

#### Kenny Lau (Aug 06 2020 at 11:08):

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

nice

#### Kevin Buzzard (Aug 06 2020 at 11:15):

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

#### Gabriel Ebner (Aug 06 2020 at 11:16):

I thought we decided that somebody should implement auto.

#### Kenny Lau (Aug 06 2020 at 11:16):

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

or PR'ed

#### Gabriel Ebner (Aug 06 2020 at 11:16):

slimcheck slim_check

#2080

yes that's it

#### Kenny Lau (Aug 06 2020 at 11:18):

no way I can remember the name

#### Kenny Lau (Aug 06 2020 at 11:19):

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

#### Kenny Lau (Aug 06 2020 at 11:24):

is there a mathematical proof using model theory?

#### Kenny Lau (Aug 06 2020 at 11:24):

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

#### Kenny Lau (Aug 06 2020 at 11:26):

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 (Aug 06 2020 at 11:30):

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

right

#### Kenny Lau (Aug 06 2020 at 11:33):

hmm I don't know how to fix my statement

#### Kenny Lau (Aug 06 2020 at 11:33):

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

#### Mario Carneiro (Aug 06 2020 at 11:43):

maybe n+1 quantifiers?

#### Mario Carneiro (Aug 06 2020 at 11:44):

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

#### Mario Carneiro (Aug 06 2020 at 11:49):

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

#### Mario Carneiro (Aug 06 2020 at 11:50):

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

#### Utensil Song (Aug 06 2020 at 13:12):

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 (Aug 06 2020 at 19:39):

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 (Aug 06 2020 at 22:29):

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

Thanks!

#### Alex J. Best (Aug 06 2020 at 23:04):

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 (Aug 07 2020 at 00:06):

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


Last updated: May 12 2021 at 23:13 UTC