terminating recursion on recursive list-like structure

Stream: lean4

[Jared green]

im trying to define a function depth on variadic, but it fails to prove termination.

import Init.Prelude
import Init.Coe
import Mathlib.Data.List.Basic

variable {α : Type}
inductive IList α
  where
  | single : α -> IList α
  | cons : α -> IList α -> IList α

def IList.fold  (l : IList α)  (f : α -> b -> b)  (g : α -> b) : b :=
  match l with
  | single a => g a
  | cons a as => f a (fold as f g)

def IList.map  (f : α -> b) : IList α -> IList b
  | single a => single (f a)
  | cons a as => cons (f a) (map f as)

def IList.toList : IList α -> {l : List α // l ≠ []}
  | single a => ⟨ [a], by simp⟩
  | cons a as => ⟨ (a :: (IList.toList as)),by simp⟩

def IList.ofList (l: {l : List α // l ≠ []}) : IList α :=
  match l with
  | ⟨ [x], _ ⟩ => .single x
  | ⟨ x :: xs@(y :: ys),h⟩ => .cons x ( IList.ofList ⟨ xs, fun h => by aesop ⟩ )

instance : Coe (IList α) {l : List α // l ≠ []} where
  coe l := IList.toList l

instance : Coe {l : List α // l ≠ []} (IList α) where
  coe l := IList.ofList l

[h : DecidableEq α]
inductive variadic (α :Type) [h : DecidableEq α]
(pred : α -> Prop)
  where
  | vatom : α -> (variadic α pred)
  | vAnd : IList (variadic α pred) -> variadic α pred
  | vOr : IList (variadic α pred) -> variadic α pred
  | vNot : variadic α pred -> variadic α pred
--deriving DecidableEq

namespace variadic

 def depth (v : variadic α pred) : Nat :=
  match v with
  | vatom _ => 1
  | vAnd l => (IList.fold l (fun x y => max (depth x) y) (fun y => depth y)) + 1
  | vOr l => (IList.fold l (fun x y => max (depth x) y) (fun y => depth y)) + 1
  | vNot a => depth a + 1

[Shreyas Srinivas]

I suggest encoding depth into the variadic

[Shreyas Srinivas]

I am guessing lean can't see any obvious reason why max (depth x) y is decreasing.

[Jared green]

is that the only way? if the other ways are too complicated, i guess i will do that.

[Shreyas Srinivas]

I see it as the easy way out. Can you come up with a parameter that is decreasing in the recursion?

[Shreyas Srinivas]

I can't

[Shreyas Srinivas]

The recursive call is under a binder

[Jared green]

i thought maybe the definition of variadic could be changed some other way

[Shreyas Srinivas]

That's a whole other can of worms. I am just suggesting a way to salvage this definition with some extra additions.

[Henrik Böving]

If you define something along the lines of docs#List.attach and use it before the fold this is entirely possible.

[Henrik Böving]

Alternativley if you don't want to prove stuff about this particular function just give it a partial def

[Jared green]

@Henrik Böving how would that look?

[Henrik Böving]

What part?

[Jared green]

list.attach

[Henrik Böving]

inductive Tree (α : Type) where
| tip (x : α) : Tree α
| node (xs : List (Tree α)) : Tree α

def Tree.sum (t : Tree Nat) : Nat :=
  match t with
  | tip x => x
  | node xs => xs.attach.foldl (init := 0) (fun acc ⟨x, h⟩ => acc + x.sum)
termination_by t

[Henrik Böving]

The attach makes it such that Lean can see underneath the binder that the x is a member of xs and thus the function decreases

[Henrik Böving]

The terminaton_by is also optional in this case, Lean can see it on its own

[Jared green]

about implementing attach?

[Henrik Böving]

You can click the source button to see how it's done. Though it does require doing some additional effort yourself. I would suggest not to implement your own IList inductive and instead use an abbreviation for a List subtype

[Jared green]

like, first convert .toList.1?

[Henrik Böving]

I would suggest to not have IList at all and instead define abbrev ILIst (a : Type) : Type := {l : List α // l ≠ []}`

[Jared green]

then i would lose the ability to pattern match in the way i need.

[Edward van de Meent]

you could replace IList a -> with a -> List a ->, possibly?

[Jared green]

@Edward van de Meent what does that do?

[Edward van de Meent]

it means you get to use the preexisting List infrastructure, particularly  docs#List.attach which Henrik mentioned

[Edward van de Meent]

and you still can match.

[Jared green]

how would that look?

[Henrik Böving]

abbrev IList (α : Type) : Type := { xs : List α // xs ≠ [] }

@[match_pattern]
def IList.single (x : α) : IList α := ⟨[x], by simp⟩

@[match_pattern]
def IList.cons (x : α) (xs : IList α) : IList α := ⟨x :: xs, by simp⟩

def IList.isSingle (xs : IList α) : Bool :=
  match xs with
  | IList.single x => true
  | IList.cons x xs => false

it's a bit disappointing that this doesn't work

[Henrik Böving]

abbrev IList (α : Type) : Type := { xs : List α // xs ≠ [] }



def IList.isSingle (xs : IList α) : Bool :=
  match xs with
  | ⟨[x], _⟩ => true
  | ⟨x :: xs, _⟩ => false

though doing it by hand does very much work, so you can just pattern match

[Edward van de Meent]

turns out, all you really need is a bit of mutual recursion following the structure of your inductive:

import Init.Prelude
import Init.Coe
import Mathlib.Data.List.Basic

variable {α : Type}

inductive variadic (α :Type) (pred : α -> Prop)
  where
  | vatom : α -> (variadic α pred)
  | vAnd : variadic α pred → List (variadic α pred) -> variadic α pred
  | vOr : variadic α pred → List (variadic α pred) -> variadic α pred
  | vNot : variadic α pred -> variadic α pred


namespace variadic

mutual

def list_variadic_depth (l : List (variadic α pred)) : Nat :=
  match l with
    | [] => 0
    | v :: l => max (depth' v) (list_variadic_depth l)

def depth' (v : variadic α pred) : Nat :=
  match v with
    | vatom _ => 1
    | vAnd v l => (max (depth' v) (list_variadic_depth l)) + 1
    | vOr v l => (max (depth' v) (list_variadic_depth l)) + 1
    | vNot v => depth' v + 1

end

[Edward van de Meent]

let's see if i can get it to work with IList too...

[Jared green]

@Edward van de Meent see if it can be done with it as abbreviation, as suggested by henrik

[Edward van de Meent]

are you getting the kernel error too?

[Jared green]

yes

[Edward van de Meent]

ah wait i know what's going on. you can't fix that, because you can't mention predicates on your type in an argument for your inductive type

[Edward van de Meent]

i.e. this is an illegal constructor:

inductive T
 | foo (T -> Sort _) -> T

[Edward van de Meent]

i think your best bet would be either switching to the version with List or switching to an inductive definition of IList

[Jared green]

go with the inductive version

[Edward van de Meent]

import Init.Prelude
import Init.Coe
import Mathlib.Data.List.Basic

variable {α : Type}

inductive IList α
  where
  | single : α -> IList α
  | cons : α -> IList α -> IList α

inductive variadic (α :Type) (pred : α -> Prop)
  where
  | vatom : α -> (variadic α pred)
  | vAnd : IList (variadic α pred) -> variadic α pred
  | vOr : IList (variadic α pred) -> variadic α pred
  | vNot : variadic α pred -> variadic α pred

namespace variadic

mutual
def ilist_depth : ( IList (variadic α pred)) → Nat
  | .single v => variadic_depth v
  | .cons v l => max (variadic_depth v) (ilist_depth l)


def variadic_depth : variadic α pred → Nat
  | .vatom _ => 1
  | .vAnd l => ilist_depth l + 1
  | .vOr l => ilist_depth l + 1
  | .vNot v => variadic_depth v + 1

end

[Jared green]

how do i get the theorem that the depth of an ilist variadic is at least that of each element?

[Henrik Böving]

can you state the theorem

[Jared green]

import Init.Prelude
import Init.Coe
import Mathlib.Data.List.Basic

variable {α : Type}
inductive IList α
  where
  | single : α -> IList α
  | cons : α -> IList α -> IList α

def IList.fold  (l : IList α)  (f : α -> b -> b)  (g : α -> b) : b :=
  match l with
  | single a => g a
  | cons a as => f a (fold as f g)

def IList.map  (f : α -> b) : IList α -> IList b
  | single a => single (f a)
  | cons a as => cons (f a) (map f as)

def IList.toList : IList α -> {l : List α // l ≠ []}
  | single a => ⟨ [a], by simp⟩
  | cons a as => ⟨ (a :: (IList.toList as)),by simp⟩


--universe u
variable  {α : Type}[h : DecidableEq α]
inductive variadic (α :Type) [h : DecidableEq α]
(pred : α -> Prop)
  where
  | vatom : α -> (variadic α pred)
  | vAnd : IList (variadic α pred) -> variadic α pred
  | vOr : IList (variadic α pred) -> variadic α pred
  | vNot : variadic α pred -> variadic α pred
--deriving DecidableEq

namespace variadic

mutual
def ilist_depth : ( IList (variadic α pred)) → Nat
  | .single v => variadic_depth v
  | .cons v l => max (variadic_depth v) (ilist_depth l)

def variadic_depth : variadic α pred → Nat
  | .vatom _ => 1
  | .vAnd l => ilist_depth l + 1
  | .vOr l => ilist_depth l + 1
  | .vNot v => variadic_depth v + 1

end
theorem depth_le_elem : ∀ l : IList (variadic α pred), x ∈ l.toList.1, variadic_depth x  ≤ ilist_depth l :=
  by
  intro l x hx
  induction' l a a as hx
  unfold ilist_depth
  have h: x = a := by {
    unfold IList.toList at hx
    sorry
  }
  sorry

[Edward van de Meent]

the basic idea for such a proof is useing the inductive definition of l or x or both, since these functions are defined that way. in this case we only need induction on l:

theorem depth_le_elem : ∀ l : IList (variadic α pred), ∀ x ∈ l.toList.1,
    variadic_depth x ≤ ilist_depth l := by
  intro l
  induction l with
    | single a =>
      intro x
      dsimp [IList.toList,ilist_depth]
      simp only [List.mem_singleton]
      rintro rfl
      exact Nat.le_refl x.variadic_depth
    | cons a l hind =>
      intro x
      dsimp [IList.toList,ilist_depth]
      simp only [List.mem_cons]
      rintro (rfl|r)
      · exact Nat.le_max_left x.variadic_depth (ilist_depth l)
      · exact hind x r |>.trans  <| Nat.le_max_right a.variadic_depth (ilist_depth l)

[Edward van de Meent]

if you need induction over both variables/definitions, you will probably want to separate your theorem out in two just like the definitions, and prove them in a mutual block.

[Edward van de Meent]

not the case here, but if you run into these kinds of "how do i work with inductive definitions" issues

[Jared green]

all those exacts get a type mismatch.

[Edward van de Meent]

that's odd... let me take a look

[Edward van de Meent]

no issue for me... although you are missing a ∀ in the statement of the theorem...

[Edward van de Meent]

immediately after the first comma

[Jared green]

i copied what you gave me. on the first one, it says , has type x.variadic_depth ≤ x.variadic_depth, but is expected to have type x.variadic_depth ≤ ilist_depth (IList.single x)

[Edward van de Meent]

that's odd...
please do try to reproduce it in the lean playground, it works for me there.

[Edward van de Meent]

for the sake of completeness, this is what it should look like

Large Code Block

import Init.Prelude
import Init.Coe
import Mathlib.Data.List.Basic

variable {α : Type}
inductive IList α
  where
  | single : α -> IList α
  | cons : α -> IList α -> IList α

def IList.fold  (l : IList α)  (f : α -> b -> b)  (g : α -> b) : b :=
  match l with
  | single a => g a
  | cons a as => f a (fold as f g)

def IList.map  (f : α -> b) : IList α -> IList b
  | single a => single (f a)
  | cons a as => cons (f a) (map f as)

def IList.toList : IList α -> {l : List α // l ≠ []}
  | single a => ⟨ [a], by simp⟩
  | cons a as => ⟨ (a :: (IList.toList as)),by simp⟩


--universe u
variable  {α : Type}[h : DecidableEq α]
inductive variadic (α :Type) [h : DecidableEq α]
(pred : α -> Prop)
  where
  | vatom : α -> (variadic α pred)
  | vAnd : IList (variadic α pred) -> variadic α pred
  | vOr : IList (variadic α pred) -> variadic α pred
  | vNot : variadic α pred -> variadic α pred
--deriving DecidableEq

namespace variadic

mutual
def ilist_depth : ( IList (variadic α pred)) → Nat
  | .single v => variadic_depth v
  | .cons v l => max (variadic_depth v) (ilist_depth l)

def variadic_depth : variadic α pred → Nat
  | .vatom _ => 1
  | .vAnd l => ilist_depth l + 1
  | .vOr l => ilist_depth l + 1
  | .vNot v => variadic_depth v + 1

end
theorem depth_le_elem : ∀ l : IList (variadic α pred), ∀ x ∈ l.toList.1,
    variadic_depth x ≤ ilist_depth l := by
  intro l
  induction l with
    | single a =>
      intro x
      rw [IList.toList,ilist_depth]
      simp only [List.mem_singleton]
      rintro rfl
      exact Nat.le_refl x.variadic_depth
    | cons a l hind =>
      intro x
      rw [IList.toList,ilist_depth]
      simp only [List.mem_cons]
      rintro (rfl|r)
      · exact Nat.le_max_left x.variadic_depth (ilist_depth l)
      · exact hind x r |>.trans  <| Nat.le_max_right a.variadic_depth (ilist_depth l)

[Jared green]

yes, but it isnt working in my editor.

[Kevin Buzzard]

Then you may have an out of date mathlib

[Edward van de Meent]

from the error, it would seem that the dsimp [ilist_depth] isn't firing?

[Edward van de Meent]

because that should be reduced at that point...

[Edward van de Meent]

i don't think this is a mathlib version issue...

[Jared green]

@Kevin Buzzard odd, i updated it yesterday

[Edward van de Meent]

could you try replacing dsimp with rw in the single section of the induction?

[Kevin Buzzard]

Mathlib has updated to Lean 4.11.0-rc1 since yesterday.

[Jared green]

that works for both dsimps.

[Kevin Buzzard]

Indeed I can confirm that the code doesn't work with mathlib-from-a-few-days-ago but works fine with today's mathlib.

[Edward van de Meent]

huh

[Edward van de Meent]

how does that happen???

[Jared green]

im on rev # 1f03949ae423ae9fb010318e73f8969e44288c92

[Jared green]

lean v4.10.0

[Kevin Buzzard]

Indeed I can confirm that it doesn't work with that version for me. But it works with today's mathlib so there's no problem here :-)

[Edward van de Meent]

i'm curious what change caused/fixed this issue?

[Jared green]

how do i get DecidableEq for variadic? i need the proof as follows, but i dont know how to finish it.

def dec_eq_IList : DecidableEq α -> DecidableEq IList α :=
  by
  intro ha
  unfold DecidableEq
  intro a b
  have h : (a = b) <-> (a.toList.1 = b.toList.1) := by {
    sorry
  }
  rw [h]
  apply instDecidableEqList

[Edward van de Meent]

for IList, simply deriving DecidableEq seems to work...

[Jared green]

how does that look?

[Edward van de Meent]

inductive IList α
  where
  | single : α -> IList α
  | cons : α -> IList α -> IList α
deriving DecidableEq

[Jared green]

if i couldnt do that? (im updating now so i can)

[Edward van de Meent]

otherwise, you can simply pattern match on constructors and use if h : a = b then Decidable.isTrue (by simpa) else Decidable.isFalse (by simpa) when the constructors match, otherwise simply Decidable.isFalse (by simp)

[Edward van de Meent]

should do it

[Edward van de Meent]

out of curiosity, why is pred part of the signature of variadic while it doesn't seem to occur in the signature of constructors of variadic in any useful way?

[Jared green]

i dont know what you mean

[Jared green]

if you mean its on another line, that was so i could comment out the decidableeq

[Edward van de Meent]

i mean, why is it there at all? it doesn't get used?

[Jared green]

it does get used

[Edward van de Meent]

not in the constructors...

[Jared green]

in other functions i define elsewhere

[Edward van de Meent]

if it's not part of the signature of the constructors, surely there is no point in including it at all?

[Jared green]

i consider it necessary, as i have to be able to convert it to prop, because of certain properties i need to prove.

[Edward van de Meent]

allright then...

[Jared green]

so apparently deriving DecidableEq on IList didnt get decidableEq on variadic on its own.