using_well_founded

Stream: general

[Edward Ayers]

I'm looking at RB trees again. I found a really good implementation in Coq that I am copying over to Lean: https://github.com/coq/coq/blob/a1fc621b943dbf904705dc88ed27c26daf4c5e72/theories/MSets/MSetRBT.v
Here is the start of my code:
https://github.com/EdAyers/mathlib/blob/rb/data/rb.lean
My problem is that it can't prove that my definition of append is terminating automatically. Is there a quick fix for this kind of thing or am I going to have to use well_founded.fix? I can't figure out how to use the using_well_founded keyword.

[Kevin Buzzard]

Did you look at the docs at https://github.com/EdAyers/mathlib/blob/rb/docs/extras/well_founded_recursion.md ?

[Edward Ayers]

Ah thanks I haven't read that one yet

[Kevin Buzzard]

I'm not saying it solves your problem, but it does have a bunch of cool tricks.

[Edward Ayers]

One of the things it can't show is

⊢ tr.sizeof α lr < tr.sizeof α ll + (tr.sizeof α lr + 2)

Is there a tactic that will solve that instantaneously?

[Patrick Massot]

https://github.com/leanprover-community/mathlib-nursery/blob/master/src/tactic/monotonicity/interactive.lean#L571-L595 presumably

[Patrick Massot]

not yet in mathlib, but you can temporarily add a dependency to this repo

[Patrick Massot]

What's the problem with corelib rbtrees?

[Edward Ayers]

Corelib rbtrees don't have erase

[Edward Ayers]

And there are no proofs about them.

[Patrick Massot]

oh

[Edward Ayers]

I fixed this by adding my own has_well_founded instance

instance custom_wf : has_well_founded (tr α × tr α) := has_well_founded_of_has_sizeof (tr α × tr α)

[Edward Ayers]

Before it was using wf using lexical ordering which was throwing it.

[Edward Ayers]

at least I think that's why

[Leonardo de Moura]

@Edward Ayers The proofs are here https://github.com/leanprover/lean/tree/master/library/data/rbtree

[Kevin Buzzard]

(deleted)

[Edward Ayers]

thanks Leo! sorry I didn't spot them.

[Sebastien Gouezel]

I am trying to define a function using the equation compiler, but I don't understand how one is supposed to use using_well_founded. Here is a minimal example:

def P : ∀(n : with_top ℕ), Prop
| (some n) := true
| none := by {
    have : ∀n:ℕ, (n : with_top ℕ) < ⊤ := λn, with_top.coe_lt_top n,
    exact (∀n:ℕ, P n) }
using_well_founded { rel_tac := λ_ _, `[exact ⟨(<), with_top.well_founded_lt nat.lt_wf⟩],
dec_tac := tactic.assumption }

This fails with the message

The nested exception contains the failure state for the decreasing tactic.
nested exception message:
assumption tactic failed

[Simon Hudon]

Can you remove the by? You can do the same without it

[Sebastien Gouezel]

def P : ∀(n : with_top ℕ), Prop
| (some n) := true
| none :=
    have ∀n:ℕ, (n : with_top ℕ) < ⊤ := λn, with_top.coe_lt_top n,
    (∀n:ℕ, P n)
using_well_founded { rel_tac := λ_ _, `[exact ⟨(<), with_top.well_founded_lt nat.lt_wf⟩],
dec_tac := tactic.assumption }

fails in the same way.

[Mario Carneiro]

You have to use the term mode have

[Mario Carneiro]

oh but the second one also fails?

[Mario Carneiro]

oh, of course assumption fails here, you didn't give the right decreasing proof

[Mario Carneiro]

def P : ∀(n : with_top ℕ), Prop
| (some n) := true
| none := ∀ n : ℕ,
    have (n : with_top ℕ) < ⊤ := with_top.coe_lt_top n,
    P n
using_well_founded { rel_tac := λ_ _, `[exact ⟨(<), with_top.well_founded_lt nat.lt_wf⟩],
dec_tac := tactic.assumption }

[Sebastien Gouezel]

Thanks a lot. The problem is that assumption will not apply the parameter n to what I have proved previously, it has to be proved in the exact form it needs. Would the following be acceptable style?

def P : ∀(n : with_top ℕ), Prop
| (some n) := true
| none := (∀n:ℕ, P n)
using_well_founded {
  rel_tac := λ_ _, `[exact ⟨_, with_top.well_founded_lt nat.lt_wf⟩],
  dec_tac := `[apply with_top.coe_lt_top] }

[Rob Lewis]

That looks fine to me. But if for some reason, you wanted to keep your have statement in the original form, you could use apply_assumption as the decision tactic.