Discussion, Braga method

Dear @joom,

I just left CPP'26 where I thought I would meet you in person but I understand it was problematic for you to travel there. I think we met earlier in the past when you asked me about some updates to the project

https://github.com/DmxLarchey/Kruskal-AlmostFull

so that the `opam` works on your Mac platform.

With Jean-Francçois Monin, I am the co-author of the Braga method that you might have heard of as well

https://github.com/DmxLarchey/The-Braga-Method

Using this method, below would be an alternate implementation of `unfold_tree` using a dependent version of `map` that seems shorter that what you have implemented.

```coq
Require Import List Utf8 Extraction.

Import ListNotations.

Set Implicit Arguments.

#[local] Notation "x ∈ l" := (In x l) (at level 70, no associativity, format "x ∈ l").

Definition dep_map X Y : ∀l : list X, (∀x, x ∈ l → Y) → list Y :=
fix loop l :=
match l with
| [] => λ _, []
| x::l => λ f, f x (in_eq _ _)
:: loop l (λ y h, f y (in_cons _ _ _ h))
end.

Inductive tree (X : Type) : Type :=
| node : X → list (tree X) → tree X.

Section unfold_tree.

Variables (A : Type) (next : A → list A).

Let R := λ a b, a ∈ next b.

Fixpoint unfold_tree_aux a (d : Acc R a) : tree A :=
node a (dep_map (next a) (λ b h, @unfold_tree_aux b (Acc_inv d h))).

Hypothesis wf : well_founded R.

Definition unfold_tree a := unfold_tree_aux (wf a).

End unfold_tree.

Recursive Extraction unfold_tree.
```

In the Braga method, you can moreover deal with partial algorithms and there is an implementation of DFS that might be related to your development as well.

Best regards and hopefully meet you soon,

Dominique

Start by comparing the repository's current unfold_tree implementation with the proposed dep_map-based version in the issue. Read the referenced Braga method and its DFS implementation to determine whether either approach fits this project. The issue does not define a specific change or acceptance criteria, so confirm the intended outcome before editing.

Written by the indexing model from the issue text.