rw div insufficient for defining equation

Stream: new members

[Plam]

Hi!

I'm working my way through theorem proving in Lean and have hit a bit of a snag.

In section 8.4 we define div via well-founded recursion (I have called it div'). Then we are told that we can prove the defining equation of div as follows

example (x y : ℕ) :
  div' x y = if 0 < y ∧ y ≤ x then div' (x - y) y + 1 else 0 :=
by simp [div']

but when I attempt this, I get an unsolved goal. Specifically,

well_founded.fix lt_wf div'.F x y = ite (0 < y ∧ y ≤ x) (1 + well_founded.fix lt_wf div'.F (x - y) y) 0

Is this because my version of div' lacks something div has? Something has changed in Lean since that was written? I've done something wrong?

Thanks for any guidance

(By the way, #eval doesn't work in the super fast way described in the book for me. #eval fib 100 doesn't work, never mind #eval fib 10000. Seems unlikely they're related, but thought it worth mentioning!)

[Patrick Massot]

Could you post a complete example? If I simply type in a Lean file:

open nat

def div : ℕ → ℕ → ℕ
| x y :=
  if h : 0 < y ∧ y ≤ x then
    have x - y < x,
      from sub_lt (lt_of_lt_of_le h.left h.right) h.left,
    div (x - y) y + 1
  else
    0

example (x y : ℕ) :
  div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 :=
by rw [div]

then everything works as advertised

[Plam]

That's good to know! Trying it out with my definition using the equation compiler like that works, but it doesn't work using well_founded.fix directly.

Here's the example:

open nat

def div_rec_lemma' {x y : ℕ} : 0 < y ∧ y ≤ x → x - y < x :=
λ h, sub_lt (lt_of_lt_of_le h.left h.right) h.left

def div'.F (x : ℕ) (f : Π x₁, x₁ < x → ℕ → ℕ) (y: ℕ) : ℕ :=
if h : 0 < y ∧ y ≤ x then
  f (x - y) (div_rec_lemma' h) y + 1
else
  zero

def div' := well_founded.fix lt_wf div'.F

def div'' : ℕ → ℕ → ℕ
| x y :=
  if h : 0 < y ∧ y ≤ x then
    have x - y < x,
      from sub_lt (lt_of_lt_of_le h.left h.right) h.left,
    div'' (x - y) y + 1
  else
    0

-- Fails!:
example (x y : ℕ) :
  div' x y = if 0 < y ∧ y ≤ x then div' (x - y) y + 1 else 0 :=
by rw [div']

-- Works!:
example (x y : ℕ) :
  div'' x y = if 0 < y ∧ y ≤ x then div'' (x - y) y + 1 else 0 :=
by rw [div'']

[Patrick Massot]

I'm not an expert at well founded recursion, but I think you could try reading https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md

[Andrew Ashworth]

regarding fib 100 being slow: the docs are outdated. automatic memoization was disabled awhile back

[Plam]

That was a useful read, but I appear not to have internalised it yet! I introduced a hypothesis the well foundedness checker seems to want, and I fail to make progress:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (psum (Σ' (m : ℕ), ℕ) (Σ' (m n : ℕ), ℕ))
    (@has_well_founded_of_has_sizeof (psum (Σ' (m : ℕ), ℕ) (Σ' (m n : ℕ), ℕ))
       (@psum.has_sizeof (Σ' (m : ℕ), ℕ) (Σ' (m n : ℕ), ℕ)
          (@psigma.has_sizeof ℕ (λ (m : ℕ), ℕ) nat.has_sizeof (λ (a : ℕ), nat.has_sizeof))
          (@psigma.has_sizeof ℕ (λ (m : ℕ), Σ' (n : ℕ), ℕ) nat.has_sizeof
             (λ (a : ℕ), @psigma.has_sizeof ℕ (λ (n : ℕ), ℕ) nat.has_sizeof (λ (a : ℕ), nat.has_sizeof)))))
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
failed
state:
m n : ℕ,
h₁ : n + m < nat.succ n + nat.succ m
⊢ n + m < nat.succ m + nat.succ n

[Kevin Buzzard]

Does this help: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md ?

[Kevin Buzzard]

Note that h\1 is not what you want to prove; the issue is that it tried to solve the goal using an assumption but h\1 is not quite the right assumption.

[Kevin Buzzard]

Oh sorry, I see Patrick already posted that.

[Chris Hughes]

sometime adding dec_tac := tactic.assumption to the using_well_founded helps.

[Kevin Buzzard]

Maybe you should post some code rather than just the error

[Chris Hughes]

Although this definition should be well founded according to the default well founded relation, which is the lexicographic ordering.

[Chris Hughes]

Depending on the other cases.

[Plam]

Thanks for the hints. Having corrected my h\1, I still end up with the error. Here's the code prompting the error (still broken in several places)

mutual theorem add_comm, add_assoc
with add_comm : ∀ m n, m + n = n + m
| 0 n := zero_add n
| m 0 := by simp [zero_add, add_zero]
| (nat.succ m) (nat.succ n) :=
  have h₁ : n + m < nat.succ m + nat.succ n, from _,
  by { simp [add],
    rw [←succ_add_succ, ←succ_add_succ, ←add_comm m n] }
with add_assoc : ∀ m n p, (m + n) + p = m + (n + p)
| 0 n p := by simp [zero_add]
| m 0 p := by simp [add_zero, zero_add]
| m n (p + 1) := by simp [add_assoc n p 1, add, add_comm]

Note that add has been defined (and infixed as +) locally

[Scott Morrison]

Plam, you should post a minimal working example, i.e. with everything need for someone to run it locally.

[Plam]

Gotcha! Sorry for being slow on the uptake on that

namespace hidden
def add (m : ℕ) : ℕ → ℕ
| 0 := m
| (nat.succ n) := nat.succ (add n)

local infix ` + ` := add
local attribute [pattern] add

theorem add_zero  : ∀ m, (m + 0) = m := λ m, rfl
theorem zero_add : ∀ m, 0 + m = m
| 0 := rfl
| (n + 1) := by simp [add, zero_add n]

theorem succ_add_succ : ∀ m n, nat.succ (m + n) = nat.succ m + n
| m 0 := rfl
| m (n + 1) := by simp [add, succ_add_succ m n]

mutual theorem add_comm, add_assoc
with add_comm : ∀ m n, m + n = n + m
| 0 n := zero_add n
| m 0 := by simp [zero_add, add_zero]
| (nat.succ m) (nat.succ n) :=
  by { simp [add, add_comm m n, succ_add_succ m n]}
with add_assoc : ∀ m n p, (m + n) + p = m + (n + p)
| 0 n p := by simp [zero_add]
| m 0 p := by simp [add_zero, zero_add]
| m n 0 := by simp [add_zero]
| m n (p + 1) := by simp [add_assoc n p 1, add, add_comm ]
end hidden

[Kevin Buzzard]

You can easily prove add_assoc by itself without intertwining it with add_comm. add_assoc doesn't need any commutativity hypotheses.

[Kevin Buzzard]

What is your actual question? Proving associativity by induction on p and then proving commutativity afterwards is the standard way of doing it. Are you specifically trying to do it in a complicated way and then trying to get the equation compiler to sort it all out, or are you just wanting to prove it?

[Kevin Buzzard]

https://xenaproject.wordpress.com/2017/10/31/building-the-non-negative-integers-from-scratch/ is a (more tactic-oriented) approach

[Plam]

Thanks for the link. I don't mind not intertwining, but I do want to get practice with the equation compiler for proofs (as that is an explicit goal of the exercise)

[Plam]

Also I guess I'm explicitly interested in what is going wrong with the well-foundedness checker

[Plam]

(I got the assoc and comm proofs sorted based on what you said -- thanks!)