## Stream: new members

### Topic: non-empty lists, again

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

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

#### 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)⟩]}


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

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


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


#### Kevin Buzzard (Oct 26 2019 at 20:32):

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

#### Bryan Gin-ge Chen (Oct 26 2019 at 20:33):

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

#### Kevin Buzzard (Oct 26 2019 at 20:33):

because simp gets too good.

#### Vincent Beffara (Oct 26 2019 at 20:34):

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

#### 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'}


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

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

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

#### Bryan Gin-ge Chen (Oct 26 2019 at 20:50):

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

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


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

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

#### Bryan Gin-ge Chen (Oct 26 2019 at 20:55):

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

#### Vincent Beffara (Oct 26 2019 at 20:56):

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

#### Mario Carneiro (Oct 26 2019 at 21:23):

I think simple_l is list.nodup

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