## 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;
if (!(visited_vertices >> adjacent & 1))


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