# Zulip Chat Archive

## Stream: lean4

### Topic: interweave proof and code

#### Huỳnh Trần Khanh (Jan 22 2021 at 15:21):

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 (Jan 22 2021 at 15:23):

dp is short for dynamic programming by the way

#### Yakov Pechersky (Jan 22 2021 at 15:34):

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 (Jan 22 2021 at 15:36):

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 (Jan 22 2021 at 15:39):

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

Last updated: May 07 2021 at 13:21 UTC