I want to generate binary strings and reason about them!

Stream: new members

[Huỳnh Trần Khanh]

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?

[Huỳnh Trần Khanh]

As usual, thanks in advance!

[Bryan Gin-ge Chen]

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

[Huỳnh Trần Khanh]

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.

[Yakov Pechersky]

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

[Mario Carneiro]

does Lean have TCO?

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

[Mario Carneiro]

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

[Yakov Pechersky]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

[Mario Carneiro]

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]

[Huỳnh Trần Khanh]

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)

[Huỳnh Trần Khanh]

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.

[Mario Carneiro]

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

[Mario Carneiro]

it's a technique cribbed from haskell

[Mario Carneiro]

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

[Mario Carneiro]

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 []

[Mario Carneiro]

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

[Huỳnh Trần Khanh]

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.

[Sandy Maguire]

@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++

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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 β

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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)

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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 --;
}

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

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

[Sandy Maguire]

so in our mock C program:

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

[Sandy Maguire]

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

[Sandy Maguire]

happy to help dig through this furrther with you later

[Sandy Maguire]

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

[Mario Carneiro]

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).

[Mario Carneiro]

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.

[Mario Carneiro]

@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 $m^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))
}

[Mario Carneiro]

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

[Mario Carneiro]

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));
}

[Huỳnh Trần Khanh]

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

[Mario Carneiro]

which one?

[Huỳnh Trần Khanh]

In the selections_aux function

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

It feels a lot like solving cryptograms.

[Kevin Buzzard]

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.

[Huỳnh Trần Khanh]

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?

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

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

[Eric Wieser]

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

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

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

[Eric Wieser]

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.

[Huỳnh Trần Khanh]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Huỳnh Trần Khanh]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

to_binary also looks a little painful

[Mario Carneiro]

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

[Huỳnh Trần Khanh]

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.

[Huỳnh Trần Khanh]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Huỳnh Trần Khanh]

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

[Eric Wieser]

Whoops, my clipboard has been betraying me today

[Mario Carneiro]

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

[Mario Carneiro]

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

[Huỳnh Trần Khanh]

Lightning quick question: how do I use slim_check?

[Kevin Buzzard]

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

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

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.

[Bryan Gin-ge Chen]

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.

[Mario Carneiro]

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