Zulip Chat Archive

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

Utensil Song (Aug 06 2020 at 10:32):

tactic#extract_goal ?

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

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

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
  admit,
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?

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

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!4! cases, so try all orders.

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

I remember seeing some PR about a tactic finding contradiction

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

Kevin Buzzard (Aug 06 2020 at 11:08):

hey look what I found

Kenny Lau (Aug 06 2020 at 11:09):

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?

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

or PR'ed

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

slimcheck slim_check

Gabriel Ebner (Aug 06 2020 at 11:17):

#2080

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

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 nn quantifiers then (φ)    (fin nφ)(\vdash \varphi) \iff (\mathsf{fin}~n \vDash \varphi)

Gabriel Ebner (Aug 06 2020 at 11:30):

How about x1xn(x1<<xn)\exists x_1 \cdots \exists x_n (x_1 < \cdots < x_n)?

Kenny Lau (Aug 06 2020 at 11:32):

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 nn 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, x,y1yn,(x<y1<<yn)(x>y1>>yn)\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 (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.

Kevin Buzzard (Aug 06 2020 at 22:29):

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: Dec 20 2023 at 11:08 UTC