golfing `Ico` union

Stream: maths

[Yury G. Kudryashov]

I have the following goal:

example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c := sorry

I know how to prove this using lots of by_cases and Ico_union_Ico. Is there any easier way?

[Floris van Doorn]

Here it is for decidable linear orders. I think Ico_union_Ico is the most general lemma that "merges" the union of two Icos (I do have some nonterminal simps in my proof).
After doing all this, I'm not sure if this was actually easier than doing it directly, but Ico_union_Ico is probably also useful for a bunch of other things.

lemma Ico_union_Ico' {α} [decidable_linear_order α] {a b c d : α}
  (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) :
  Ico a c ∪ Ico b d = Ico a d :=
begin
  apply subset.antisymm, apply union_subset; apply Ico_subset_Ico; {refl <|> assumption},
  rw ← Ico_union_Ico_eq_Ico h1 (le_trans h2 h3), apply union_subset_union_left,
  apply Ico_subset_Ico, refl, assumption
end

lemma Ico_union_Ico {α} [decidable_linear_order α] {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
  cases le_total a b with h3 h3; cases le_total c d with h4 h4; simp [h3, h4] at h1 h2 ⊢,
  { cases le_total a c with h5 h5; cases le_total b d with h6 h6; simp [h5, h6],
    { apply Ico_union_Ico'; assumption },
    { apply union_eq_self_of_subset_right, apply Ico_subset_Ico; assumption },
    { apply union_eq_self_of_subset_left, apply Ico_subset_Ico; assumption },
    { rw union_comm, apply Ico_union_Ico'; assumption },
     },
  { simp [h1, h2] },
  { simp [h1, h2] },
  { rw Ico_eq_empty, simp * }
end

lemma Ico_union_Ico_same {α} [decidable_linear_order α] {a b c : α} :
  Ico a b ∪ Ico b c = Ico (min a b) (max b c) :=
Ico_union_Ico (le_trans (min_le_right _ _) (le_max_left _ _))
              (le_trans (min_le_left _ _) (le_max_right _ _))

example {α} [decidable_linear_order α] (a b c : α) :
  Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
begin
  rw [Ico_union_Ico_same, Ico_union_Ico, union_comm (Ico b a), Ico_union_Ico_same, Ico_union_Ico],
  { simp only [max_left_comm, min_left_comm, min_comm, max_comm] },
  all_goals { simp, finish },
end

[Kevin Buzzard]

I think the proof should be: WLOG a<=b<=c; linarith.

[Kevin Buzzard]

The theorem statement is S3-invariant.

[Kevin Buzzard]

Aah I see, you still have to do a case split on X<b

[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

If you do split_ifs at * you can end up with five variables called a sometimes. I was using semicolons but all_goals is clearer. I got from 1 goal to 160 and then back down to 1 but I didn't quite finish and now I have to go :-/ Do I need one more case split? Why do I need case splits? Is there something that linarith doesn't know? Would like to diagnose but have family duties

[Kenny Lau]

@Kevin Buzzard what's the maths proof that isn't "draw a picture"?

[Kevin Buzzard]

I just posted it: get the tactics to draw the picture

[Kevin Buzzard]

Why can't I close my last goal? c<a<=d<b

[Jasmin Blanchette]

Because no hammer?
Screen-Shot-2020-07-25-at-13.01.42.png

[Jasmin Blanchette]

(In turn, because excruciatingly low Lean 3 metaprogramming framework.)

[Kevin Buzzard]

Yeah that's the correct proof

[Kevin Buzzard]

"It's obvious"

[Floris van Doorn]

Yes, we do miss sledgehammer in Lean.
However, many of your conjunctions should be disjunctions: you only know

h1 : a ≤ c ∨ b ≤ c ∨ a ≤ d ∨ b ≤ d,
h2 : c ≤ a ∨ d ≤ a ∨ c ≤ b ∨ d ≤ b

[Floris van Doorn]

@Jasmin Blanchette

[Floris van Doorn]

Oh sorry, you responded to Kevin, you were not golfing my lemma. My bad.

[Floris van Doorn]

Does sledgehammer solve the complete lemma by itself?

[Patrick Massot]

The screenshot suggests we miss auto or force, not really sledgehammer (unless you consider these to be part of sledgehammer).

[Yury G. Kudryashov]

I came up with the following (for a decidable_linear_order):

lemma Ico_union_Ico_union_Ico_cycle :
  Ico a b ∪ Ico b c ∪ Ico c a = Ico (min a (min b c)) (max a (max b c)) :=
ext $ λ x, by simp [iff_def, or_imp_distrib, lt_or_le] { contextual := tt };
  simp [← or_assoc, or_comm, lt_or_le]

[Patrick Massot]

It would be really nice to have a tactic doing this is a pretty general context.

[Jasmin Blanchette]

@Floris: I can't test easily without knowing what Ico is.

[Reid Barton]

src#set.Ico

[Jasmin Blanchette]

@Patrick Massot another proof is possible with Isabelle's simp + linarith.

[Mario Carneiro]

Here's a more basic proof along the lines of floris's first proof:

lemma Ico_union_Ico {α} [decidable_linear_order α] {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
  apply subset.antisymm,
  { apply union_subset; apply Ico_subset_Ico; simp [le_refl] },
  rintro x ⟨h3, h4⟩; simp at h3 h4 ⊢,
  cases h3; cases h4; simp [h3, h4]; by_contra hn; push_neg at hn; cases hn with h5 h6,
  { exact not_le_of_lt (lt_min h6 h4) (le_trans h2 (max_le h3 h5)) },
  { exact not_le_of_lt (lt_min h5 h4) (le_trans h1 (max_le h3 h6)) }
end

I tried linarith on the last two goals but it didn't work, does it not do proofs in pure inequality structures?

[Gabriel Ebner]

Golfed:

lemma Ico_Ico_Ico {α} [linear_order α] (a b c : α) :
  Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
by ext; split; finish using [lt_of_le_of_lt, lt_of_lt_of_le, lt_irrefl] {max_ematch_rounds := 2}

(Please don't run the profiler on this.)

[Gabriel Ebner]

Slightly faster (five seconds):

lemma Ico_Ico_Ico {α} [linear_order α] (a b c : α) :
  Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
by ext; simp; super with lt_irrefl lt_of_lt_of_le lt_of_le_of_lt le_or_lt {timeout := 50000}

This should be acceptably fast in :four_leaf_clover:.

[Patrick Massot]

Jasmin Blanchette said:

Patrick Massot another proof is possible with Isabelle's simp + linarith.

We want all of this :grinning:

[Yury G. Kudryashov]

Note that we can't use Lean linarith because we have only (decidable_)linear_order, no ordered_field.

[Yury G. Kudryashov]

BTW, @Jasmin Blanchette what does Isabelle say in this context (linear_order only)?

[Sebastien Gouezel]

lemma auto_is_strong:
  fixes a b c::"'a::linorder"
  shows "{a ..< b} ∪ {b ..< c} ∪ {c ..< a} = {b ..< a} ∪ {c ..< b} ∪ {a ..< c}"
by auto

[Sebastien Gouezel]

(takes less than 1/10s)

[Sebastien Gouezel]

I guess auto will use some simp lemmas that will depend on the order of the points, then split automatically on case disjunction, then use some version of linarith that works in linear orders, but I don't know how to ask details about the proof.

[Sebastien Gouezel]

In fact, I don't think it uses any fancy version of linarith. Probably it only applies lt_of_le, lt_trans a few times (at most 5, say), see all the consequences it gets from this, and then sees if the goal is in there (but in a more efficient way called a tableau prover). Essentially what Gabriel did with its super invocation, in fact. Except that it is really fast in Isabelle, and completely automatic.

[Jasmin Blanchette]

@Jannis Limperg I hope you are paying attention. ;)

[Kenny Lau]

import data.set.intervals.basic

open set

example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
begin
  cases le_total a b with hab hba; cases le_total b c with hbc hcb,
  { rw [Ico_eq_empty hab, Ico_eq_empty hbc, Ico_eq_empty (le_trans hab hbc),
      empty_union, empty_union, union_empty, Ico_union_Ico_eq_Ico hab hbc] },
  { cases le_total a c with hac hca,
    { rw [Ico_eq_empty hac, Ico_eq_empty hcb, Ico_eq_empty hab,
        empty_union, union_empty, union_empty, union_comm, Ico_union_Ico_eq_Ico hac hcb] },
    { rw [Ico_eq_empty hca, Ico_eq_empty hcb, Ico_eq_empty hab,
        empty_union, union_empty, union_empty, union_comm, Ico_union_Ico_eq_Ico hca hab] } },
  { cases le_total a c with hac hca,
    { rw [Ico_eq_empty hac, Ico_eq_empty hbc, Ico_eq_empty hba,
        empty_union, union_empty, union_empty, Ico_union_Ico_eq_Ico hba hac] },
    { rw [Ico_eq_empty hca, Ico_eq_empty hbc, Ico_eq_empty hba,
        empty_union, union_empty, union_empty, Ico_union_Ico_eq_Ico hbc hca] } },
  { rw [Ico_eq_empty hcb, Ico_eq_empty hba, Ico_eq_empty (le_trans hcb hba),
      empty_union, empty_union, union_empty, union_comm, Ico_union_Ico_eq_Ico hcb hba] }
end

[Kevin Buzzard]

Yury G. Kudryashov said:

I know how to prove this using lots of by_cases and Ico_union_Ico. Is there any easier way?

[Kevin Buzzard]

So what is auto?

[Sebastien Gouezel]

From https://people.mpi-inf.mpg.de/~jblanche/frocos2011-dis-proof.pdf:

On the user level, the simplifier is eclipsed by auto, a proof method that interleaves simplification with a small amount of proof search. It is impossible to describe suc-cinctly what auto does due to its heuristic, ad hoc nature. Its great strength is its ability to discharge the easy parts of a goal and leave the user with the more difficult ones. This helps the user to quickly focus on the core of a problem.Strengthened versions of auto perform more sophisticated proof search, while still interleaving it with simplification. The search is based on tableau methods [39]. These methods are often useful, but since search is involved, not only are they slower than the simplifier and auto, they are endgame provers that do not provide any hints when they fail to prove the goal

@Jasmin Blanchette , do you know of a reference describing a little bit more of the internals of auto? I think I miss it in Lean even more than sledgehammer...

[Mario Carneiro]

I've read descriptions of auto like that several times before and it's indistinguishable from "auto is magic"

[Mario Carneiro]

and as a user it also is difficult to demystify by watching it work

[Sebastien Gouezel]

Apparently (see the code at http://isabelle.in.tum.de/repos/isabelle/file/f3e1144a1cec/src/Provers/clasimp.ML), it combines blast (https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/blast.pdf) with the simplifier.

[Patrick Massot]

Mario Carneiro said:

I've read descriptions of auto like that several times before and it's indistinguishable from "auto is magic"

This sounds like the holy grail of interactive theorem proving: a tactic that proves obvious goals without any need to understand how it works.

[Mario Carneiro]

I generally have a bad experience with "magic" tactics. If it actually solves all goals I care about, well that's great, but that's also a pipe dream. Unless I understand the failure modes, I won't be able to use it effectively

[Mario Carneiro]

I remember working in isabelle during a tutorial, this was my number one complaint - everything was "by auto" and I didn't even understand what the syntax of tactic proofs was (and of course I can't ask isabelle to show me the proof either). It was very unsatisfying

[Jasmin Blanchette]

auto isn't that magic. It's really simplifier + some intro and elim rules, some applied aggressively, some not (with backtracking). From its output, which is similar to the simplifier's except that you can get multiple subgols, you can usually tell "oh, I forgot to register commutativity of foo as a simp rule".

[Sebastien Gouezel]

auto is not a closing tactic: it takes care of what it can, and leaves you with the remaining goals. And you can tweak it like (auto simp: foo bar intro: foo' bar') telling it to add foo and bar to the simpset during this run, and to apply the lemmas foo' and bar' whenever it can. When you are used to it, it is incredibly efficient.

[Jasmin Blanchette]

But indeed, it would be nice if auto had some detailed output, or at least existed in some squeeze_auto fashion.

[Jasmin Blanchette]

And if auto were ever reproduced in Lean, it would have to have better output.

[Jasmin Blanchette]

As for the reference: I'm not aware of any.

[Mario Carneiro]

how important is heuristic instantiation for auto?

[Mario Carneiro]

Does it differ in any important way from tidy? If it's just "case on or, split on and, simp" then tidy does that already

[Sebastien Gouezel]

auto does backtracking.

[Mario Carneiro]

what do you get in an auto failure if it backtracks?

[Sebastien Gouezel]

Auto does several things:

• it applies the simplifier (always).
• there are some lemmas that it will always apply if they make sense. No backtracking involved. Typically you are left with several subgoals afterwards.
• there are somme lemmas that it will apply if after applying them it is able to prove the goal (or the part of the goal it is working on). Here backtracking happens.

This means that on some subgoals it will try to find a proof and if it doesn't it will just leave you the subgoal untouched. Other subgoals will be solved thanks to backtracking and proof search. Typically, in the end you will just be left with the nontrivial remaining subgoals, a.k.a., the interesting part of the proof.

[Sebastien Gouezel]

(NB: this is what I understood from playing quite some time with Isabelle, I have never looked at auto's inner workings)

[Kenny Lau]

then how do you do all that in 1/10 s?

[Sebastien Gouezel]

That's Isabelle and simple type theory (no unification, no implicit parameters, and so on).

[Mario Carneiro]

so what are intro and elim rules and how do they contribute to that overall structure?

[Mario Carneiro]

I understand that these have to be annotated in the library, yes?

[Sebastien Gouezel]

Yes. You have intro! lemmas (i.e., lemmas tagged with this attribute in the library), which are lemmas that auto should always apply when they make sense, and intro (or intro?) lemmas that will only be applied in the middle of a proof search process with backtracking. And elim I never really understood :-)

[Sebastien Gouezel]

Note that the intro! lemmas are not equivalences in general, so maybe a statement that was provable is not provable any more after applying auto. But when a lemma is the right thing to do like 95% of the time, it is a good idea to mark it at intro! (and of course the intro set can be tweaked in an invocation of auto).

[Mario Carneiro]

Does simplify have its own annotation e.g. simp? Or does it reuse intro and elim in some way

[Sebastien Gouezel]

You also have simp tags, yes. You have 3 different kinds of lemmas, the simp ones, the intro ones, and the elim ones.

[Mario Carneiro]

Lean also has intro and intro! attributes, but no one knows what they do :)

[Sebastien Gouezel]

Probably they don't do anything for now because we don't have auto, but they have been planned a long way ahead!

[Patrick Massot]

That's not true.

[Patrick Massot]

I know what they do.

[Patrick Massot]

https://github.com/leanprover-community/lean/blob/master/library/init/meta/backward.lean

[Mario Carneiro]

we should give back_chaining an interactive front end and try using it

[Sebastien Gouezel]

Is it like apply_rules?

[Mario Carneiro]

pretty sure

[Patrick Massot]

Yes, it's Leo's version of apply_rules.

[Patrick Massot]

But it's clearly an experiment that was mostly abandonned.

[Mario Carneiro]

does it do things?

[Sebastien Gouezel]

I've done apply_rules because I was longing for auto and I couldn't do anything smarter, but I'm pretty sure Leo's version is much better!

[Mario Carneiro]

the problem with relying on leo's tactics is that they don't get maintenance because no one knows the code

[Mario Carneiro]

the smt/eblast stuff died for basically that reason

[Mario Carneiro]

honestly simp has held up pretty well all things considered

[Mario Carneiro]

but if you are okay with using them as is then I don't see why we can't give a nice front end to the tactic and see if it's any good

[Mario Carneiro]

It passes the basic test:

example {n : ℕ} : n ≤ n ⊔ n ⊔ n :=
by apply_rules [le_sup_left_of_le, le_refl]

example {n : ℕ} : n ≤ n ⊔ n ⊔ n :=
by do
  [`le_sup_left_of_le, `le_refl].mmap tactic.mk_const >>=
  tactic.back_chaining_using

[Kenny Lau]

we don't need more powerful tactics; we need more basic tactics and more creative proofs:

import data.set.intervals.basic tactic

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']

example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
subset.antisymm (subset.trans (union_subset_union (union_subset_union
    (@Ico_subset_Ico_union_Ico _ _ a c b) (@Ico_subset_Ico_union_Ico _ _ b a c)) (@Ico_subset_Ico_union_Ico _ _ c b a)) (by unions))
  (subset.trans (union_subset_union (union_subset_union
    (@Ico_subset_Ico_union_Ico _ _ b c a) (@Ico_subset_Ico_union_Ico _ _ c a b)) (@Ico_subset_Ico_union_Ico _ _ a b c)) (by unions))

[Kenny Lau]

turns out Lean is pretty smart:

import data.set.intervals.basic tactic

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']

example {α} [linear_order α] (a b c : α) : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
subset.antisymm (subset.trans (union_subset_union (union_subset_union
    Ico_subset_Ico_union_Ico Ico_subset_Ico_union_Ico) Ico_subset_Ico_union_Ico) (by unions))
  (subset.trans (union_subset_union (union_subset_union
    Ico_subset_Ico_union_Ico Ico_subset_Ico_union_Ico) Ico_subset_Ico_union_Ico) (by unions))

[Sebastien Gouezel]

Kenny Lau said:

we don't need more powerful tactics

Come on Kenny! Would you complain if you had a tactic auto which could close this lemma with by auto in 1/10s?

[Gabriel Ebner]

Mario Carneiro said:

we should give back_chaining an interactive front end and try using it

I think auto would be great to have. Note that back_chaining only does a third of auto: namely applying the "intro" rules. My gut feeling is that most of the work of creating a Lean version of auto would consist of judiciously adding intro and elim attributes. These sets require just as much care, effort, and curation as the simp set.

[Mario Carneiro]

It actually has a bit of the other parts of auto as well, because the core tactic also includes a pre_tactic and leaf_tactic for interoperating with the backtracking search. If you put in simp as the pre_tactic it seems like you've got 2/3 of auto

[Mario Carneiro]

I definitely agree that it is important for us to start curating the intro set

[Mario Carneiro]

I suspect that there is a chicken and egg problem with getting a good intro set vs getting the auto tactic working

[Gabriel Ebner]

Don't forget the elim set.

[Mario Carneiro]

Do you know what that is? Sebastien didn't above

[Gabriel Ebner]

intro lemmas are used with apply, i.e. they only apply to the target of the goal. elim lemmas are similar to cases, they apply to the hypotheses.

[Gabriel Ebner]

E.g., if you have an assumption ∃ x, p x then you want to apply docs#exists.elim

[Mario Carneiro]

do you think we should use curated lemmas for that? Unlike isabelle we get most of that for free by using cases

[Mario Carneiro]

but maybe there are things like custom recursors we should be applying instead

[Mario Carneiro]

do you know examples of elim rules that are not just subsets of cases behavior?

[Jasmin Blanchette]

I'd consider using the intro! attribute globally for a unidirectional rule (i.e., one that doesn't preserve provability) a bug. The whole point is that these "safe" rules should be applied exhaustively, like simps, without loss of generality.

[Mario Carneiro]

An example of a unidirectional intro! rule would be something like closure for division like x \in real /\ y \in real /\ y != 0 -> x / y \in real for a hypothetical typing predicate for real division (maybe these are ZFC reals or something so that typing is a theorem)

[Mario Carneiro]

in fact even setting aside partial functions, something like x \in real /\ y \in real -> x + y \in real might very well not be bidirectional

[Sebastien Gouezel]

For another example, if you want to prove continuous (f + g), it seems to me completely reasonable to apply continuous.add and reduce it to the continuity of f and g, although of course you can have discontinuous functions whose sum is continuous, but this should never show up in real proofs.

[Sebastien Gouezel]

A rule that does preserve provability could instead be written as an iff and registered as a simp lemma, so to me the whole point of intro! is for rules that don't preserve provability but are completely reasonable like the continuity example.

[Jasmin Blanchette]

I'd say that's the point of intro.

[Jasmin Blanchette]

See e.g. http://www21.in.tum.de/~ballarin/fomus/part1/part1.pdf

[Jasmin Blanchette]

Search for "safe" and "unsafe" throughout.

[Jannis Limperg]

Jasmin Blanchette said:

Jannis Limperg I hope you are paying attention. ;)

I wasn't because I'm not subscribed to this stream, in which case I apparently don't even get notified if I'm @-mentioned. -.- Am now though.

[Jalex Stark]

When you @ someone who is not subscribed to the stream you're posting in, there should be a prompt to invite them to the stream