Zulip Chat Archive

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)