Zulip Chat Archive

Stream: lean4

Topic: interweave proof and code


view this post on Zulip 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

view this post on Zulip Huỳnh Trần Khanh (Jan 22 2021 at 15:23):

dp is short for dynamic programming by the way

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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