Formalizing a proof in Lean, not sure how

Stream: new members

[Chris M]

I have an informal proof and I'm curious how to formalize it in Lean. I'll strip away the details: Broadly the algorithm goes like this:

We have a tree (i.e. a DAG) G, where each node N has some data associated to it in the form of a function D:G.Nodes\to DataType1. We are also given a function F that takes a tree with data(G,D), and outputs another tree (G,D')where D' differs from D on the root node of the tree and its child nodes. We want to use F to recursively adjust the data in the tree.

I have an algorithm H, which recursively applies F, but it recurses "forwards" on the graph. This is pseudocode:

def H (G,D) := --informal definition
  for each child node c of the root node of G,
    Let (G_c, D_c) be the subgraph of G starting with c
    Let (G_x, D'_c) be the result of H applied to (G_c, D_c)
  Let (G,\tilde D') be the result of replacing the subgraphs (G_c, D_c) in (G, D) with (G_c, D'_c) for each c,
  Let H(G,D) = (G,D') be the result of applying F to (G,\tilde D')

Intuitively, the algorithm first moves all the way to the leaves of the tree, applies F there, and then recurses backwards. We know that the graph is finite.

Here is what I don't know how to formalize: I want to use this algorithm in an existence proof (H shows that for any pair (G,D) there exists a pair (G,D') with certain properties that I won't go into), but this definition uses a form of recursion that is different from well-founded recursion e.g. on the natural numbers. In fact it seems to me like I can't even define H in lean without the meta keyword because it is not using well-founded recursion. Intuitively I can just say "H keeps calling a graph that is smaller than the original, and the size of graphs is bounded above 0, so it is well-defined", but I'm not sure how to formalize this.

I can think of two solutions:

1. Drop the idea of actually defining H, and just prove the result by mathematical induction on the depth of the graph. I'd prefer not to do this since I want to have H as a computational object.
2. Define a function H_n which takes a graph of depth n (or maximal depth n) and only have H_{n+1} call H_n or H_k with k\leq n. Then define H in terms of H_n where n is the size of the input graph. But this seems ugly to me. I'd rather just define H directly for reasons of simplicity and clarity.

[Eric Wieser]

If you can express your recursion using a match statement, then you can always provide a using_well_founded definition explicitly - there are some recent discussions about this elsewhere on zulip

[Reid Barton]

It sounds like you just do structural recursion on trees though.

[Reid Barton]

I guess it might not be so simple depending on the representation of trees

[Eric Wieser]

Does the type of this declaration faithfully represent your problem?

inductive graph
| mk : list (graph) → graph

def H {α β : Type*} (G : graph) (D : graph → α) (F : graph → (graph → α) → (graph → β)) : graph → β := sorry

[Chris M]

Let me just copy it and put line breaks in:

inductive graph
| mk : list (graph) → graph

def H {α β : Type*} (G : graph) (D : graph → α)
(F : graph → (graph → α) → (graph → β))
: graph → β
:= sorry

[Chris M]

I have to think about it, but I have to leave now. I'll look at this again soon.

[Eric Wieser]

Actually it looks like alpha and beta have to be the same

[Eric Wieser]

To be clear, is this a DAG or a tree? I don't think your operation makes sense on a general DAG.

[Alistair Tucker]

This is how I have interpreted it:

mutual inductive tree, list_tree (α : Type)
with tree : Type
| node : α → list_tree → tree
with list_tree : Type
| nil {} : list_tree
| cons    : tree → list_tree → list_tree

def F {α β : Type} : α → list_tree β → β := sorry

mutual def H, H_tilde {α β : Type}
with H : tree α → tree β
| (tree.node a l) := tree.node (F a (H_tilde l)) (H_tilde l)
with H_tilde : list_tree α → list_tree β
| list_tree.nil := list_tree.nil
| (list_tree.cons t ts) := list_tree.cons (H t) (H_tilde ts)

But I'm sure there's some much neater way to express it using the equation compiler and (as Eric Wieser suggests)

inductive tree (α : Type)
| mk : α → list tree → tree

I think the authoritative source on this stuff is TPIL chapters 7 and 8.

[Alistair Tucker]

@Chris M This seems to work too (at least it typechecks!) and perhaps it's closer to what you asked for.

inductive tree {α : Type} (β : α → Type)
| mk (a : α) (φ : β a → tree) : tree

variables {α : Type} {β : α → Type} {δ δ' : Type}

inductive node : tree β → Type
| root {G : tree β} : node G
| child {a : α} {φ : β a → tree β} (c : β a) (n : node (φ c)) : node ⟨a, φ⟩

def f : Π {a : α} {φ : β a → tree β} (D' : Π c, node (φ c) → δ'), δ → δ' :=
sorry

def F {a : α} {φ : β a → tree β} (D' : Π c, node (φ c) → δ') (d : δ) : node ⟨a, φ⟩ → δ'
| (node.root) := f D' d
| (node.child c n) := D' c n

def H : Π (G : tree β) (D : node G → δ), node G → δ'
| ⟨a, φ⟩ D := F (λ c, H (φ c) (λ n, D (node.child c n))) (D node.root)