Proofs that should be automatic

Stream: general

[Oliver Nash]

I recently decided that I'm far too tolerant when Lean asks me to prove trivialities. Today I decided I'd start collecting a list of stark examples of proofs that:

• Lean seems unable to do automatically
• Lean really should be able to do automatically

[Oliver Nash]

I just encountered my first potential example:

import data.set.basic

open set

example {α : Type*} {a : α} {U V : set α} (hUV : U ∪ V = univ) (ha : a ∉ U) : a ∈ V :=
begin
  replace hUV : a ∈ U ∨ a ∈ V, { rw ← mem_union, simp [hUV], },
  tauto,
end

[Oliver Nash]

My question is: is this really an example or am I missing a tactic / trick?

[Yaël Dillies]

You should state U ∪ V = univ as codisjoint U V.

[Eric Wieser]

This also works:

example {α : Type*} {a : α} {U V : set α} (hUV : U ∪ V = univ) (ha : a ∉ U) : a ∈ V :=
begin
  rw set.ext_iff at hUV,
  simpa [ha] using hUV a,
end

[Oliver Nash]

Yaël Dillies said:

You should state U ∪ V = univ as codisjoint U V.

Maybe this would be a better idiom but I don't think it addresses my point.

[Wrenna Robson]

What is the behaviour you expect?

[Wrenna Robson]

I'm not at a computer to be able to try it, but I would solve this via:

• a \mem univ
• a \mem U union V (rw hUV)
• a \mem U or a \mem V
• a \mem V (using ha in some suitable logic lemma)

I'm honestly not sure you could ask for more than that?

[Wrenna Robson]

and Eric's proof is imo proof that lean seems to be able to do it.

[Wrenna Robson]

do we have codisjoint U V iff forall a, a mem U or a mem V? Because it strikes me that that lemma might be useful here

[Yaël Dillies]

Not yet, no.

[Kevin Buzzard]

It's not true for things like groups

[Oliver Nash]

Wrenna Robson said:

What is the behaviour you expect?

I would like Lean never present me with something this trivial but if it ever did, I would like a tactic like tauto to close it.

[Wrenna Robson]

I don't think this is a realistic expectation.

[Wrenna Robson]

What if you replace hUV in your example with "a \mem U union V"?

[Wrenna Robson]

That feels at least more reasonable to expect to be tautologous.

[Yaël Dillies]

Wrenna, this would be automatic in Isabelle. Oliver's point is that we don't have enough automation in mathlib.

[Wrenna Robson]

hmm, fair enough

[Wrenna Robson]

I would have assumed an automator would trip on the fact that hUV is much stronger than needed so you need to work out what to use.

[Wrenna Robson]

how would Isabelle do it; what is the approach they use?

[Wrenna Robson]

I don't disagree by the way that we could do with more automation in mathlib.

[Oliver Nash]

I know almost nothing about proof automation. My hope in starting this thread was that we might assemble a corpus of test cases that some smart person writing such tactics could use.

[Yaël Dillies]

Isabelle has a lot (like a lot) of automation, but I expect this would be solved using sledgehammer, which is a very polyvalent self-replacing tactic. How it works is that you write your proof forwardly and automation tries to fill in the step every time. If it doesn't get it, you give it more hints and try again.

[Yaël Dillies]

Someone could try this example in Isabelle, but I expect it needs at most one hint.

[Wrenna Robson]

right I would expect it to be able to do it with a single hint! but not from nothing.

[Wrenna Robson]

Eric's solution is very nearly that.

[Wrenna Robson]

like that simpa is doing a reasonable degree of automation

[Yaël Dillies]

But Eric still had to come up with it! I'm sorry to break it to you, but Eric is not your tactic.

[Eric Rodriguez]

what about yael_search? :b

On a serious note, these sort of proofs maybe need a self-replacing tactic a-la polyrith, or (i)tauto needs to be able to expand common definitions (at least to do with sets/finsets). simp is very flexible but having to come up with a neat simp(a) proof for everything is not only annoying, but distracting from what you're working towards

[Yaël Dillies]

Here, I would expect automation to use docs#set.eq_univ_iff_forall.

[Eric Rodriguez]

I recently spent a nontrivial amount of time on the goal (x : Z) (x : N) : x - 1 - k = x - k.succ which is not right

[Yaël Dillies]

rw [nat.succ_eq_add_one, int.coe_nat_add, ←sub_sub, sub_right_comm]?

[Eric Rodriguez]

again, yael_search is not a tactic. it's clear that they can be done, but why do I need to hassle with this?

[Eric Rodriguez]

and sure, maybe succ is an implementation detail and if I rw [succ_eq_add_one] then maybe ring or push_cast, ring will work. but if implementation details keep appearing in goals for whatever reasons then it doesn't really matter this idealism, because it affects the day-to-day

[Eric Rodriguez]

(and it means I have to do have : ... := by { ... } instead of have ... := by tactic or ideally even inlining it)

[Moritz Doll]

not really a single proof, but I spent recently too much time on finding the correct version of lemmas like docs#mul_le_mul_of_nonneg_left
maybe a variant of congr for inequalities would be nice. So a (b+d) < a (c + d) gets reduced to b < c and a bunch of stuff that positivity can prove

[Ruben Van de Velde]

Isn't that tactic#mono?

[Yaël Dillies]

I would really love having Coq's generalized rewriting, if only for ≤.

[Moritz Doll]

Ruben Van de Velde said:

Isn't that tactic#mono?

I have never heard of that tactic, I will have a look at it

[Wrenna Robson]

Eric Rodriguez said:

I recently spent a nontrivial amount of time on the goal (x : Z) (x : N) : x - 1 - k = x - k.succ which is not right

Yes this feels like a really good example.

[Wrenna Robson]

By the way - why does mem_union_eq exist? I was expecting mem_union to be the simp lemma here...

[Yaël Dillies]

= lemmas and ↔ are not quite treated the same. Eric Wieser fixed some of this, but I'm not sure the issue is fully solved.

[Wrenna Robson]

example {α : Type*} {a : α} {U V : set α} (hUV : a ∈ U ∪ V) (ha : a ∉ U) : a ∈ V :=
by { simp only [mem_union_eq, or_iff_not_imp_left, hUV] at hUV, tauto }

[Wrenna Robson]

This is the best I've got for that, btw

[Wrenna Robson]

Or if you allow non-terminal simps:

example {α : Type*} {a : α} {U V : set α} (hUV : a ∈ U ∪ V) (ha : a ∉ U) : a ∈ V :=
by { simp at hUV, tauto }

[Kevin Buzzard]

An example which came up yesterday on the discord: given a finset of five integers each of which is at most 50, prove that the sum is at most 50+49+48+47+46. This does not need a proof in a classroom situation but was pretty nasty to do in Lean

[Wrenna Robson]

(But I changed hUV, so I cheated.)

[Yaël Dillies]

Wrenna Robson said:

Or if you allow non-terminal simps:

example {α : Type*} {a : α} {U V : set α} (hUV : a ∈ U ∪ V) (ha : a ∉ U) : a ∈ V :=
by { simp [or_iff_not_imp_left, hUV] at hUV, tauto }

This is a fine simp, because tauto is a fancy tactic too.

[Wrenna Robson]

Incidentally, an example of these is some stuff which SMT solvers can discharge easily, that I was talking about with some of the lean-crypto people.

[Wrenna Robson]

example {α : Type*} {a : α} {U V : set α} (hUV : U ∪ V = univ) (ha : a ∉ U) : a ∈ V :=
by { simp [eq_univ_iff_forall] at hUV, specialize hUV a, tauto }

Does this fufill the "one hint" requirement? I would say maybe. Should eq_univ_iff_forall be a simp lemma in general?

[Eric Rodriguez]

Kevin Buzzard said:

An example which came up yesterday on the discord: given a finset of five integers each of which is at most 50, prove that the sum is at most 50+49+48+47+46. This does not need a proof in a classroom situation but was pretty nasty to do in Lean

I'd argue that that proof by induction really is the "morally" right thing to do. Some of the subgoal proofs were pretty absurd, though...

[Wrenna Robson]

Oh:

example {α : Type*} {a : α} {U V : set α} (hUV : U ∪ V = univ) (ha : a ∉ U) : a ∈ V :=
by { simp [eq_univ_iff_forall] at hUV, finish }

[Wrenna Robson]

I mean this is pretty close to full automation I would argue. Arguably it's only not because of the form of hUV.

[Wrenna Robson]

Kevin Buzzard said:

An example which came up yesterday on the discord: given a finset of five integers each of which is at most 50, prove that the sum is at most 50+49+48+47+46. This does not need a proof in a classroom situation but was pretty nasty to do in Lean

So this is equivalent to a <= 50, b <= 50, c <= 50, d <= 50, e <= 50, a < b < c < d < e, show that a + b + c + d + e < 240, right?

[Wrenna Robson]

Can Lean do it in that form?

[Wrenna Robson]

Because this is an easy SMT solve:

; Variable declarations
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)

; Constraints
(assert (<= a 50))
(assert (<= b 50))
(assert (<= c 50))
(assert (<= d 50))
(assert (<= e 50))

(assert (< a b))
(assert (< b c))
(assert (< c d))
(assert (< d e))
(assert (> (+ (+ (+ (+ a b) c) d) e) 240 ))

; Solve
(check-sat)
(get-model)

[Wrenna Robson]

https://compsys-tools.ens-lyon.fr/z3/index.php

[Wrenna Robson]

Right and indeed:

example {a b c d e : ℤ} (ha : a ≤ 50) (hb : b ≤ 50) (hc : c ≤ 50) (hd : d ≤ 50) (he : e ≤ 50)
(hab : a < b) (hbc : b < c) (hcd : c < d) (hde : d < e) :
  a + b + c + d + e ≤ 46 + 47 + 48 + 49 + 50 := by linarith

[Johan Commelin]

So we are just 1 wlog away from the general statement.

[Johan Commelin]

But I guess wlog struggles with 5!.

[Wrenna Robson]

yeah and this wouldn't work if you wanted to prove it for all n, I suppose.

[Moritz Doll]

Ruben Van de Velde said:

Isn't that tactic#mono?

thank you so much Ruben. Even though the proofs are now longer by lines, they are so much more readable:

-    refine mul_le_mul_of_nonneg_left _ (inv_nonneg.mpr fac_nonneg),
-    refine pow_le_pow_of_le_left (by positivity) _ _,
-    -- We use linarith to prove |x - y| ≤ |b - a|:
-    exact abs_le_abs (by linarith [hx.2, hy.1]) (by linarith [hx.1, hy.2]),
+    mono*,
+    any_goals { positivity },
+    { exact hx.2 },
+    { exact hy.1 },
+    { linarith [hx.1, hy.2] },

and

-  refine mul_le_mul_of_nonneg_left _ hSup,
-  refine mul_le_mul_of_nonneg_left _ (pow_nonneg (sub_pos.mpr h).le _),
-  exact sub_le_sub_right hx.2 _,
+  mono* with 0 ≤ (b - a) ^ n,
+  any_goals { positivity },
+  exact hx.2,

[Moritz Doll]

it feels like mono*, any_goals { positivity } is exactly the thing I wanted to have

[Bolton Bailey]

What do people think of this as a proof that should be automatic?

lemma nat.min_add_sub (a b : ℕ) : min a b + (a - b) = a := sorry

It feels like if only there was a way to get lean to realize that the definition of min is somehow essentially casework, then this could be solved by tidy or something.

[Johan Commelin]

It also needs to understand truncated subtraction.

[Johan Commelin]

My first reaction was: "That looks very wrong! The symmetry is broken!" -- And then "Oooooh wait. ℕ... Never mind."

[Eric Wieser]

Perhaps a general mechanism to indicate "to prove stuff about foo x y you should case on some_lemma x y" would help with that

[Eric Wieser]

We have things like docs#finset.sup_induction already, but those are too strong if your goal also includes a bare s as well as s.sup f

[Bolton Bailey]

Eric Wieser said:

Perhaps a general mechanism to indicate "to prove stuff about foo x y you should case on some_lemma x y" would help with that

Maybe a @[case_simp] tag for lemmas of the form a = if b then c else d where c and d are both simpler than a

[Heather Macbeth]

Moritz Doll said:

not really a single proof, but I spent recently too much time on finding the correct version of lemmas like docs#mul_le_mul_of_nonneg_left
maybe a variant of congr for inequalities would be nice. So a (b+d) < a (c + d) gets reduced to b < c and a bunch of stuff that positivity can prove

@Moritz Doll I totally agree, I think this "inequality-congr" is the basic mental tactic we use to prove inequalities on paper. I actually have a work-in-progress version of this tactic for teaching, see
https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation.html#proving-inequalities

It needs more polishing before joining mathlib, though.

[Heather Macbeth]

This was actually my motivation for writing positivity.

[Yaël Dillies]

Oh this is also the tactic idea I was telling you in DMs, right? What I got from discussing it with Jannis is that we even needed generalised rewriting.

[Heather Macbeth]

@Yaël Dillies I think this is easier than generalized rewriting, and more akin to congr than to rw (it's interesting to me that both Moritz and I used congr as our mental analogy).

As I understand it, generalized-rewriting by h : a ≤ b would let you, e.g., reduce a goal ⊢ 3 * a ≤ 5 to a goal ⊢ 3 * b ≤ 5.

By contrast, what I have written is a finishing tactic which would, e.g., prove the goal ⊢ 3 * a ≤ 3 * b.

[Heather Macbeth]

It's very much in the same vein as the tactic mono* (discussed upthread), but designed to be "greedy". Compare their behaviour on the goal ⊢ a * x ≤ b * x.

• the tactic I wrote will go ahead and reduce this to the goals a ≤ b and 0 ≤ x.
• the tactic mono will tell you that it could reduce this to (x ≤ 0 and b ≤ a) or to (0 ≤ x and a ≤ b), and ask you to disambiguate.

In my experience, paper proofs are usually written in such a way that the greedy behaviour is correct, so it's a more efficient user experience if you don't have to disambiguate (especially when you're using the recursive form mono* and would have disambiguate several times in a single proof).

But they are close enough that it would probably be possible to re-implement my tactic as a variant of mono.

[Moritz Doll]

concerning mono* I had a slight issue, where mono produced more positivity-goals than what I had when wrote the proof by hand. This might be related to the "non-greedyness" of mono.

[Yaël Dillies]

Ah yes, so this is not quite the tactic I want/need. But still interesting!

[Yaël Dillies]

SRL has those huge calc blocks that would become much more readable if I could rewrite along inequalities, but I can't use your tactic there because most calls would be non finishing.

[Jannis Limperg]

Bolton Bailey said:

lemma nat.min_add_sub (a b : ℕ) : min a b + (a - b) = a := sorry

Aesop will be able to do this, assuming a good simp set:

import Aesop

@[simp]
theorem Nat.not_le_le (a b : Nat) : ¬ a ≤ b ↔ b ≤ a := sorry

@[simp]
theorem Nat.sub_eq_zero (h : a ≤ b) : a - b = 0 := sorry

@[simp]
theorem Nat.add_sub {a b : Nat} (h : b ≤ a) : b + (a - b) = a := sorry

theorem Nat.min_add_sub (a b : Nat) : min a b + (a - b) = a := by
  aesop (add norm unfold min)

Aesop recognises that the goal, after unfolding min, contains an if, and splits along its condition. (It essentially runs split_ifs eagerly, which imo is usually the right thing to do.) simp does the rest.

[Damiano Testa]

I had forgotten about this example. On branch#adomani_remove_subs, this also is a proof:

import tactic.remove_subs

example (a b : ℕ) : min a b + (a - b) = a :=
by remove_subs; simp; assumption

[Damiano Testa]

@Jannis Limperg should Nat.not_le_le really be Nat.not_le_lt, with a strict inequality on one side?

[Jannis Limperg]

Hehe, yes, of course.

[Damiano Testa]

With that lemma, Aesop should be able to prove much more than Nat.min_add_sub :upside_down:

[Damiano Testa]

In the spirit of automatization, the nat-subtraction discussion and the example with max/min that @Bolton Bailey and @Eric Wieser mentioned above seem to suggest support for a tactic similar to split_ifs that would look for stuff on which to do cases and actually do it.

Would this be something desirable?

[Damiano Testa]

The tactic remove_subs could be easily modified to at least split over max/min but probably even more generally, to fit with some user-flag that tells it what to do cases on.

[Eric Rodriguez]

example {α β} {f : α → β} {b : β} : (∃ a, f a = b) ∨ ∀ a, f a ≠ b

finish can do this but we're encouraged not to use it, afair. tauto! and itauto! failing on this is unexplicable (and it's not ne, the ¬ version fails as well)

[Michael Stoll]

I suspect tauto does not know about moving negations out of quantifiers?

[Bolton Bailey]

To generalize what I was saying before in the context of this example, I feel there should be more emphasis on automatic tactics breaking down logical connectives. Just as tidy calls split when it sees an and and intro when it sees a -> I feel like it should call something likedecidable.or_iff_not_imp_left when it sees the goal is a disjunction (and indeed classical, rw decidable.or_iff_not_imp_left, tidy, closes the goal).

[Kevin Buzzard]

@Timothee Lacroix 's AI can solve this one! I just kept selecting the top option. Maybe it got lucky but still!

[Mario Carneiro]

itauto doesn't know anything about predicate logic

[Wrenna Robson]

Anyone know a way to make this automatic (assuming we're in a classical context):
lemma blahj {a b : Prop} (h : ¬a ↔ ¬b) : a ↔ b := sorry

[Wrenna Robson]

It's essentially just one direction of not_iff_not but we don't actually seem to have it.

[Yaël Dillies]

Could be called iff.of_not

[Mario Carneiro]

not_iff_not.1

[Wrenna Robson]

Aye, I mean, that's what I did, but none of the automated tools could find it...

[Mario Carneiro]

library search should find one directional versions of iff lemmas

[Mario Carneiro]

it might be underpowered in lean 4

[Wrenna Robson]

It fails in Lean 3.
lemma blahj {a b : Prop} (h : ¬a ↔ ¬b) : a ↔ b := by library_search!
lemma blahj {a b : Prop} (h : ¬a ↔ ¬b) : a ↔ b := by library_search

both fail.

[Scott Morrison]

That's unfortunate, and perhaps counts as a library_search bug...

[Michael Stoll]

lemma blahj {a b : Prop} (h : ¬a ↔ ¬b) : a ↔ b := by tauto!