Computing Roth numbers

Stream: maths

[Yaël Dillies]

In #10509, Bhavik and I are computing small Roth numbers. The n-th Roth number is the size of the largest subset of finset.range n which doesn't contain arithmetic progressions of length 3 (aka Salem-Spencer set). Our current decidability instances (aka algorithms :grinning:) for roth_number_nat n ≤ m run in O (n.choose m * m^2). Can we do better?

[Yaël Dillies]

One idea would be to define inductively the maximal (wrt inclusion) Salem-Spencer subsets of a finset. This can work quite quickly because you know that a maximal Salem-Spencer subset of insert a s is a maximal Salem-Spencer subset of s with eventually a added.

[Yaël Dillies]

And we can trim further by restricting to maximal Salem-Spencer subsets but this time wrt card. It happens that quite often there's a unique such maximal subset, which can speed up subsequent calculations.

[Yaël Dillies]

I guess this is a question to @Mario Carneiro, how much can we get out of working over lists rather than finsets, and is there any way we can speed up using some lazy evaluation or related black magic?

[Mario Carneiro]

Not exactly sure what the algorithm is, but it sounds like it's possible to do better

[Mario Carneiro]

You probably don't need to do anything fancy with lazy evaluation, and it doesn't make much difference whether you are working over finsets or lists but lists are generally easier to work with

[Mario Carneiro]

also you don't want to use insert to build a finset unless you have to

[Yaël Dillies]

What would you use instead of insert?

[Mario Carneiro]

cons

[Yaël Dillies]

Ah sure!

[Yaël Dillies]

Another perk of lists is that you can use the underlying order on the elements to cut down by a factor of 3 or 6 the amount of computation required.

[Mario Carneiro]

I can't tell if this is correct. It seems to be unique all the time

def check : ℕ → list ℕ → bool
| a [] := tt
| a (b :: l) := l.all (λ c, a * c ≠ b * b) && check a l

def maximal_salem_spencer : ℕ → list (ℕ × list ℕ)
| 0 := [(0, [])]
| (n+1) :=
  let ls := maximal_salem_spencer n in
  let candidates := ls.map (λ p, if check n p.2 then (p.1 + 1, n::p.2) else p) in
  let maxlen := candidates.foldl (λ a l, max a l.1) 0 in
  candidates.filter (λ p, p.1 = maxlen)

#eval maximal_salem_spencer 80
-- [(59, [79, 78, 77, 74, 73, 71, 70, 69, 67, 66, 65, 62, 61, 59, 58, 57, 56, 55, 54, 53, 51, 48, 47, 46,
--    43, 42, 41, 40, 39, 38, 37, 35, 34, 33, 31, 30, 29, 27, 26, 24, 23, 22, 21, 19, 17, 16, 15, 14, 13, 11, 10, 8, 7, 6, 5, 3, 2, 1, 0])]

[Bhavik Mehta]

I know it should be unique at 14, not unique for 15,16,17 or 18, and not unique at a few points below that too; it's definitely not unique at 4: {0,1,3} and {0,2,3} both work

[Bhavik Mehta]

It's worth adding that there has been research on this from the computer science side: eg https://www.cs.umd.edu/~gasarch/papers/3apI.pdf

[Bhavik Mehta]

There is an important difference however in that to prove lower bounds we can just provide an example (computed by someone else), but to prove upper bounds we'd need to re-do the search in Lean (or find some clever other method, which is itself hard)

[David Wärn]

check should use addition instead of multiplication. Otherwise it looks correct to me

[Mario Carneiro]

The numbers all seem to match the computations in the PR but it's definitely not finding all the solutions

def check : ℕ → list ℕ → bool
| a [] := tt
| a (b :: l) := l.all (λ c, a + c ≠ b + b) && check a l

def maximal_salem_spencer : ℕ → list (ℕ × list ℕ)
| 0 := [(0, [])]
| (n+1) :=
  let ls := maximal_salem_spencer n in
  let candidates := ls.map (λ p, if check n p.2 then (p.1 + 1, n::p.2) else p) in
  let maxlen := candidates.foldl (λ a l, max a l.1) 0 in
  candidates.filter (λ p, p.1 = maxlen)

#eval (list.range 50).mmap (λ n, do
  let p := maximal_salem_spencer n,
  tactic.trace sformat!"roth {n} = {p.head.1}, {p.length} solutions")

roth 0 = 0, 1 solutions
roth 1 = 1, 1 solutions
roth 2 = 2, 1 solutions
roth 3 = 2, 1 solutions
roth 4 = 3, 1 solutions
roth 5 = 4, 1 solutions
roth 6 = 4, 1 solutions
roth 7 = 4, 1 solutions
roth 8 = 4, 1 solutions
roth 9 = 4, 1 solutions
roth 10 = 5, 1 solutions
roth 11 = 6, 1 solutions
roth 12 = 6, 1 solutions
roth 13 = 7, 1 solutions
roth 14 = 8, 1 solutions

[Mario Carneiro]

In the example for 4, the issue is that {0, 2} is not marked as a maximal set for n = 3 because it is not obtained by adding 2 to a maximal set for n = 2

[Yaël Dillies]

Oh, so you need to keep track of all maximal sets wrt inclusion.

[Bhavik Mehta]

roth 51 should be 17, for example - but maximal_salem_spencer computes 16

[Yaël Dillies]

Wait, that doesn't work either :confused:

[Mario Carneiro]

Even removing the max size restriction doesn't help, because {0} is not maximal wrt inclusion for n = 2 but it participates in a maximal set for n = 3

[Yaël Dillies]

So what's true is that if the Roth number increases, then the new maximal Salem-Spencer subsets come from previous ones.

[Bhavik Mehta]

Bhavik Mehta said:

roth 51 should be 17, for example - but maximal_salem_spencer computes 16

1 2 4 5 10 13 14 17 31 35 37 38 40 46 47 50 51 (1-indexed rather than 0-indexed, sorry) is an example

[Yaël Dillies]

And if it doesn't increase, then it comes from a previous maximal subset, or a previous almost maximal subset

[Mario Carneiro]

maybe the candidates need to consider not just n :: l where l is from the previous set but also n :: (l \ a) where a is an element from l

[Bhavik Mehta]

May I point you to the paper I linked above to save some time, since there are some algorithms given to do these computations (eg in section 6 - also section 9 talks about a dynamic program which I think is similar to the one above)

[Mario Carneiro]

I think this is a rendering of the BASIC2 algorithm from the paper:

def three_free : ℕ → list ℕ → bool
| a [] := tt
| a (b :: l) := l.all (λ c, a + c ≠ b + b) && three_free a l

def roth_aux : list ℕ → ℕ → ℕ → list ℕ → bool
| [] n d α := ff
| (s :: sz) n d α :=
  ((s ≥ d + 1) && roth_aux sz (n + 1) d α) ||
  (three_free n α && match d with
    | 0 := tt
    | (d'+1) := roth_aux sz (n + 1) d' (n :: α)
    end)

def roth : ℕ → ℕ × list ℕ
| 0 := (0, [])
| (n+1) := let (a, l) := roth n in (if roth_aux (a::l) 0 a [] then a + 1 else a, a :: l)

#eval (roth 40).2.reverse.enum
-- [(0, 0), (1, 1), (2, 2), (3, 2), (4, 3), (5, 4), (6, 4), (7, 4), (8, 4), (9, 5), (10, 5), (11, 6), (12, 6), (13, 7), (14, 8), (15, 8),
--  (16, 8), (17, 8), (18, 8), (19, 8), (20, 9), (21, 9), (22, 9), (23, 9), (24, 10), (25, 10), (26, 11), (27, 11), (28, 11), (29, 11), (30, 12),
--  (31, 12), (32, 13), (33, 13), (34, 13), (35, 13), (36, 14), (37, 14), (38, 14), (39, 14)]

[Mario Carneiro]

unfortunately it times out before getting to 51

[Yaël Dillies]

That's already much better than we what we currently have! Ours times out at 15.

[Mario Carneiro]

oh hey, I ran it at the console and it gave roth 51 = 17

[Mario Carneiro]

after 49 seconds

[Mario Carneiro]

I leave the proof of correctness as an exercise to the reader :D

[Yaël Dillies]

This ios gonna be a tough one :cold_sweat:

[Yaël Dillies]

Is there any reason to use bool here? Does it compute faster somehow?

[Mario Carneiro]

faster than what?

[Yaël Dillies]

than Prop

[Mario Carneiro]

prop doesn't compute at all; you would have to write a decidability instance on top of this, which would more than double the length (more because the decidability instance is dependent over the original function so it has to do a bunch of cases and simp stuff)

[Mario Carneiro]

you can think of bool as being a cheap way to bundle a prop with its decidability instance

[Mario Carneiro]

Also, I want to be very sure that the && and || are short circuiting here, otherwise the algorithm doesn't work at all

[Yaël Dillies]

Aaah okay. I had never seen how both ways of computing relate. And, to be honest, I had no idea how to compute anything remotely nontrivial until 4 days ago.

[Yaël Dillies]

ANd what's the correct way to get information out of a bool? That is, what should my lemma relating roth_number_nat/|add_salem_spencer and your roth be writing? a = tt?

[Mario Carneiro]

there are coercions both ways and simp lemmas every which way, so you don't have to acknowledge the difference for the most part

[Yaël Dillies]

So something like salem_spencer _ ↔ three_free _ will do?

[Mario Carneiro]

example (n : ℕ) : roth n = (roth_number_nat n, (list.range n).map roth_number_nat) := sorry

[Kevin Buzzard]

Is it better in lean 4?

[Yaël Dillies]

Yeah sure, but what about three_free? I will ned to prove that three_free is equivalent to add_salem_spencer to prove correctness of the algorithm.

[Mario Carneiro]

example (a : ℕ) (l : list ℕ)
  (h₁ : add_salem_spencer {n | n ∈ l}) (h₂ : list.chain (>) a l) :
  add_salem_spencer {n | n ∈ a :: l} ↔ three_free a l := sorry

[Mario Carneiro]

example (s n m d : ℕ) (α : list ℕ)
  (h₁ : add_salem_spencer {n | n ∈ α}) (h₂ : list.chain' (>) α)
  (hm : s + m = n + 1) (hd : roth_number_nat n = d + α.length) :
  ¬ roth_aux ((list.range s).map roth_number_nat) m d α ↔
  (∀ β : set ℕ, (∀ x ∈ β, x ≤ n) → {n | n ∈ α} ⊆ β →
    add_salem_spencer β → nat.card β ≤ n) := sorry

[Bhavik Mehta]

Yaël Dillies said:

That's already much better than we what we currently have! Ours times out at 15.

This is more awkward than I expected; our original one computes via #eval at 17 (maybe 18); but := rfl or := dec_trivial times out instead, similarly (roth 40).1 = 15 := dec_trivial doesn't work either :/

[Bhavik Mehta]

Nonetheless the new version does get further than my crappy version in both metrics

[Yaël Dillies]

Is there any way to reuse calculations from one lemma for another? This would clearly come in handy here.

[Bhavik Mehta]

If there were a lemma which stated the result of some calculations, then a later lemma wouldn't need to repeat them since they'd been proved

[Yaël Dillies]

Yes of course, but I was fearing that the results would be too long to state.

[Yaël Dillies]

While I was under the Channel I figured out that Mario's version is compact enough for this.

[Yaël Dillies]

Okay, I managed to prove

lemma three_free_spec (hl : list.chain (>) a l) (h₁ : add_salem_spencer {n | n ∈ l}) :
  three_free a l ↔ add_salem_spencer {n | n ∈ a :: l} :=

This was Not So Fun. Also, why is add_salem_spencer {n | n ∈ l} needed?

[Yaël Dillies]

This is becoming big, so I'm gonna get rid of the explicit_values bit of the PR.

[Mario Carneiro]

because add_salem_spencer is about sets while three_free is about lists. Alternatively, you could coerce the list to a finset and then to a set, but there isn't a coercion from lists directly to sets at the moment.

[Mario Carneiro]

I'm curious what your proof was, because it seems like it wouldn't be that bad

[Mario Carneiro]

In fact, it might help to have a theorem about add_salem_spencer (insert a s) and apply it here

[Yaël Dillies]

I did add a theorem add_salem_spencer_insert to reduce the number of cases to check from 3 (new element on the left of the LHS, on the right of the LHS, on the RHS) to 2 (on the LHS, on the RHS).

The proof

lemma three_free_spec (hl : chain (>) a l) (h₁ : add_salem_spencer {n | n ∈ l}) :
  three_free a l ↔ add_salem_spencer {n | n ∈ a :: l} :=
begin
  induction l with d l ih,
  { refine iff_of_true rfl _,
    simp_rw [mem_singleton, set.set_of_eq_eq_singleton],
    exact add_salem_spencer_singleton a },
  have : {n : ℕ | n ∈ a :: d :: l} = insert d {n : ℕ | n ∈ a :: l},
  { ext,
    simp only [set.mem_insert_iff, mem_cons_iff, set.mem_set_of_eq],
    exact or.left_comm },
  rw [this, three_free, bool.band_comm, band_coe_iff, bool.coe_all,
    ih (hl.mono $ sublist_cons _ _) (h₁.mono $ l.subset_cons _), add_salem_spencer_insert],
  simp_rw bool.coe_to_bool,
  refine and_congr_right (λ hl', ⟨λ hs, ⟨_, _⟩, _⟩),
  { rintro b c (rfl | hb) (rfl | hc),
    { exact add_right_cancel },
    { rintro h,
      cases hl with _ _ _ _ hdb hl,
      have hcd : c < d := hl.rel hc,
      exact ((add_lt_add hcd $ hcd.trans hdb).ne' h).elim },
    { exact λ h, ((add_lt_add (rel_of_chain_cons hl : c > d) $
        hl.rel $ mem_cons_of_mem _ hb).ne h).elim },
    { exact h₁ (mem_cons_self _ _) (mem_cons_of_mem _ hb) (mem_cons_of_mem _ hc) } },
  { rintro b c (rfl | hb) (rfl | hc),
    { exact λ _, rfl },
    { exact λ h, (hs _ hc h).elim },
    { exact λ h, (hs _ hb $ (add_comm _ _).trans h).elim },
    { exact h₁ (mem_cons_of_mem _ hb) (mem_cons_of_mem _ hc) (mem_cons_self _ _) } },
  { rintro ⟨_, hs⟩ b hb h,
    have hab : a = b := hs (mem_cons_self _ _) (or.inr hb) h,
    rw hab at hl h,
    have hbd : b > d := rel_of_chain_cons hl,
    exact (add_lt_add hbd hbd).ne' h }
end

[Yaël Dillies]

Mario Carneiro said:

because add_salem_spencer is about sets while three_free is about lists.

That explains the notation {n | n ∈ l}, but not why we need the hypothesis, unless you mean because of the order in the list?

[Yaël Dillies]

Also, is this supposed to be true?

lemma three_free.of_cons' (h : chain (>) a l) (hl : three_free a (b :: l)) : three_free b l :=

[Mario Carneiro]

no

[Mario Carneiro]

three_free is checking only whether adding a to l keeps it three-free

[Yaël Dillies]

Yeah okay that's what I thought. You never check for b on the LHS.

[Mario Carneiro]

also the ordering relation is used to ensure that the only thing we have to check is a + c = b + b and not other permutations of that

[Mario Carneiro]

but I guess you figured that out already

[Yaël Dillies]

Yeah, that's what I was trying to get to before Bhavik sent the paper.

[Mario Carneiro]

do you have an #mwe version of that proof? I pulled the PR but I don't have add_salem_spencer_singleton, bool.coe_all and possibly others

[Yaël Dillies]

Let me 5min. I'll remove the explicit_values off the PR and put that on a new branch small_roth.

[Mario Carneiro]

I suspect that a lot of the work can be reduced to things like list.pairwise_iff_chain for sorted lists, and expressing the salem spencer property as pairwise of something

[Mario Carneiro]

although it's a ternary property which makes it harder

[Yaël Dillies]

Pushed!

[Yaël Dillies]

I thought about that, but decided it wasn't worth changing because the list appearing in list.chain (d :: l) has one cons while the one in list.pairwise (a :: d :: l) has two, so you spend more time just looking into it.

[Mario Carneiro]

It's still missing coe_all and list.chain.mono. (BTW for the second one I've inferred the theorem statement

lemma list.chain.mono {α} {R : α → α → Prop} {a : α} {l l' : list α}
  (H : l' <+ l) (h : l.chain R a) : l'.chain R a := sorry

but I would have preferred this name to be dealing with monotonicity wrt R.)

[Yaël Dillies]

bool.coe_all and list.chain.mono are in namespaces at lines 53 and 83 respectively.

[Yaël Dillies]

i'll be happy to rename list.chain.mono into list.chain.sublist because it's also clearer that it's monotonicity wrt list.sublist, not list.prefix or list.suffix.

[Mario Carneiro]

Yaël Dillies said:

bool.coe_all and list.chain.mono are in namespaces at lines 53 and 83 respectively.

in the salem_spencer PR? I don't see it.

[Yaël Dillies]

No, in branch#small_roth

[Yaël Dillies]

Yaël Dillies said:

Let me 5min. I'll remove the explicit_values off the PR and put that on a new branch small_roth.

Sorry you must've missed that

[Yaël Dillies]

Mario Carneiro said:

example (n : ℕ) : roth n = (roth_number_nat n, (list.range n).map roth_number_nat) := sorry

This is missing a reverse. list.range goes the wrong way.

[Mario Carneiro]

list.iota might work then

[Mario Carneiro]

it might be off by one

[Yaël Dillies]

What is each variable in roth_aux supposed to represent?

[Mario Carneiro]

Here's a shorter proof for three_free_spec making more use of pairwise:

theorem list.forall_of_forall_of_pairwise_flip {α} {R : α → α → Prop}
  {l : list α} (H₁ : ∀ x ∈ l, R x x) (H₂ : pairwise R l) (H₃ : pairwise (flip R) l) :
  ∀ (x ∈ l) (y ∈ l), R x y := sorry

lemma three_free_spec (hl : chain (>) a l) (h₁ : add_salem_spencer {n | n ∈ l}) :
  three_free a l ↔ add_salem_spencer {n | n ∈ a :: l} :=
begin
  transitivity list.pairwise (λ b c, a + c ≠ b + b) l,
  { clear hl h₁,
    induction l; simp [three_free, list.pairwise.nil, list.pairwise.cons, bool.coe_all, *] },
  have : {n : ℕ | n ∈ a :: l} = insert a {n : ℕ | n ∈ l},
  { ext, simp only [set.mem_insert_iff, mem_cons_iff, set.mem_set_of_eq] },
  rw [this, add_salem_spencer_insert],
  refine ⟨λ H, ⟨h₁, λ b c hb hc e, _, λ b c hb hc e, _⟩, λ H, _⟩,
  { cases forall_of_forall_of_pairwise_flip _ H _ _ hc _ hb e,
    { exact λ b hb, ne_of_gt (add_lt_add_right (hl.rel hb) _) },
    have : transitive (>) := λ a b c h1 h2, lt_trans h2 h1,
    refine (pairwise_cons.1 ((chain_iff_pairwise this).1 hl)).2.imp_of_mem (λ b c hb hc h, _),
    exact ne_of_gt (add_lt_add (hl.rel hc) h) },
  { cases ne_of_lt (add_lt_add (hl.rel hb) (hl.rel hc)) e },
  { refine pairwise.imp_mem.2 (pairwise_of_forall (λ c b hc hb e, _)),
    exact ne_of_gt (hl.rel hb) (H.2.1 hb hc e) },
end

[Mario Carneiro]

@Yaël Dillies

• sz is the list of previous roth values, but only up to a bound s satisfying s + m = n + 1.
• n is a constant, and does not actually appear in roth_aux, but s goes down as m goes up.
• In the paper, m corresponds to |α|.
• d corresponds to roth n - #α; we're trying to find out if roth (n+1) = roth n or roth (n+1) = roth n + 1, so if d underflows then we're done.
• α is the bitstring α from the paper, except that it is represented as a list of nat instead of a 0-1 string, so α.length is #α and |α| has to be tracked separately (that's m).

[Mario Carneiro]

You can read a lot of this from the statement of roth_aux_spec

[Mario Carneiro]

Oh, the statement of roth_aux_spec is wrong, the n at the end should be roth_number_nat n:

example (s n m d : ℕ) (α : list ℕ)
  (h₁ : add_salem_spencer {n | n ∈ α}) (h₂ : list.chain' (>) α)
  (hm : s + m = n + 1) (hd : roth_number_nat n = d + α.length) :
  ¬ roth_aux ((list.range s).map roth_number_nat) m d α ↔
  (∀ β : set ℕ, (∀ x ∈ β, x ≤ n) → {n | n ∈ α} ⊆ β →
    add_salem_spencer β → nat.card β ≤ roth_number_nat n) := sorry

[Mario Carneiro]

Here's another way to write roth_aux in terms of a set of lemmas which expresses a nondeterministic computation along the lines of roth_aux. @Yaël Dillies Do you think it would be easier to prove these lemmas instead of roth_aux_spec? The nondeterminism is a boon, because it means that many things don't have to be checked: any branches of the search that turned out not to matter are not explored.

def roth_ub_aux (s m d : ℕ) (α : list ℕ) : Prop :=
∀ n, s + m = n + 1 → add_salem_spencer {n | n ∈ α} → list.chain' (>) α →
∀ β : set ℕ, (∀ x ∈ β, x ≤ n) → {n | n ∈ α} ⊆ β → add_salem_spencer β → nat.card β ≤ d + α.length

theorem roth_ub_aux_zero (n m d : ℕ) (α : list ℕ) : roth_ub_aux 0 m d α := sorry

def roth_ub_aux₁ (s m d : ℕ) (α : list ℕ) : Prop :=
d ≥ roth_number_nat s ∨ roth_ub_aux s (m + 1) d α

def roth_ub_aux₂ (s m d : ℕ) (α : list ℕ) : Prop :=
¬ three_free m α ∨ ∃ d', d = d' + 1 ∧ roth_ub_aux s (m + 1) d' (m :: α)

theorem roth_ub_aux_succ {s m d α}
  (h₁ : roth_ub_aux₁ s m d α) (h₂ : roth_ub_aux₂ s m d α) : roth_ub_aux (s+1) m d α := sorry

theorem roth_ub_aux₁_left {s m d α}
  (h : roth_number_nat s ≤ d) : roth_ub_aux₁ s m d α := or.inl h

theorem roth_ub_aux₁_right {s m d α}
  (h : roth_ub_aux s (m+1) d α) : roth_ub_aux₁ s m d α := or.inr h

theorem roth_ub_aux₂_left {s m d α}
  (h : three_free m α = ff) : roth_ub_aux₂ s m d α := or.inl (by simp [h])

theorem roth_ub_aux₂_right {s m d α}
  (h : roth_ub_aux s (m+1) d (m::α)) : roth_ub_aux₂ s m (d+1) α := or.inr ⟨_, rfl, h⟩

theorem roth_ub_aux_out {n d}
  (h : roth_ub_aux (n+1) 0 d []) : roth_number_nat (n+1) ≤ d := sorry

[Mario Carneiro]

This set of lemmas is tuned for proving that roth (n+1) = roth n, because that's the hard case; you can also skip a row of roth numbers that are all the same and only work on the last case before it increases. When the number goes up, it's easy because you just need a counterexample

[Yaël Dillies]

What do you mean by "nondeterministic computation"? I'm a bit lost by what you're trying to do, I think.

[Bhavik Mehta]

Mario Carneiro said:

Here's another way to write roth_aux in terms of a set of lemmas which expresses a nondeterministic computation along the lines of roth_aux. Yaël Dillies Do you think it would be easier to prove these lemmas instead of roth_aux_spec? The nondeterminism is a boon, because it means that many things don't have to be checked: any branches of the search that turned out not to matter are not explored.

def roth_ub_aux (s m d : ℕ) (α : list ℕ) : Prop :=
add_salem_spencer {n | n ∈ α} → list.chain (>) m α →
∀ β : finset ℕ, (∀ x ∈ β, x < s + m) → β.filter (< m) = list.to_finset α →
add_salem_spencer (β : set ℕ) → β.card ≤ d + α.length

theorem roth_ub_aux_zero (n m d : ℕ) (α : list ℕ) : roth_ub_aux 0 m d α := sorry

def roth_ub_aux₁ (s m d : ℕ) (α : list ℕ) : Prop :=
d ≥ roth_number_nat s ∨ roth_ub_aux s (m + 1) d α

def roth_ub_aux₂ (s m d : ℕ) (α : list ℕ) : Prop :=
¬ three_free m α ∨ ∃ d', d = d' + 1 ∧ roth_ub_aux s (m + 1) d' (m :: α)

theorem roth_ub_aux_succ {s m d α}
  (h₁ : roth_ub_aux₁ s m d α) (h₂ : roth_ub_aux₂ s m d α) : roth_ub_aux (s+1) m d α := sorry

theorem roth_ub_aux₁_left {s m d α}
  (h : roth_number_nat s ≤ d) : roth_ub_aux₁ s m d α := or.inl h

theorem roth_ub_aux₁_right {s m d α}
  (h : roth_ub_aux s (m+1) d α) : roth_ub_aux₁ s m d α := or.inr h

theorem roth_ub_aux₂_left {s m d α}
  (h : three_free m α = ff) : roth_ub_aux₂ s m d α := or.inl (by simp [h])

theorem roth_ub_aux₂_right {s m d α}
  (h : roth_ub_aux s (m+1) d (m::α)) : roth_ub_aux₂ s m (d+1) α := or.inr ⟨_, rfl, h⟩

theorem roth_ub_aux_out {n d}
  (h : roth_ub_aux n 0 d []) : roth_number_nat n ≤ d := sorry

This looks very promising!

[Mario Carneiro]

Yaël Dillies said:

What do you mean by "nondeterministic computation"? I'm a bit lost by what you're trying to do, I think.

The set of lemmas mentioned there can be used to construct a proof of roth_number_nat n <= d in a fairly obvious way: first apply roth_ub_aux_out, then roth_ub_aux_succ, then for each subgoal apply roth_ub_aux[₁,₂]_left or roth_ub_aux[₁,₂]_right, and keep going until you reach a leaf where you apply roth_ub_aux_zero. This exactly mimics the evaluation of the boolean expression in roth_aux, assuming that it evaluates to ff.

The part that is nondeterministic here is that unlike roth_aux, there is no "order of evaluation" here. In each of the two disjunctions you have a choice of two proofs, but for a boolean function a && b = ff you have to first evaluate a = ff, or else a = tt and then b = ff. With the nondeterministic version you either evaluate a = ff or b = ff, so the computation of a = tt is saved (a significant win in the case a := three_free a l).

Furthermore, we also have an advantage in the first conjunct. Evaluating d < s is cheap, so it's not that important to skip it, but in the revised lemmas that is actually a roth_number_nat s ≤ d assumption, which can be a reference to a previously proved theorem. But more powerfully, we can choose to use roth_ub_aux₁_right even when roth_number_nat s ≤ d is true. This is a bunch of extra work so at first it might seem counterproductive, but this can be used in order to skip steps in the Roth sequence.

For example, roth 9 = 5 while roth 5 .. 8 = 4, so to prove all the values in this neighborhood it suffices to give bounds like so:

roth 4 <= 3
4 <= roth 5
roth 8 <= 4
5 <= roth 9
...

Now consider the proof of roth 8 <= 4, assuming we have the previous lines as lemmas. We don't have a proof that roth 7 <= 4 because we are skipping steps, so if it comes up that we need roth 7 <= 4 or roth 6 <= 4 when evaluating roth_ub_aux₁_left, we can just take the roth_ub_aux₁_right branch instead.

[Yaël Dillies]

So you don't mean to actually compute here? But rather to skip branches of the actual computation?

[Mario Carneiro]

Depends on what you mean by "actual computation". The proof term encodes a witness for a nondeterministic computation, while the tactic that produces the proof term executes a deterministic computation (in a significantly more efficient machine model). Depending on how things go even the tactic computation might skip some steps if we choose to evaluate it only at certain values or seed it with witnesses from the paper or some other data constructed e.g. in a CAS. Putting these approaches together you can get significantly further than you would otherwise

[Yaël Dillies]

@Mario Carneiro, are you sure you didn't make an off by one error in the set of lemma? I think roth_aux_succ is false for a = 0, m = 0, d = 0, l = [0].

lemma roth_aux_succ (h₁ : roth_aux₁ a m d l) (h₂ : roth_aux₂ a m d l) : roth_aux (a + 1) m d l :=

[Yaël Dillies]

Update: I'm not so sure anymore, but I still fail to understand what made you choose those definitions.

[Mario Carneiro]

@Yaël Dillies The idea behind roth_aux deferring to roth_aux₁ and roth_aux₂ is that the successor case (that is, roth_aux (a+1)) for roth_aux is

roth_aux (a + 1) m d l =
  (d ≥ roth_number_nat a ∨ roth_aux a (m + 1) d l) ∧
  (¬ three_free m l ∨ ∃ d', d = d' + 1 ∧ roth_aux a (m + 1) d' (m :: l))

[Yaël Dillies]

How immediate is it to rewrite it as such?

[Mario Carneiro]

In the original algorithm, this was by definition and the hard part with proving that the algorithm's result is in fact constraining the roth number; in this version the result is correct by definition but this equality (actually we only need one direction of implication here) is the hard part

[Mario Carneiro]

But it shouldn't be too hard, assuming I got the definition of roth_aux (the algorithm's invariant) correct

[Yaël Dillies]

My draft proof is getting longer and longer... and mostly I do not see this head ∧ in what I'm doing.

[Mario Carneiro]

I forget all the details, but I believe that we are trying to prove something about all bit sequences starting with l, and one part of the /\ is proving stuff about the ff::l sequences and the other part is tt::l sequences

[Yaël Dillies]

So I should case on whether m ∈ l or something.

[Mario Carneiro]

er, I guess we encoded them as strictly decreasing lists of numbers instead of bit strings, hence by the second part has m::l and the other has l

[Yaël Dillies]

Currently, I'm casing on roth_aux₁ a m d l and roth_aux₂ a m d l, which yields four cases looking quite distinctly different.

[Mario Carneiro]

what's in the context?

[Yaël Dillies]

Here's the context before casing

l: list ℕ
adm: ℕ
h₁: roth_aux₁ a m d l
h₂: roth_aux₂ a m d l
hl: chain gt m l
s: finset ℕ
hs₀: ∀ (x : ℕ), x ∈ s → x < a + 1 + m
hs₁: finset.filter (λ (_x : ℕ), _x < m) s = l.to_finset
hs₂: add_salem_spencer ↑s
hl₃: l.nodup
hls: ∀ ⦃x : ℕ⦄, x ∈ l → x ∈ s
⊢ (finset.filter (not ∘ λ (_x : ℕ), _x < m) s).card ≤ d

[Yaël Dillies]

Note that I simplified the definition of roth_aux because the first assumption was redundant.

[Mario Carneiro]

?

[Mario Carneiro]

which assumption did you drop

[Yaël Dillies]

def old_roth_aux (a m d : ℕ) (l : list ℕ) : Prop :=
add_salem_spencer {n | n ∈ l} → list.chain (>) m l →
  ∀ s : finset ℕ, (∀ x ∈ s, x < a + m) → s.filter (< m) = l.to_finset →
    add_salem_spencer (s : set ℕ) → s.card ≤ d + l.length
-- VS
def roth_aux (a m d : ℕ) (l : list ℕ) : Prop :=
list.chain (>) m l → ∀ s : finset ℕ, (∀ x ∈ s, x < a + m) → s.filter (< m) = l.to_finset →
  add_salem_spencer (s : set ℕ) → s.card ≤ d + l.length

[Mario Carneiro]

I think you still need to know add_salem_spencer {n | n ∈ l} because it's used in the correctness proof for three_free

[Mario Carneiro]

it's fine if you derive it from the other hypotheses, although I can't tell if it's shorter than having the redundant assumption and using three_free_spec to extend it

[Yaël Dillies]

Yes, I can derive it

[Mario Carneiro]

Yes, I think you want to case on m ∈ l. If it is true, then you case on roth_aux₂ and ignore roth_aux₁, and vice versa if it is false

[Yaël Dillies]

That makes more sense. I was deriving m ∈ l from casing on roth_aux₁ and roth_aux₂.

[Yaël Dillies]

It works much better when you understand what's happening. Who would have thought :grinning:

[Yaël Dillies]

Aaand, it's done!

[Kevin Buzzard]

When I started with lean I'd just leap into every proof on the basis that I was a good puzzle-solver so I should just be able to follow my nose and do everything first try. I soon learnt that this wasn't always the case. I remember trying Scott Morrison's category theory exercises in LFTCM20 and realising very quickly that paper and pencil was going to be essential :-)

[Yaël Dillies]

People keep asking me whether Lean requires rather maths or programming, and the answer is clear, unless you get into metaprogramming or the typeclass hierarchy.