Question about decreasing_by's hypotheses

Stream: new members

[casenc]

I'm attempting to write a function that computes Project Euler nº 9 (find the pythagorean triplet $(a,b,c)$ such that $a+b+c=1000$), and I'm struggling to prove that the function terminates

My progress so far is:

def PE₉ : Option Nat :=
  let rec go a b := match (a, b) with
    | (zero, zero)    => none
    | (zero, succ b') => go 999 b'
    | (succ a', _)    => if a^2 + b^2 = (1000-a-b)^2 then some (a*b*(1000-a-b))
                         else go a' b
  termination_by a + 1000 * b
  decreasing_by
    . sorry
    . sorry
  go 999 999

An important part of the would-be proof is that a = succ a' and b = succ b', but these hypotheses aren't available inside the decreasing_by block. How do I convince lean that this is the case?

(I hope this is the right channel to ask newbie questions, do tell if it's not)

[Dexin Zhang]

You can use match h : (a, b) to get equalities

def PE₉ : Option Nat :=
  let rec go a b := match h : (a, b) with
    | (zero, zero)    => none
    | (zero, succ b') => go 999 b'
    | (succ a', _)    => if a^2 + b^2 = (1000-a-b)^2 then some (a*b*(1000-a-b))
                         else go a' b
  termination_by a + 1000 * b
  decreasing_by
    all_goals
      simp at h
      simp [h.1, h.2]
    grind
  go 999 999

[casenc]

Brilliant, that's exactly what I was looking for
Thank you!

[Robin Arnez]

A bit simplified:

def PE₉ : Option Nat :=
  let rec go : Nat → Nat → Option Nat
    | 0, 0          => none
    | 0, b' + 1     => go 999 b'
    | a@(a' + 1), b => if a^2 + b^2 = (1000-a-b)^2 then some (a*b*(1000-a-b))
                       else go a' b
  termination_by a b => a + 1000 * b
  go 999 999

[casenc]

Why does this form not need a full decreasing_by proof, but the other does?

[Robin Arnez]

Because it can prove it on its own here

[casenc]

But not in the other?

[Robin Arnez]

I guess being simpler pays off

[casenc]

I continued to bash my head into this for a while, trying to solve it with the tools that I know exist, and it's finally accepted:

def PE₉ : Option Nat :=
  let rec go a b := match h : (a, b) with
    | (zero, zero)    => none
    | (zero, succ b') => go 999 b'
    | (succ a', _)    => if a^2 + b^2 = (1000-a-b)^2 then some (a*b*(1000-a-b))
                          else go a' b
  termination_by a + 1000 * b
  decreasing_by
    . simp at h
      rw [h.left, h.right, zero_add, mul_add, mul_one, add_comm]
      apply Nat.add_lt_add_left
      decide
    . simp at h
      rw [h.left]
      have x : a' + 1 + 1000 * b = a' + 1000 * b + 1 := by
        simp [add_assoc]
        rw [add_comm]
      rw [x]
      apply Nat.lt_add_one
  go 999 999

it's awful but it most certainly works

[Robin Arnez]

If you want to bash automation at it, decreasing_by all_goals grind

[Robin Arnez]

It's a bit more powerful than the simp + omega combo that's normally used.