Enforce wellfoundedness in type definition

Stream: new members

[nrs]

I have the following inductive type:

inductive Tree (a : Type) : Type where
  | node : (val: a) -> List (Tree a) -> Tree a

I would like it to be wellfounded with respect to the following relation: (Tree.list returns the List (Tree a) used in the node constructor )

def isImmediateSubtree (a b : Tree α) : Prop := a ∈ b.list

I know neither Tree nor isImmediateSubtree as defined above are wellfounded, so I would like to define another type

class wfTree (α : Type) where
  tree : Tree α
  wf : ?

that would enforce wellfoundedness of that relation wrt. wfTrees. Would anyone have suggestions of how I could go about this?

[Mario Carneiro]

It is already well founded wrt that relation

[nrs]

Mario Carneiro said:

It is already well founded wrt that relation

oh, so I would only need to write wf : WellFounded isImmediateSubtree?

[Mario Carneiro]

no, I mean you can prove it, you don't need to enforce anything

[nrs]

Mario Carneiro said:

no, I mean you can prove it, you don't need to enforce anything

in the constructor node, don't we have that nothing prevents List (Tree a) as defined above from growing indefinitely?

[Mario Carneiro]

Lists are finite by definition

[Mario Carneiro]

and nested inductive types are built inductively, meaning that they only contain smaller things

[Mario Carneiro]

this is basically well founded by the definition of what an inductive type is

[Mario Carneiro]

in fact well foundedness itself is defined using inductive types, which are the primitive concept in lean's type theory

[nrs]

Mario Carneiro said:

in fact well foundedness itself is defined using inductive types, which are the primitive concept in lean's type theory

oh, so any attempt to define a non-wellfounded Tree value will fail by virtue of needing to provide a termination proof for defining the value right?

[Mario Carneiro]

theorem wf : WellFounded (@isImmediateSubtree α) := ⟨acc⟩ where
  acc : (t : Tree α) → Acc isImmediateSubtree t
  | .node .. => .intro _ (accList _)
  accList : (l : List (Tree α)) → ∀ a ∈ l, Acc isImmediateSubtree a
  | _ :: _, _, .head _ => acc _
  | _ :: _, _, .tail _ h => accList _ _ h

[Mario Carneiro]

No there are no termination proofs needed to define a value of the type, but you can only build values by applying the constructor to values you built previously, so you will never get infinitely large things that way

[nrs]

Mario Carneiro said:

No there are no termination proofs needed to define a value of the type, but you can only build values by applying the constructor to values you built previously, so you will never get infinitely large things that way

ah I see! thank you very much for taking the time, things are way clearer to me now, ty!

[nrs]

Mario Carneiro said:

Lists are finite by definition

right, but a subsequent Tree

Mario Carneiro said:

theorem wf : WellFounded (@isImmediateSubtree α) := ⟨acc⟩ where
  acc : (t : Tree α) → Acc isImmediateSubtree t
  | .node .. => .intro _ (accList _)
  accList : (l : List (Tree α)) → ∀ a ∈ l, Acc isImmediateSubtree a
  | _ :: _, _, .head _ => acc _
  | _ :: _, _, .tail _ h => accList _ _ h

I have been studying this theorem for a while, I have a question for you if you have time (no worries otherwise, already very much appreciate the answer!): what exactly is being passed to acc here? I'm a bit confused by the fact that defining the function acc with pattern matching typechecks while using := doesn't

[nrs]

for anyone else who might be interested, the following makes it a bit clearer. Mario Carneiro is having Lean infer the correct thing to place there

  | .node .. => by
    apply Acc.intro
    intros
    rename_i a b c d
    apply accList
    exact d

@Mario Carneiro would still very much be interested in understanding how you managed to reason your way into that representation, it is very elegant!

[Mario Carneiro]

here it is with the implicit arguments filled in:

theorem wf : WellFounded (@isImmediateSubtree α) := ⟨acc⟩ where
  acc : (t : Tree α) → Acc isImmediateSubtree t
  | .node a l => .intro (.node a l) (accList l)
  accList : (l : List (Tree α)) → ∀ a ∈ l, Acc isImmediateSubtree a
  | a :: _, _, .head _ => acc a
  | _ :: l, b, .tail _ h => accList l b h

[Mario Carneiro]

because the types are so constraining here, lean can figure all these out by itself

[Mario Carneiro]

nrs said:

what exactly is being passed to acc here?

There are two calls to acc in this proof. In the first one (on the first line), it's not being applied at all, the whole function applying it to every argument is passed to produce a proof of well-foundedness. In the second one, it is applied to a, which is the subtree which we selected using the a \in l hypothesis.

Stepping back a bit and giving an explanation for the proof in words: we need to show that every element is "accessible" by the isImmediateSubtree relation, where Acc isImmediateSubtree t holds if Acc isImmediateSubtree a holds for every a \in t.list. We prove this by induction on t, mutually with another theorem that talks about a l : List (Tree a) and says that every element of l is Acc isImmediateSubtree. (We should expect this proof to proceed by mutual induction because a nested inductive type is basically a mutual inductive where the types being defined are all the types appearing in the constructors involving the type being defined, here Tree α and List (Tree α).)

In the tree case, we can apply the definition of Acc to reduce to showing that ∀ a ∈ l, Acc isImmediateSubtree a, which is the other (list) inductive hypothesis.

In the list case, we can match on the list, which is nonempty because we've assumed it has a member a, and the element a is either at the head in which case we apply the node IH, or it's in the tail which is the list IH.

[nrs]

Mario Carneiro said:

nrs said:

what exactly is being passed to acc here?

There are two calls to acc in this proof. In the first one (on the first line), it's not being applied at all, the whole function applying it to every argument is passed to produce a proof of well-foundedness. In the second one, it is applied to a, which is the subtree which we selected using the a \in l hypothesis.

Stepping back a bit and giving an explanation for the proof in words: we need to show that every element is "accessible" by the isImmediateSubtree relation, where Acc isImmediateSubtree t holds if Acc isImmediateSubtree a holds for every a \in t.list. We prove this by induction on t, mutually with another theorem that talks about a l : List (Tree a) and says that every element of l is Acc isImmediateSubtree. (We should expect this proof to proceed by mutual induction because a nested inductive type is basically a mutual inductive where the types being defined are all the types appearing in the constructors involving the type being defined, here Tree α and List (Tree α).)

In the tree case, we can apply the definition of Acc to reduce to showing that ∀ a ∈ l, Acc isImmediateSubtree a, which is the other (list) inductive hypothesis.

In the list case, we can match on the list, which is nonempty because we've assumed it has a member a, and the element a is either at the head in which case we apply the node IH, or it's in the tail which is the list IH.

Thank you very much for the answer, it is very clear to me now!! Highly appreciate the time you've taken to answer this!!