Zulip Chat Archive

Stream: new members

Topic: I want to generate binary strings and reason about them!


view this post on Zulip Huỳnh Trần Khanh (Jan 17 2021 at 04:40):

A couple of questions:
1/ This is how I generate binary strings of length n.

import data.nat.basic
import data.list.range

open list

def strings :   list (list )
| 0 := [[]]
| (n + 1) := ((strings n).map (λ string, [string ++ [0], string ++ [1]])).join

#eval strings 3

But it takes forever for this code to generate strings of length 20 (and it happens to gobble up my RAM too, :sob:) even though this C++ can generate strings perfectly fine:

#include <bits/stdc++.h>
using namespace std;
int main()
{
    int n = 20;

    for (int mask = 0; mask < (1 << n); mask++)
    {
        for (int i = n - 1; i >= 0; i--)
            cout << (mask >> i & 1);
        cout << "\n";
    }
}

How can I optimize the Lean code?
2/ How do I generate binary strings of length n (again) that are lexicographically less than or equal to a certain binary string (also of length n)? Should I just kind of 'filter' the binary strings? Or are there more elegant approaches?

view this post on Zulip Huỳnh Trần Khanh (Jan 17 2021 at 04:41):

As usual, thanks in advance!

view this post on Zulip Bryan Gin-ge Chen (Jan 17 2021 at 04:44):

Is it important that they are actually strings? Mathlib has some code on bitvectors: https://leanprover-community.github.io/mathlib_docs/data/bitvec/core.html

view this post on Zulip Huỳnh Trần Khanh (Jan 17 2021 at 04:45):

Bryan Gin-ge Chen said:

Is it important that they are actually strings? Mathlib has some code on bitvectors: https://leanprover-community.github.io/mathlib_docs/data/bitvec/core.html

No, they can be bitvectors. I didn't know that mathlib has bitvectors.

view this post on Zulip Yakov Pechersky (Jan 17 2021 at 04:58):

First of all, your code isn't tail call optimized (does Lean have TCO?). Additionally, appending to the end of a list is O(N). If you're constructing the lists, either place in the front (using cons), or use a different data structure

view this post on Zulip Mario Carneiro (Jan 17 2021 at 05:01):

does Lean have TCO?

No, but it doesn't hurt to pretend that it did

view this post on Zulip Mario Carneiro (Jan 17 2021 at 05:03):

Regarding optimizing this, it depends on what you want to generate the strings for. It's probably a bad idea to construct a list of all exponentially-many strings lexicographically less than a given string, you want some more implicit representation that generates the strings on demand

view this post on Zulip Yakov Pechersky (Jan 17 2021 at 05:04):

A cheat to construct the lists would be some combination on list.range with nat.digits with a base of 2.

view this post on Zulip Mario Carneiro (Jan 17 2021 at 05:04):

That said, your strings function isn't bad if the point is to have a reference implementation that the efficient one is refining

view this post on Zulip Mario Carneiro (Jan 17 2021 at 05:06):

it's important to distinguish "program you can easily reason about" from "program that runs fast". Although lean programs can to some extent satisfy both criteria they pull in opposite directions and it's usually best to keep them separate

view this post on Zulip Mario Carneiro (Jan 17 2021 at 05:22):

For strings, assuming you want that exact type signature (which in particular implies that you have to construct the entire list of lists in memory before printing it, unlike the C++ version), I would suggest:

def selections_aux {α β} (l : list α) :   (list α  β)  list β  list β
| 0     f r := f [] :: r
| (n+1) f r := l.foldr (λ a, selections_aux n (f  list.cons a)) r

def selections {α} (n : ) (l : list α) : list (list α) :=
selections_aux l n id []

#eval selections 3 [ff, tt]

view this post on Zulip Mario Carneiro (Jan 17 2021 at 05:30):

and you can use that as the basis for a program to compute those less than a given binary string:

def below_aux :   list bool  (list bool  list bool)  list (list bool)
| 0 t f := []
| (n+1) [] f := [] -- impossible
| (n+1) (ff::t) f := below_aux n t (f  list.cons ff)
| (n+1) (tt::t) f :=
  selections_aux [ff, tt] n (f  list.cons ff) $
  below_aux n t (f  list.cons tt)

def below (l : list bool) : list (list bool) := below_aux l.length l id

#eval below [tt, tt, ff]

view this post on Zulip Huỳnh Trần Khanh (Jan 17 2021 at 09:36):

So this function composition trick is a way to append to a linked list in O(1) right? Or am I missing something?

def iota :   (list   list )
| 0 := id
| (n + 1) := iota n  list.cons (n + 1)

view this post on Zulip Huỳnh Trần Khanh (Jan 17 2021 at 09:41):

So it seems that in the (list ℕ → list ℕ) encoding, the identity function is the empty list and list.cons some_value is a list with one element.

view this post on Zulip Mario Carneiro (Jan 17 2021 at 09:42):

Indeed. In fact, we have a type for this encoding, called dlist

view this post on Zulip Mario Carneiro (Jan 17 2021 at 09:43):

it's a technique cribbed from haskell

view this post on Zulip Mario Carneiro (Jan 17 2021 at 09:44):

The version just above is a slightly more advanced version of the trick where we have built both mapping and appending into the recursive function

view this post on Zulip Mario Carneiro (Jan 17 2021 at 09:46):

The usual way you would prove theorems about that function is to prove that selections_aux n l f r = map f (selections_aux n l id []) ++ r, so that you only have to worry about the case where the last two parameters are id and []

view this post on Zulip Mario Carneiro (Jan 17 2021 at 09:47):

take a look at docs#list.sublists'_aux_eq_sublists' for example

view this post on Zulip Huỳnh Trần Khanh (Jan 17 2021 at 14:36):

After hours of poring over documentation I still couldn't understand how your code works. I have absolutely no functional programming experience. If you or someone else could explain both the selections and the below function I would really appreciate it.

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:25):

@Huỳnh Trần Khanh a nice property of purely functional programming languages like lean is that you can substitute a name for the thing it's defined as. sounds very reasonable if you are a mathematician, but this is crazy talk in C++

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:26):

eg if i have the C++ program int x = 0; int c = ++x, return c + c; i can't just inline the definition of c --- int x = 0; return ++x + ++x is a very differnet program

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:27):

my point being that a great way to understand functional programs is to just substitute definitions to get a feeling for how the execution of a program works

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:28):

when you don't have variable mutation (like in lean), a common trick is to define a new _aux function that takes the current-state of your variables as arguments

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:29):

that function is usually recursive, and by changing the arguments you call yourself with, you emulate statefully mutating your variables

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:30):

so selections above is the entry point, which calls selections_aux with the initial values of its arguments

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:31):

that is to say, selections is just a convenience function for calling selections_aux, so it suffices to understand the latter

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:31):

def selections_aux {α β} (l : list α) :   (list α  β)  list β  list β
| 0     f r := f [] :: r
| (n+1) f r := l.foldr (λ a, selections_aux n (f  list.cons a)) r

here we are pattern matching on the last three arguments of the function

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:32):

the | 0 f r := syntax denotes a pattern match, which is sorta like a C++ case statement on steroids

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:33):

since the type of the function is : ℕ → (list α → β) → list β → list β, that means there are three arguments of types:
1)
2) a function (list α → β) -- taking a list of alphas and returning a beta
3) list β

and then this function finally returns a list β

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:34):

with this in mind, we return to | 0 f r := ..., which does the ... ONLY when the argument is 0

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:35):

and it binds the (list α → β) parameter to the name f, likewise the list β to r

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:36):

after the := comes the return value. it needs to be of type list β

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:36):

f [] is a function call to f with an empty list, and :: puts an element at the begining of a list.

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:37):

so this expression inserts f [] at the beginning of r

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:37):

it's not immediately clear to me what's happening here, so let's look at the next pattern match

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:38):

patterns are tried from top to bottom, so | (n+1) f r : is tried only when the is NOT zero (otherwise the first case would have run already)

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:38):

it binds the same f and r parameters, but additionally now binds n to be one less than the argument

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:39):

(why? because it's saying that n + 1 is the argument that was passed, so n is one less than that)

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:39):

let's ignore the foldr bit for a second, and look at the recursive call. selections_aux n (f ∘ list.cons a)

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:40):

notice that we're calling selections_aux with n --- that is, one less than the argument we started with

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:41):

as such you can sort of reimagine the execution of this function as a while loop of the form

while (n > 0) {
  // do something
  n --;
}

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:42):

sorry to leave you hanging here, but i need to run

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:43):

one last thing to point out before i do is that not only is n getting smaller in this loop

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:43):

but also f is being expanded to (f ∘ list.cons a)

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:43):

so in our mock C program:

while (n > 0) {
  // do something
  f = f  list.cons a;
  n --;
}

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:45):

(this isn't exactly true due to the foldr, but it's a good mental approximation of the recursive transformation)

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:46):

happy to help dig through this furrther with you later

view this post on Zulip Sandy Maguire (Jan 17 2021 at 21:52):

you got thrown a doozy for your first glimpse at functional programming!

view this post on Zulip Mario Carneiro (Jan 18 2021 at 02:54):

Okay, so here's the idea behind selections. The goal, slightly generalized from your original statement of producing all binary strings of length n, is to produce a list of all lists of length n consisting of the elements of the input list. These are going to have the first element of the list varying the most slowly, and the last element of the list varies on each consecutive item. So for example:

selections [a,b,c] 2 = [[a, a], [a, b], [a, c], [b, a], [b, b], [b, c], [c, a], [c, b], [c, c]]

The key to computing this is to first figure out a recursive formula for doing so. The n=0 case is just [[]], that is, there is one string and it has length 0, and (n+1) long string is obtained by appending a to each element of the list, and concatenating it with adding b, and so on, like this:

selections [a,b,c] 2 =
  map (λ x, a::x) (selections [a,b,c] 1) ++
  map (λ x, b::x) (selections [a,b,c] 1) ++
  map (λ x, c::x) (selections [a,b,c] 1) ++ []

We can write this directly as a definition, it's a bit simpler than the one I gave:

def selections' {α} (l : list α) :   list (list α)
| 0     := [[]]
| (n+1) := list.join $ l.map (λ a, list.map (λ x, a::x) (selections' n))

#eval selections' [1,2,3] 2
-- [[1, 1], [1, 2], [1, 3], [2, 1], [2, 2], [2, 3], [3, 1], [3, 2], [3, 3]]

This version is also correct, and you can check that it has the same behavior as selections. Just to go over the recursive case here a bit, we can write the append of a bunch of lists l1 ++ l2 ++ l3 ++ [] as list.join [l1, l2, l3], and each list is like map (λ x, a::x) (selections [a,b,c] 1) that I mentioned before (The [a,b,c] part is omitted in lean because it's a parameter in the recursion).

view this post on Zulip Mario Carneiro (Jan 18 2021 at 03:11):

However, this method of producing lists is inefficient, because in each step of the recursion we are constructing a bunch of lists, mapping over them (which involves making a new copy of each list), and then appending them (which involves making a bunch of intermediate lists). So we're going to be allocating new lists many times before we're done. The key observation here is that each recursive call to selections is in a context of a map and an append, so if we had a function selections_aux l a f r that was defined as map f (selections l a) ++ r, then we could express the recursive case from before as:

selections [a,b,c] 2 =
  selections_aux [a,b,c] 1 (λ x, a::x) $
  selections_aux [a,b,c] 1 (λ x, b::x) $
  selections_aux [a,b,c] 1 (λ x, c::x) []

The neat thing about mapping and appending is that both of these are associative in the sense that a map of a map is a map and an append of an append is an append, so we can generalize this equation to if we also had to map more things:

map f (selections [a,b,c] 2) ++ r =
  map (λ x, f (a::x)) (selections [a,b,c] 1) ++
  map (λ x, f (b::x)) (selections [a,b,c] 1) ++
  map (λ x, f (c::x)) (selections [a,b,c] 1) ++ r

so that if we write this with selections_aux, we get

selections_aux [a,b,c] 2 f r =
  selections_aux [a,b,c] 1 (λ x, f (a::x)) $
  selections_aux [a,b,c] 1 (λ x, f (b::x)) $
  selections_aux [a,b,c] 1 (λ x, f (c::x)) r

which is a proper recursive equation for selections_aux.

Since we aren't appending lists directly anymore, we can't use list.join as before; we actually want to use list.foldr here, which does the operation

[a,b,c].foldr g r = g a (g b (g c r))

We have to provide a function g which will be applied with the arguments a, b, c in turn and the result from the remainder of the list, which is the same structure as above. So rewriting our example equation one more time we get

selections_aux [a,b,c] 2 f r = [a, b, c].foldr (λ y, selections_aux [a,b,c] 1 (λ x, f (y::x))) r

and now if we just generalize [a,b,c] and 1 in this equation we get the actual recursive equation for selections_aux.

The base case was previously selections 0 l = [[]], but now that we have to map and append, we need

  map f (selections 0 l) ++ r
= map f [[]] ++ r
= [f []] ++ r
= f [] :: r

so that's why the zero case is f [] :: r.

The result:

def selections_aux {α β} (l : list α) :   (list α  β)  list β  list β
| 0     f r := f [] :: r
| (n+1) f r := l.foldr (λ y, selections_aux n (λ x, f (y::x))) r

and we can rewrite the lambda into a composition for the original version.

view this post on Zulip Mario Carneiro (Jan 18 2021 at 03:28):

@Sandy Maguire, this function is really a recursive function, it's not a while loop in disguise because it calls itself recursively m times where m is the length of the input list (2 in the case of binary strings) in each recursive call. The recursion has depth exactly n, which is why you get mnm^n elements in the list in the end - the call tree a perfectly balanced m-way tree of depth n. If you were to render it in C++, you would still need a recursion. (There are ways to do it iteratively but that's a really different algorithm than the one here.) Here's a Rust version of the algorithm, with variables named analogously to the lean version:

fn selections_aux<T: Clone>(l: &[T], n: usize, f: Vec<T>, r: &mut Vec<Vec<T>>) {
  match n.checked_sub(1) {
    None => r.push(f),
    Some(n2) => for a in l {
      let mut f2 = f.clone();
      f2.push(a.clone());
      selections_aux(l, n2, f2, r);
    }
  }
}

fn selections<T: Clone>(l: &[T], n: usize) -> Vec<Vec<T>> {
  let mut r = vec![];
  selections_aux(l, n, vec![], &mut r);
  r
}

fn main() {
  println!("{:?}", selections(&[1, 2, 3], 2))
}

view this post on Zulip Mario Carneiro (Jan 18 2021 at 03:39):

(btw, you can use the button in the top left of the code snippet to test/edit this code)

view this post on Zulip Mario Carneiro (Jan 18 2021 at 04:48):

Just for fun, here's an iterative implementation with O(n) memory usage:

fn selections_foreach<T>(l: &[T], n: usize, mut f: impl FnMut(&[&T])) {
  if n == 0 { return f(&[]) }
  let mut it1 = l.iter();
  let first = if let Some(first) = it1.next() { first } else { return };
  let mut stack = vec![it1; n];
  let mut cur = vec![first; n];
  'next: loop {
    f(&cur);
    for (it, val) in stack.iter_mut().rev().zip(cur.iter_mut().rev()) {
      if let Some(a) = it.next() {
        *val = a;
        continue 'next
      } else {
        *it = l.iter();
        *val = it.next().unwrap();
      }
    }
    return
  }
}

fn main() {
  selections_foreach(&[1, 2, 3], 2, |c| println!("{:?}", c));
}

view this post on Zulip Huỳnh Trần Khanh (Jan 18 2021 at 14:37):

So the β type parameter represents both the list ℕ type and the type right?

view this post on Zulip Mario Carneiro (Jan 18 2021 at 14:39):

which one?

view this post on Zulip Huỳnh Trần Khanh (Jan 18 2021 at 14:40):

In the selections_aux function

view this post on Zulip Mario Carneiro (Jan 18 2021 at 14:41):

in selections_aux, the beta type parameter only needs to be list A in order to be useful for selections, but it can be generalized so why not

view this post on Zulip Mario Carneiro (Jan 18 2021 at 14:41):

since selections uses id for the function f that implies that list A = B

view this post on Zulip Mario Carneiro (Jan 18 2021 at 14:42):

and when using selections to produce a list of bools you need A = bool, or to make a list of nat you need A = nat

view this post on Zulip Huỳnh Trần Khanh (Jan 18 2021 at 16:05):

Thanks a lot! Now I understand how the selections function works. I substituted polymorphic stuff with concrete types and the foldr function with ordinary function composition and the selections function now makes total sense!

def selections_aux (alphabet : list ) :   (list   list )  (list (list )  list (list ))
| 0     current_string accumulated_list := current_string [] :: accumulated_list
| (n + 1) current_string accumulated_list :=
  (selections_aux n (current_string  list.cons 0)  selections_aux n (current_string  list.cons 1)) accumulated_list

view this post on Zulip Huỳnh Trần Khanh (Jan 18 2021 at 16:06):

It feels a lot like solving cryptograms.

view this post on Zulip Kevin Buzzard (Jan 18 2021 at 17:28):

Going the other way (finding the general thing which can apply in more than one situation) is called abstraction, and it seems to be a common feature of both maths and computer science. Spotting underlying patterns is something mathematicians can get excited about.

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

Tomorrow I will implement the "digit dynamic programming" algorithm in Lean. But I want to make sure that my definitions are alright first.

def strings (n : ) := (range n).map (nat.to_digits 2)
def popcount (string : list ) := string.foldl (λ accumulated, λ digit, accumulated + digit) 0
def total_popcount (n : ) := (strings n).foldl (λ accumulated, λ current_string, accumulated + popcount current_string) 0

Are the definitions alright? Any suggestions?

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

The total_popcount function computes the number of 1 digits in the binary representations of numbers from 0 to n - 1.

view this post on Zulip Huỳnh Trần Khanh (Jan 19 2021 at 16:01):

So again, here is the code I'm going to port to Lean.

view this post on Zulip Eric Wieser (Jan 19 2021 at 16:21):

Not relevant to your porting, but λ accumulated, λ digit, _ is long for λ accumulated digit, _, and (λ accumulated, λ digit, accumulated + digit) is long for (+).

view this post on Zulip Huỳnh Trần Khanh (Jan 20 2021 at 09:04):

Alright, ported! Now how do I prove that the dp function is equivalent to the total_popcount function?

import data.nat.basic
import data.list.range
open list

def strings (n : ) := (range n).map (nat.to_digits 2)
def popcount (string : list ) := string.foldl (+) 0
def total_popcount (n : ) := (strings n).foldl (λ accumulated current_string, accumulated + popcount current_string) 0

def dp_cardinality : list bool  bool  
| [] tt := 1
| [] ff := 0
| (ff::the_rest) ff := dp_cardinality the_rest ff
| (tt::the_rest) ff := dp_cardinality the_rest tt + dp_cardinality the_rest ff
| (_::the_rest) tt := 2 * dp_cardinality the_rest tt

def dp_popcount : list bool  bool  
| [] _ := 0
| (ff::the_rest) ff := dp_popcount the_rest ff
| (tt::the_rest) ff := dp_popcount the_rest tt + (dp_popcount the_rest ff + dp_cardinality the_rest ff)
| (_::the_rest) tt := dp_popcount the_rest tt + (dp_popcount the_rest tt + dp_cardinality the_rest tt)

def to_bool (n : ) := list.reverse ((nat.to_digits 2 n).map (λ x, if x = 0 then ff else tt))

def dp (n : ) := dp_popcount (to_bool n) ff

view this post on Zulip Huỳnh Trần Khanh (Jan 20 2021 at 09:05):

Memoizing the parameters would yield an algorithm that runs in logarithmic time!

view this post on Zulip Eric Wieser (Jan 20 2021 at 09:10):

Another tip: your popcount is just string.sum, which will make the proof marginally easier. It's tempting in fact to just define total_popcount as (((range n).map $ nat.to_digits 2).map list.sum).sum, which eliminates the other two definitions.

view this post on Zulip Huỳnh Trần Khanh (Jan 20 2021 at 14:34):

I am genuinely stuck. I have never proved something like this before. Can anyone please help me out, thanks in advance. I guess there would be some sort of plumbing to convert between different representations right?

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 14:35):

Why don't you start by formalising your question and adding it to the MWE above? People like explicit sorryed proofs.

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 14:36):

Also, why not sketch a (non-Lean) proof of what you want to do?

view this post on Zulip Huỳnh Trần Khanh (Jan 20 2021 at 14:38):

Alright so here is the MWE with an explicit sorry'd proof.

import data.nat.basic
import data.list.range
open list

def popcount (n : ) := (((range n).map $ nat.to_digits 2).map list.sum).sum

def dp_cardinality : list bool  bool  
| [] tt := 1
| [] ff := 0
| (ff::the_rest) ff := dp_cardinality the_rest ff
| (tt::the_rest) ff := dp_cardinality the_rest tt + dp_cardinality the_rest ff
| (_::the_rest) tt := 2 * dp_cardinality the_rest tt

def dp_popcount : list bool  bool  
| [] _ := 0
| (ff::the_rest) ff := dp_popcount the_rest ff
| (tt::the_rest) ff := dp_popcount the_rest tt + (dp_popcount the_rest ff + dp_cardinality the_rest ff)
| (_::the_rest) tt := dp_popcount the_rest tt + (dp_popcount the_rest tt + dp_cardinality the_rest tt)

def to_binary (n : ) := list.reverse ((nat.to_digits 2 n).map (λ x, if x = 0 then ff else tt))

def dp (n : ) := dp_popcount (to_binary n) ff

lemma equivalent (n : ) : dp n = popcount n := begin
  sorry,
end

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 14:40):

slim_check can't find any counterexamples so that's a good start :D

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 14:41):

So what's the proof sketch you have in mind? Lean won't do anything automatically, it needs to be guided.

view this post on Zulip Mario Carneiro (Jan 20 2021 at 14:41):

Why did you use (range n).map (nat.to_digits 2) instead of selections? You're going to need a bunch of theorems about digits that don't really matter here

view this post on Zulip Mario Carneiro (Jan 20 2021 at 14:42):

to_binary also looks a little painful

view this post on Zulip Mario Carneiro (Jan 20 2021 at 15:12):

Here are some lemmas that should help you along the way:

def eval_binary : list bool  
| [] := 0
| (ff :: l) := 2 * eval_binary l
| (tt :: l) := 2 * eval_binary l + 1

lemma dp_cardinality_tt :  l, dp_cardinality l tt = 2 ^ length l := sorry
lemma dp_cardinality_ff :  l, dp_cardinality l ff = eval_binary l.reverse := sorry

lemma dp_popcount_tt :  l : list bool, let n := length l in
  dp_popcount l tt = n * 2 ^ (n - 1) := sorry

lemma eval_binary_to_binary :  n, eval_binary (to_binary n).reverse = n := sorry

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

The algorithm that is being implemented is called "digit DP". The "digit DP" algorithm tries to construct every possible string that satisfies a given condition, for example in this case lexicographically less than the binary representation of n.

The first parameter of the two dp functions represents the current digit that is being probed. It's somewhat similar to the selections function: the first digit is probed first, then the second, then the third, then the nth. And the second parameter indicates whether or not the current number is already less than n. If every number with the already probed digits is less than n then the digits that are yet to be probed can be anything, otherwise the next digit must be <= the corresponding digit of the number n.

The dp_cardinality function counts numbers that start with the already probed digits and are less than n. The dp_popcount function counts the number of set bits.

Let me dissect the two functions.

def dp_cardinality : list bool  bool  
-- No more digits to probe. The final number is less than `n` so there is exactly 1 number that can be formed.
| [] tt := 1
-- No more digits to probe. The final number is >= `n`. No number can be formed.
| [] ff := 0
-- If the corresponding digit of `n` is zero, the only possible value for the current digit is 0. Not every number with the already probed digits is less than `n`, therefore the second parameter is ff.
| (ff::the_rest) ff := dp_cardinality the_rest ff
-- The corresponding digit of `n` is one. The current digit can be either 0 or 1. If the current digit is 0 then every number with the already probed digits is less than `n`, therefore the second parameter is tt. Otherwise, the second parameter is ff.
| (tt::the_rest) ff := dp_cardinality the_rest tt + dp_cardinality the_rest ff
-- The second parameter indicates that the rest of the number can be anything and the number is still less than `n`.
| (_::the_rest) tt := 2 * dp_cardinality the_rest tt
def dp_popcount : list bool  bool  
-- No more digits, 1 number can be formed.
| [] _ := 0

-- The current digit is 0.
| (ff::the_rest) ff := dp_popcount the_rest ff

-- The current digit can either be 0 or 1. When the current digit is 1, the total number of set bits increases by the # of numbers with the already probed digits that are less than `n`.
| (tt::the_rest) ff := dp_popcount the_rest tt + (dp_popcount the_rest ff + dp_cardinality the_rest ff)
| (_::the_rest) tt := dp_popcount the_rest tt + (dp_popcount the_rest tt + dp_cardinality the_rest tt)

As I don't have a math background, I don't really have a proof sketch. But I think the description of the algorithm somewhat serves as a justification for its correctness.

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

Apologies if the explanation is confusing, I am not really good with words.

view this post on Zulip Mario Carneiro (Jan 20 2021 at 15:21):

The dp_cardinality function counts numbers that start with the already probed digits and are less than n. The dp_popcount function counts the number of set bits.

Those sound like excellent lemmas

view this post on Zulip Eric Wieser (Jan 20 2021 at 15:30):

I had a very quick attempt by just throwing simp at the problem, and found a missing lemma about range, which I've PR'd as #5821

view this post on Zulip Huỳnh Trần Khanh (Jan 20 2021 at 16:07):

@Eric Wieser You mean https://github.com/leanprover-community/mathlib/pull/5821 right?

view this post on Zulip Eric Wieser (Jan 20 2021 at 16:08):

Whoops, my clipboard has been betraying me today

view this post on Zulip Mario Carneiro (Jan 20 2021 at 16:24):

Here's a more directed proof sketch:

theorem range_add (a b) : range (a + b) = range a ++ map (λ n, a + n) (range b) := sorry

def set_bits (n : ) :  := (nat.digits 2 n).sum

theorem set_bits_succ (n k : ) (h : n < 2 ^ k) : set_bits (2 ^ k + n) = set_bits n + 1 := sorry

def eval_binary : list bool  
| [] := 0
| (ff :: l) := 2 * eval_binary l
| (tt :: l) := 2 * eval_binary l + 1

lemma eval_binary_to_binary :  n, eval_binary (to_binary n).reverse = n := sorry
theorem eval_binary_lt :  l, eval_binary l < 2 ^ l.length := sorry

def eval_binary' : list bool  
| [] := 0
| (ff :: l) := 2 * eval_binary l
| (tt :: l) := 2 ^ l.length + 2 * eval_binary l

theorem eval_binary_rev :  l, eval_binary (reverse l) = eval_binary' l := sorry
theorem eval_binary_rev_lt :  l, eval_binary' l < 2 ^ l.length := sorry
lemma eval_binary'_to_binary :  n, eval_binary' (to_binary n) = n := sorry

def range_binary : list bool  bool  list 
| [] tt := [0]
| [] ff := []
| (ff::l) ff := range_binary l ff
| (tt::l) ff := range_binary l tt ++ map (λ n, 2 ^ length l + n) (range_binary l ff)
| (_::l) tt := range_binary l tt ++ map (λ n, 2 ^ length l + n) (range_binary l tt)

theorem range_binary_range_tt :  l,
  range_binary l tt = range (2 ^ l.length) := sorry
theorem range_binary_range_ff :  l,
  range_binary l ff = range (eval_binary' l) := sorry
theorem range_binary_length :  l b,
  (range_binary l b).length = dp_cardinality l b := sorry
theorem range_binary_set_bits :  l b,
  ((range_binary l b).map set_bits).sum = dp_popcount l b := sorry

lemma equivalent (n : ) : dp n = popcount n :=
by rw [dp,  range_binary_set_bits, popcount, map_map,
    range_binary_range_ff, eval_binary'_to_binary]; refl

view this post on Zulip Mario Carneiro (Jan 20 2021 at 16:33):

also you should be using nat.digits (from data.nat.digits) instead of nat.to_digits. It's basically the same thing but it has a lot more lemmas

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2021 at 09:42):

Lightning quick question: how do I use slim_check?

view this post on Zulip Kevin Buzzard (Jan 21 2021 at 09:43):

Is import tactic.slim_check the answer you're looking for?

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2021 at 09:43):

So deterministic timeout means that slim_check fails to find a counterexample right?

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2021 at 09:45):

Thanks for the quick response, @Kevin Buzzard :raised_hands:

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2021 at 16:05):

How would you prove this?

def coerce_bool (digits : list ) := list.reverse (digits.map (λ x, if x = 0 then ff else tt))
def coerce_digits (string : list bool) := list.reverse (string.map (λ x, if x then 1 else 0))

lemma is_identity { string : list  } { h :  x  string, x < 2 } : coerce_digits (coerce_bool string) = string := begin
  sorry,
end

It is equivalent to the eval_binary'_to_binary lemma in the Lean proof sketch.

view this post on Zulip Bryan Gin-ge Chen (Jan 21 2021 at 16:08):

Huỳnh Trần Khanh said:

So deterministic timeout means that slim_check fails to find a counterexample right?

I think slim_check will tell you explicitly if it fails to find a counterexample after a certain number of tries; a deterministic timeout might mean that something else is failing before slim_check is able to run (e.g. slim_check does a search for a testable instance and this could time out). The documentation and some examples can be found here; you can try those out to see what the normal behavior is.

view this post on Zulip Mario Carneiro (Jan 21 2021 at 16:25):

import data.list.basic

def coerce_bool (digits : list ) := list.reverse (digits.map (λ x, if x = 0 then ff else tt))
def coerce_digits (string : list bool) := list.reverse (string.map (λ x, if x then 1 else 0))

lemma is_identity {l : list } (H :  x  l, x < 2) : coerce_digits (coerce_bool l) = l :=
begin
  rw [coerce_digits, coerce_bool, list.map_reverse,
    list.reverse_reverse, list.map_map, list.map_congr, list.map_id],
  intros x h,
  replace h := H x h,
  revert x h, dec_trivial
end

Last updated: May 11 2021 at 00:31 UTC