Zulip Chat Archive

Stream: new members

Topic: non-empty lists, again


view this post on Zulip Vincent Beffara (Oct 25 2019 at 22:04):

Hi again,
Still playing around with various ways to define non-empty lists, this time following advice and using V \times list V to be able to use library functions. I still would like to make inductive definitions using pattern matching (if only for practice), but I am getting complaints about well-founded relations,

def llist (V : Type) : Type := V × list V

def simple {V : Type} : llist V -> Prop
    | v,[]   := true
    | v,w::l := ¬ v  w::l  simple w,l

What would be the proper way to do what I want? It would be very nice to avoid auxiliary functions and piling to_list and from_list, because that would push me towards defining an inductive type and having to reinvent the wheel...

view this post on Zulip Bryan Gin-ge Chen (Oct 25 2019 at 22:42):

Unfortunately I haven't been able to solve your issue but this is the doc page that's usually suggested when Lean has trouble proving something well-founded. Apologies if you've already seen it.

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 07:17):

This works:

def llist (V : Type) : Type := V × list V

def simple {V : Type} : llist V  Prop
    | (v,[])   := true
    | (v,w::l) := ¬ v  w::l  simple (w,l)
    using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (list.length  prod.snd)]}

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:06):

Thanks for the working version! Still the version with an auxiliary function,

def simple_l {V : Type} : list V -> Prop | [] := true | (x::xs) := ¬ x  xs  simple_l xs

def simple {V : Type} : V × list V -> Prop | (x,xs) := simple_l (x::xs)

feels much simpler. I'm ok with incantations about measure_wf that I don't understand (yet?) but I really would prefer not having to put them near the definition of simple because there are a lot of other things that I am defining in a similar way.

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:29):

Ah, in fact I still get an error with your version:

error: failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (llist V)
    (@has_well_founded.mk (llist V) (@measure (llist V) (λ (l : llist V), @length V (@prod.snd V (list V) l))) _)
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
tactic failed, there are no goals to be solved

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:31):

But this does:

def simple {V : Type} : llist V  Prop
    | (v,[])   := true
    | (v,w::l) := have length l < length (w::l), by { simp }, ¬ v  w::l  simple (w,l)
    using_well_founded wf_tacs

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 20:32):

Bryan's version works for me. Which version of Lean are you using?

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 20:33):

Ah, my version fails if I add import data.list.basic...

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 20:33):

because simp gets too good.

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:34):

All right, explanation is in mathlib/src/tactic/well_founded_tactics.lean

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 20:34):

Yep, you need to add a dec_tac line from that file:

import tactic.well_founded_tactics
import data.list.basic

def llist (V : Type) : Type := V × list V

def simple {V : Type} : llist V  Prop
    | (v,[])   := true
    | (v,w::l) := ¬ v  w::l  simple (w,l)
    using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (list.length  prod.snd)],
    dec_tac := well_founded_tactics.default_dec_tac'}

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 20:44):

I wonder if this issue with default_dec_tac described in tactic/well_founded_tactics.lean is something which ought to be addressed in 3.5? @Simon Hudon

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:48):

In the meantime, is there any way to attach the information to use wf_tacs to the type llist V rather than having to mention it with every inductive definition?

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:49):

Or to cheat by using a slightly more complicated measure instead of list.length so that the default tactic works again, but that would feel a little dirty ...

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 20:50):

I would be curious to know the answers to those questions too.

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:51):

Like so:

def llist (V : Type) : Type := V × list V
instance llist_wf {V : Type} : has_well_founded (llist V) := ⟨_, measure_wf ((λ n, n+n)  list.length  prod.snd)

def simple {V : Type} : llist V  Prop
    | (v,[])   := true
    | (v,w::l) := ¬ v  w::l  simple (w,l)

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 20:53):

What's the reason for (λ n, n+n) ? I removed it and it still works for me.

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:54):

Ah, that's the dirty trick to answer my second question, if I leave it out then it fails again with the "no goals to be solved" error

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 20:55):

Yes, you're right. I had some interfering definitions that confused me.

view this post on Zulip Vincent Beffara (Oct 26 2019 at 20:56):

(\lambda n, 2*n) apparently is too transparent though

view this post on Zulip Mario Carneiro (Oct 26 2019 at 21:23):

I think simple_l is list.nodup

view this post on Zulip Vincent Beffara (Oct 26 2019 at 21:51):

Yes it is! Hadn't grepped for that ...


Last updated: May 10 2021 at 00:31 UTC