Zulip Chat Archive

Stream: new members

Topic: rw div insufficient for defining equation


view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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'']

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Mar 04 2019 at 15:44):

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

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 17:42):

Oh sorry, I see Patrick already posted that.

view this post on Zulip Chris Hughes (Mar 04 2019 at 17:42):

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

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 17:42):

Maybe you should post some code rather than just the error

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Mar 04 2019 at 17:44):

Depending on the other cases.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Plam (Mar 04 2019 at 23:34):

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

view this post on Zulip 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