Zulip Chat Archive

Stream: general

Topic: using_well_founded


view this post on Zulip Edward Ayers (Aug 28 2018 at 18:34):

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.

view this post on Zulip Kevin Buzzard (Aug 28 2018 at 18:36):

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

view this post on Zulip Edward Ayers (Aug 28 2018 at 18:37):

Ah thanks I haven't read that one yet

view this post on Zulip Kevin Buzzard (Aug 28 2018 at 18:38):

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

view this post on Zulip Edward Ayers (Aug 28 2018 at 18:41):

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?

view this post on Zulip Patrick Massot (Aug 28 2018 at 18:51):

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

view this post on Zulip Patrick Massot (Aug 28 2018 at 18:52):

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

view this post on Zulip Patrick Massot (Aug 28 2018 at 18:52):

What's the problem with corelib rbtrees?

view this post on Zulip Edward Ayers (Aug 28 2018 at 18:54):

Corelib rbtrees don't have erase

view this post on Zulip Edward Ayers (Aug 28 2018 at 18:55):

And there are no proofs about them.

view this post on Zulip Patrick Massot (Aug 28 2018 at 18:55):

oh

view this post on Zulip Edward Ayers (Aug 28 2018 at 19:19):

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 α)

view this post on Zulip Edward Ayers (Aug 28 2018 at 19:20):

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

view this post on Zulip Edward Ayers (Aug 28 2018 at 19:20):

at least I think that's why

view this post on Zulip Leonardo de Moura (Aug 28 2018 at 21:07):

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

view this post on Zulip Kevin Buzzard (Aug 28 2018 at 21:32):

(deleted)

view this post on Zulip Edward Ayers (Aug 28 2018 at 21:36):

thanks Leo! sorry I didn't spot them.

view this post on Zulip Sebastien Gouezel (Apr 18 2019 at 17:41):

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

view this post on Zulip Simon Hudon (Apr 18 2019 at 17:44):

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

view this post on Zulip Sebastien Gouezel (Apr 18 2019 at 17:45):

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.

view this post on Zulip Mario Carneiro (Apr 18 2019 at 17:46):

You have to use the term mode have

view this post on Zulip Mario Carneiro (Apr 18 2019 at 17:46):

oh but the second one also fails?

view this post on Zulip Mario Carneiro (Apr 18 2019 at 17:48):

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

view this post on Zulip Mario Carneiro (Apr 18 2019 at 17:49):

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 }

view this post on Zulip Sebastien Gouezel (Apr 18 2019 at 17:57):

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

view this post on Zulip Rob Lewis (Apr 18 2019 at 18:07):

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.


Last updated: May 11 2021 at 00:31 UTC