interweave proof and code

Stream: lean4

[Huỳnh Trần Khanh]

is there a way in lean 4 to write proof and code together? I am trying to prove the correctness of a digit DP algorithm and so far in my Lean 3 code the algorithm part and the proof part are somewhat separated, somewhat disconnected

most dp algorithms can be proven correct using a simple induction argument, and i feel that integrating the proof and the algorithm together is more in line with the spirit of dp (dp is recursion, and induction is also recursion-ish?)

let's consider the TSP problem for example, let dp(vertex, visited_vertices) be the min cost of visiting every vertex from vertex then:
base case: if every vertex is visited then the cost is 0
induction: the min cost equals something like this

int result = inf;
for (int adjacent = 0; adjacent < n; adjacent++)
  if (!(visited_vertices >> adjacent & 1))
    result = min(result, cost[vertex][adjacent] + dp(adjacent, visited_vertices | (1 << adjacent)));

as you can see the algorithm kind of justifies itself but in lean you have to write a separate induction proof that quite frankly looks a lot like the original algorithm

[Huỳnh Trần Khanh]

dp is short for dynamic programming by the way

[Yakov Pechersky]

When you say "kind of justifies" itself, it's exactly turning the "kind of" into truly, which is the building of the proof term.

[Yakov Pechersky]

You could write meta code that is able to introspect the definition to help in the mechanical conversion of the definition into a proof term.

[Eric Wieser]

You can define your function to return the subtype {x : T // property_you_care_about x}