# Zulip Chat Archive

## 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]

then everything works as advertised

#### 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:40):

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

#### 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 | 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 (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 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 (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