## Stream: new members

### Topic: rw div insufficient for defining equation

#### Plam (Mar 04 2019 at 14:12):

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 (Mar 04 2019 at 14:20):

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]


#### Plam (Mar 04 2019 at 14:24):

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 (Mar 04 2019 at 14:39):

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 (Mar 04 2019 at 15:44):

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

#### Plam (Mar 04 2019 at 17:39):

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 (Mar 04 2019 at 17:41):

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 (Mar 04 2019 at 17:42):

Oh sorry, I see Patrick already posted that.

#### Chris Hughes (Mar 04 2019 at 17:42):

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

#### Kevin Buzzard (Mar 04 2019 at 17:42):

Maybe you should post some code rather than just the error

#### Chris Hughes (Mar 04 2019 at 17:44):

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

#### Chris Hughes (Mar 04 2019 at 17:44):

Depending on the other cases.

#### Plam (Mar 04 2019 at 17:49):

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
| (nat.succ m) (nat.succ n) :=
have h₁ : n + m < nat.succ m + nat.succ n, from _,
with add_assoc : ∀ m n p, (m + n) + p = m + (n + p)
| 0 n p := by simp [zero_add]


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

#### Scott Morrison (Mar 04 2019 at 21:15):

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

#### Plam (Mar 04 2019 at 21:43):

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

theorem add_zero  : ∀ m, (m + 0) = m := λ m, rfl
theorem zero_add : ∀ m, 0 + m = m
| 0 := rfl

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]

with add_comm : ∀ m n, m + n = n + m
| 0 n := zero_add n
| (nat.succ m) (nat.succ n) :=
with add_assoc : ∀ m n p, (m + n) + p = m + (n + p)
| 0 n p := by simp [zero_add]
| m n 0 := by simp [add_zero]
end hidden


#### Kevin Buzzard (Mar 04 2019 at 21:54):

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

#### Kevin Buzzard (Mar 04 2019 at 21:59):

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 (Mar 04 2019 at 22:00):

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

#### Plam (Mar 04 2019 at 23:24):

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 (Mar 04 2019 at 23:34):

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

#### Plam (Mar 04 2019 at 23:35):

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

Last updated: May 13 2021 at 22:15 UTC