Tree notation

Stream: general

[Yaël Dillies]

Is there notation for docs#tree? If not, what could one be?

[Yaël Dillies]

The context is #10645 where we're gonna use a tactic to generate a (huge) certificate tree, then cache it by putting it in the code.

[Yaël Dillies]

roth? will output Try this: roth <insert big tree here> and roth t where t is a tree will apply a custom tactic for nodes and another one for leaves.

[Yaël Dillies]

So I'm actually only interested in tree unit, with specific notation if possible because I don't want to have to write () in every node.

[Yaël Dillies]

Of course, we can always flatten tree α to list (option α) (or maybe in our case to list bool. I'm open to suggestions. I just want something usable.

[Mario Carneiro]

Do you care if the tree is "readable"? You could output some compressed representation as a string and parse it in the tactic

[Yaël Dillies]

No, I don't care about readability at all, and it's meant to be processed by a tactic anyway so an additional parsing shouldn't. However, the length of the said string could be of the order of 1000 characters, so they can't hold on a line. Is "stuff" ++ "other stuff" an acceptable way to circumvent the problem?

[Yaël Dillies]

Do you think we could go as far as outputting one big number?

[Eric Wieser]

Why is that better than a string?

[Eric Wieser]

Can you wrap numbers in lean?

[Yaël Dillies]

It's better than a string of t and f, but it's worse than a string of literally any allowable character.

[Reid Barton]

base64 encoding would be the common way to encode a blob of bits in a text file.

[Yaël Dillies]

SHould I write such a parser from scratch and dedicated to tree or should I set up an API for turning a repr into a base64 string?

[Kyle Miller]

@Yaël Dillies I had a go at this:

tree <-> string

import tactic
import data.tree
import data.nat.digits
import tactic.slim_check

--def base64_chars : string :=
--"ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"

def base64_to_char (n : ℕ) (h : n < 64) : char :=
if h1 : n < 26 then char.of_nat (n + 65)
else if h2 : n < 52 then char.of_nat (n + 71)
else if h3 : n < 62 then char.of_nat (n - 4)
else if h4 : n = 62 then '+'
else if h5 : n = 63 then '/'
else by { exfalso, simp at h3, interval_cases n; trivial, }

def base64_to_char' (n : ℕ) : char :=
if h : n < 64 then base64_to_char n h else 'A'

def base64_of_char (c : char) : option ℕ :=
let n := char.to_nat c in
if 65 <= n ∧ n < 91 then some (n - 65)
else if 97 <= n ∧ n < 123 then some (n - 71)
else if 48 <= n ∧ n < 58 then some (n + 4)
else if c = '+' then some 62
else if c = '/' then some 63
else none

--example (n : ℕ) (h : n < 64) : base64_of_char (base64_to_char n h) = n := by dec_trivial!

def to_bool_list_aux : tree unit → list bool → list bool
| tree.nil acc := ff :: acc
| (tree.node _ l r) acc := to_bool_list_aux l (to_bool_list_aux r (tt :: acc))

def to_bool_list (t : tree unit) : list bool := to_bool_list_aux t []

def of_bool_list_aux : list bool → list (tree unit) → option (tree unit)
| [] [] := none
| [] (t :: _) := some t
| (ff :: xs) stack := of_bool_list_aux xs (tree.nil :: stack)
| (tt :: xs) [] := none
| (tt :: xs) [_] := none
| (tt :: xs) (r :: l :: stack) := of_bool_list_aux xs (tree.node () l r :: stack)

def of_bool_list (xs : list bool) : option (tree unit) := of_bool_list_aux xs []

def string_of_bool_list (xs : list bool) : string :=
list.as_string $
(xs.reverse.to_chunks 6).map (λ (c : list bool),
  base64_to_char' (nat.of_digits 2 (c.map (λ b, cond b 1 0))))

/-- round tripping, list ends up padded with a `ff` prefix to have multiple-of-six length -/
def bool_list_of_string (s : string) : list bool := list.reverse $ do
  c ← s.to_list,
  n ← (base64_of_char c).to_list,
  let digs := nat.to_digits 2 n,
  d ← (digs ++ list.repeat 0 (6 - digs.length)),
  pure $ d ≠ 0

def string_of_tree (t : tree unit) : string :=
string_of_bool_list $ to_bool_list t

def tree_of_string (s : string) : option (tree unit) :=
of_bool_list $ bool_list_of_string s

abbreviation N : tree unit := tree.nil
abbreviation T : tree unit → tree unit → tree unit := tree.node ()

def t := (T (T N (T (T N N) N)) (T N (T N (T (T N N) N))))

#eval (of_bool_list (to_bool_list t) = t : bool)
-- tt
#eval (tree_of_string (string_of_tree t) = t : bool)
-- tt
#eval string_of_tree t
-- "vwC"

def t' := (T (T t t) t)

#eval (of_bool_list (to_bool_list t') = t' : bool)
-- tt
#eval (tree_of_string (string_of_tree t') = t' : bool)
-- tt
#eval string_of_tree t'
-- "fhFfhFvwC"

-- Ignores non-base64 content:
#eval (tree_of_string " fhF   fhF vwC" = t' : bool)
-- tt

[Kyle Miller]

It seems better to have a bespoke parser for your application, but having functions in mathlib to convert numbers to and from base64 seems useful.

[Kyle Miller]

(There was a some complexity in the implementation to help Lean see everything terminated. It runs a little stack manipulation language to build the tree from a list of bools.)

[Mario Carneiro]

If the base64 parser ignores non-base64 content, then you can just put newlines and indentation in the string if you need multiple lines (lean doesn't require single line literals). If this is for roth, you also don't need to encode the tree structure; you can just have a stream of "oracle calls" and just pull from the stream whenever you need to make a decision at any point in the tree

[Mario Carneiro]

BTW, it's nice to see us finally getting proofs that are a blob of bytes like metamath proofs :)

[Kevin Buzzard]

Didn't you do this already somewhere in the Matiyasevich proof?

[Mario Carneiro]

I don't think I have, although some applications have come close

[Mario Carneiro]

the matiyasevich proof is just a whole lot of single letter variables

[Mario Carneiro]

You're probably thinking of this: https://github.com/leanprover-community/mathlib/blob/master/src/number_theory/dioph.lean#L601-L612

[Mario Carneiro]

The bit at the beginning with a bunch of notations is more like manual typeclass inference proving that an expression is diophantine

[Mario Carneiro]

and it's not particularly "encoded" - it's a literal transcription of the input but with de bruijn variables

[Kevin Buzzard]

Whenever I think I can read mathlib I always remind myself that I still never made it through that part

[Yaël Dillies]

Mario Carneiro said:

you also don't need to encode the tree structure; you can just have a stream of "oracle calls" and just pull from the stream whenever you need to make a decision at any point in the tree

But is it not easier, or at least more principled; to build the tree first and then flatten it? To be clear, I need to make decisions all the time.

[Yaël Dillies]

Very nice, Kyle! I'm thinking that what we should have is a typeclass has_bytes to generally declare that a given type can be encoded with list bool and decoded from it. Then we can have a translation between list bool and base64. Both seem generally useful.

[Yaël Dillies]

I really like this little "Automate away Roth calculations" project. It's getting me to learn metaprogramming!

[Kevin Buzzard]

I think the reals biject with list bool (if you allow infinite lists)

[Yaël Dillies]

Have you ever heard of countability, Kevin? :grinning:

[Kevin Buzzard]

Oh it's finite lists of course :-(

[Kevin Buzzard]

So isn't this just denumerable then??

[Kevin Buzzard]

No -- I mean docs#encodable

[Kevin Buzzard]

And then you just biject list bool with nat (it bijects very naturally with pnat: regard ff as 0 and tt as 1, stick a 1 in front and you have a binary natural). Hopefully I'm getting the hang of this exotic list type now

[Yaël Dillies]

It is, yeah, except that we pick list bool as the encding state. Don't know if that matters too much for performance. That was my reasoning.

[Eric Wieser]

• dioph: a predicate stating that a set S ⊆ ℕ^α is Diophantine, i.e. that

Alright, keep your secrets

[Eric Rodriguez]

Eric Wieser said:

• dioph: a predicate stating that a set S ⊆ ℕ^α is Diophantine, i.e. that

Alright, keep your secrets

#12011

[Kyle Miller]

Mario Carneiro said:

If the base64 parser ignores non-base64 content, then you can just put newlines and indentation in the string if you need multiple lines (lean doesn't require single line literals).

Good idea -- the one I wrote already does :smile: Though I did that without fully realizing Lean strings allow raw newlines.

[Kyle Miller]

Yaël Dillies said:

I'm thinking that what we should have is a typeclass has_bytes to generally declare that a given type can be encoded with list bool and decoded from it. Then we can have a translation between list bool and base64. Both seem generally useful.

I know you like exploring rabbitholes, but this is a surprisingly deep one and I worry you might never return. :wink:

To make a serialization system that's robust, you would probably want a system that encodes a version into binary blob so that if you ever want to make changes to the interface later, you don't have to go and re-encode all your blobs, for example. If you don't have a generic system, then what you can do instead is create new decoding functions when you have new versions, and the choice of decoding function in the source code serves as the version indicator.

If embedding base64 certificates in proofs becomes more prevalent, then we'd have a better idea of what properties we'd want from serialization, and it might be worth having something more generic. But until then, I'd say it's additional work that shouldn't be done. (Even though I see why it would be useful.)

[Kyle Miller]

There was a trick in the base64 encoder for trees, by the way. It rounds the list bool up to the nearest multiple-of-six length, since base64 is a sequence of 6-bit numbers. I was relying on the fact that ff is interpreted in of_bool_list_aux as "push tree.nil onto the stack" and that at the end of evaluation, the function returns the top of stack. That means it can serve as a no-operation if it's at the beginning of the list.

The base64 encoder could deal with arbitrary list bool, though, by having it encode at the beginning how many bits to drop, using 3 additional bits to do so.

[Kyle Miller]

Kevin Buzzard said:

And then you just biject list bool with nat (it bijects very naturally with pnat: regard ff as 0 and tt as 1, stick a 1 in front and you have a binary natural). Hopefully I'm getting the hang of this exotic list type now

The first thing I tried was using docs#encodable for list bool, but the naturals it produced were hilariously large for the application.

The encoding scheme you mentioned would work, though. For these trees, you could skip having that 1 in front, actually, if you have the beginning of the list be the least-significant digits, because, incidentally, the list bool -> tree unit decoder can handle an arbitrary number of ff appended to the end.

[Yaël Dillies]

I'm afraid the only way to preserve me from a rabbithole is to fill it up yourself :grinning:

[Yaël Dillies]

What about we merge the correctness proof of the algorithm now and worry about making it effective later? (#10645 for reference)

[Kyle Miller]

Yaël Dillies said:

we pick list bool as the encoding state. Don't know if that matters too much for performance.

I mainly used list bool so that there'd be something to recurse on in of_bool_list_aux, but also it turns out nat.to_digits is very slow.

With a faster nat.to_digits, we can make reasonably efficient nat.to_base64 and nat.from_base64 functions.

Here's a simpler implementation than before using these functions:

tree <-> string via nat

import tactic
import data.tree
import data.nat.digits
import tactic.slim_check

--def base64_chars : string :=
--"ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"

def base64_to_char (n : ℕ) (h : n < 64) : char :=
if h1 : n < 26 then char.of_nat (n + 65)
else if h2 : n < 52 then char.of_nat (n + 71)
else if h3 : n < 62 then char.of_nat (n - 4)
else if h4 : n = 62 then '+'
else if h5 : n = 63 then '/'
else by { exfalso, simp at h3, interval_cases n; trivial, }

def base64_to_char' (n : ℕ) : char :=
if h : n < 64 then base64_to_char n h else 'A'

def base64_of_char (c : char) : option ℕ :=
let n := char.to_nat c in
if 65 <= n ∧ n < 91 then some (n - 65)
else if 97 <= n ∧ n < 123 then some (n - 71)
else if 48 <= n ∧ n < 58 then some (n + 4)
else if c = '+' then some 62
else if c = '/' then some 63
else none

--example (n : ℕ) (h : n < 64) : base64_of_char (base64_to_char n h) = n := by dec_trivial!
--example (n : ℕ) (h : n < 64) : base64_of_char (base64_to_char' n) = n := by dec_trivial!

/-- *much* faster than `nat.to_digits`. -/
def nat.to_digits' (base : ℕ) (h : 2 ≤ base) : ℕ → list ℕ
| 0 := []
| (n+1) :=
  have (n + 1) / base < n + 1, from nat.div_lt_self n.succ_pos (nat.succ_le_iff.mp h),
  ((n + 1) % base) :: nat.to_digits' ((n + 1) / base)

def nat.to_base64 (n : ℕ) : string :=
list.as_string $ (nat.to_digits' 64 (by norm_num) n).map base64_to_char'

def nat.from_base64 (s : string) : ℕ :=
nat.of_digits 64 (s.to_list >>= (λ c, (base64_of_char c).to_list))

--example (n : ℕ) : nat.from_base64 (nat.to_base64 n) = n := by slim_check

def to_nat_aux : tree unit → ℕ → ℕ
| tree.nil acc := 2 * acc
| (tree.node _ l r) acc := to_nat_aux l (to_nat_aux r (1 + 2 * acc))

def to_nat (t : tree unit) : ℕ := to_nat_aux t 0

def of_nat_aux_pop2 : list (tree unit) → tree unit × tree unit × list (tree unit)
| [] := (tree.nil, tree.nil, [])
| [t] := (t, tree.nil, [])
| (t :: t' :: ts) := (t, t', ts)

def of_nat_aux : list bool → list (tree unit) → tree unit
| [] [] := tree.nil
| [] (t :: _) := t
| (ff :: xs) stack := of_nat_aux xs (tree.nil :: stack)
| (tt :: xs) stack :=
  let (r, l, stack) := of_nat_aux_pop2 stack
  in of_nat_aux xs (tree.node () l r :: stack)

def string_of_tree (t : tree unit) : string := nat.to_base64 $ to_nat t

def tree_of_string (s : string) : tree unit :=
of_nat_aux (list.map (≠ 0) $ nat.to_digits' 2 rfl.ge (nat.from_base64 s)) []

/-! ## Examples -/

abbreviation N : tree unit := tree.nil
abbreviation T : tree unit → tree unit → tree unit := tree.node ()

def t := (T (T N (T (T N N) N)) (T N (T N (T (T N N) N))))
--def t := T N N

#eval (tree_of_string (string_of_tree t) = t : bool)
-- tt
#eval string_of_tree t
-- "ohe"

def t' := (T (T t t) t)

#eval (tree_of_string (string_of_tree t') = t' : bool)
-- tt
#eval string_of_tree t'
-- "ohe0Qf0Qf"

#eval string_of_tree tree.nil
-- ""

-- Ignores non-base64 content:
#eval (tree_of_string "  ohe 0Qf  0Q f " = t' : bool)
-- tt

[Yakov Pechersky]

Ah! I would suggest using parsers for base64_of_char! docs#parser.numeral

[Yakov Pechersky]

We can write a hex one and a base64 also.

[Mario Carneiro]

I want to point out that typeclasses like has_bytes and non-meta code is unnecessary here (again, assuming this is for roth). The main thing you need is:

• A type bitstream
• function read_bit : state bitstream bool which peels off one bit from the stream
• bitstream.mk : string -> bitstream which initializes a bitstream from a base64 string (the stream is self-closing so it is okay to have trailing 0's)
• (optional) a general typeclass implementing read : state bitstream A by calling read_bit several times, until you have enough entropy to reconstitute the type. This is basically a deserializer

[Mario Carneiro]

For Roth, I think the actual data you want to encode is bool, so you don't need the typeclass

[Mario Carneiro]

For constructing these streams we also need a utility to produce the stream and turn it into a string literal that can be pasted into the code

[Mario Carneiro]

but that would only be used during authoring, it wouldn't be run normally

[Yaël Dillies]

bitstream = list bool or do you have something else in mind? Kyle mentioned that doing arithmetic on $\N$ might be the fastest because it has special support in the kernel.

[Kyle Miller]

It seems compelling having abbreviation entropy := nat and then having rand_nat (hi : nat) : state entropy nat to get a number in the range [0,hi) when hi is positive (defined by returning s % hi and replacing the current state s with s / hi). (Maybe not using randomness terminology)

[Kyle Miller]

(An example for (de)serializing trees.)

now with monads

import tactic
import data.tree
import data.nat.digits
import tactic.slim_check

--def base64_chars : string :=
--"ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"

def base64_to_char (n : ℕ) (h : n < 64) : char :=
if h1 : n < 26 then char.of_nat (n + 65)
else if h2 : n < 52 then char.of_nat (n + 71)
else if h3 : n < 62 then char.of_nat (n - 4)
else if h4 : n = 62 then '+'
else if h5 : n = 63 then '/'
else by { exfalso, simp at h3, interval_cases n; trivial, }

def base64_to_char' (n : ℕ) : char :=
if h : n < 64 then base64_to_char n h else 'A'

def base64_of_char (c : char) : option ℕ :=
let n := char.to_nat c in
if 65 <= n ∧ n < 91 then some (n - 65)
else if 97 <= n ∧ n < 123 then some (n - 71)
else if 48 <= n ∧ n < 58 then some (n + 4)
else if c = '+' then some 62
else if c = '/' then some 63
else none

--example (n : ℕ) (h : n < 64) : base64_of_char (base64_to_char n h) = n := by dec_trivial!
--example (n : ℕ) (h : n < 64) : base64_of_char (base64_to_char' n) = n := by dec_trivial!

def nat.to_base64 (n : ℕ) : string :=
list.as_string $ (nat.digits 64 n).map base64_to_char'

def nat.from_base64 (s : string) : ℕ :=
nat.of_digits 64 (s.to_list >>= (λ c, (base64_of_char c).to_list))

--example (n : ℕ) : nat.from_base64 (nat.to_base64 n) = n := by slim_check

/-! ## nondeterminism certificate monad -/

abbreviation entropy := ℕ
abbreviation rands := state entropy

/-- should have `i < n` -/
def push_rand (i : ℕ) (n : ℕ) : rands unit :=
state_t.modify (λ e, i + e * n)

def seed_base64 (s : string) : rands unit :=
state_t.put (nat.from_base64 s)

def get_rand (n : ℕ) : rands ℕ := do
  e ← state_t.get,
  state_t.put (e / n),
  pure (e % n)

/-! ## Trees -/

def to_nat_aux : tree unit → rands unit
| tree.nil := push_rand 0 2
| (tree.node _ l r) := do
  to_nat_aux r,
  to_nat_aux l,
  push_rand 1 2

def to_nat (t : tree unit) : ℕ := (state_t.run (to_nat_aux t) 0).2

meta def of_nat_aux : rands (tree unit) := do
  b ← get_rand 2,
  if b = 0 then
    pure tree.nil
  else do
    l ← of_nat_aux,
    r ← of_nat_aux,
    pure $ tree.node () l r

def string_of_tree (t : tree unit) : string := nat.to_base64 $ to_nat t

meta def tree_of_string (s : string) : tree unit :=
(state_t.run (do seed_base64 s, of_nat_aux) 0).1

meta def print_string_of_tree (t : tree unit) (size : ℕ := 80) : io unit := do
  io.put_str "tree_of_string \"",
  io.put_str $ "\n".intercalate ((string_of_tree t).to_chunks size []),
  io.put_str "\""

/-! ## Examples -/

abbreviation N : tree unit := tree.nil
abbreviation T : tree unit → tree unit → tree unit := tree.node ()

def t := (T (T N (T (T N N) N)) (T N (T N (T (T N N) N))))
--def t := T N N

#eval (tree_of_string (string_of_tree t) = t : bool)
-- tt
#eval string_of_tree t
-- "bUD"

def t' := (T (T t t) t)

#eval (tree_of_string (string_of_tree t') = t' : bool)
-- tt
#eval string_of_tree t'
-- "vRN2oGbUD"

#eval string_of_tree tree.nil
-- ""

#eval tree_of_string ""
-- tree.nil

-- Ignores non-base64 content:
#eval (tree_of_string "  vRN2  oG bUD " = t' : bool)
-- tt

def bt : ℕ → tree unit
| 0 := tree.nil
| (n+1) := tree.node () (bt n) (bt n)

#eval print_string_of_tree (bt 12)

#eval (tree_of_string "//kJn
M5JTOZynM5kJPZyJT+JTOZyTmcykPZyJTeykTm8nM5kJPZyJT+kJnM5JTOZyPZyJTeykTm8JTOZyTmcy
k/JTOZyTmcykPZyJTeykTm8TmcyknM5kJfykTm8kJnM5PZyJTeykTm8JTOZyTmcykfykTm8kJnM5Tmcy
knM5kJ/nM5kJPZyJT+kJnM5JTOZyPZyJTeykTm8JTOZyTmcyk/kJnM5JTOZynM5kJPZyJT+JTOZyTmcy
kPZyJTeykTm8PZyJTeykTm8JTOZyTmcykfykTm8kJnM5TmcyknM5kJ/JTOZyTmcykPZyJTeykTm8Tmcy
knM5kJfykTm8kJnM5/JTOZyTmcykPZyJTeykTm8TmcyknM5kJfykTm8kJnM5PZyJTeykTm8JTOZyTmcy
kfykTm8kJnM5TmcyknM5kJ/TmcyknM5kJfykTm8kJnM5nM5kJPZyJT+kJnM5JTOZyfykTm8kJnM5Tmcy
knM5kJ/kJnM5JTOZynM5kJPZyJT+PZyJTeykTm8JTOZyTmcykfykTm8kJnM5TmcyknM5kJ/JTOZyTmcy
kPZyJTeykTm8TmcyknM5kJfykTm8kJnM5fykTm8kJnM5TmcyknM5kJ/kJnM5JTOZynM5kJPZyJT+Tmcy
knM5kJfykTm8kJnM5nM5kJPZyJT+kJnM5JTOZy/nM5kJPZyJT+kJnM5JTOZyPZyJTeykTm8JTOZyTmcy
k/kJnM5JTOZynM5kJPZyJT+JTOZyTmcykPZyJTeykTm8PZyJTeykTm8JTOZyTmcykfykTm8kJnM5Tmcy
knM5kJ/JTOZyTmcykPZyJTeykTm8TmcyknM5kJfykTm8kJnM5/kJnM5JTOZynM5kJPZyJT+JTOZyTmcy
kPZyJTeykTm8nM5kJPZyJT+kJnM5JTOZyPZyJTeykTm8JTOZyTmcyk/JTOZyTmcykPZyJTeykTm8Tmcy
knM5kJfykTm8kJnM5PZyJTeykTm8JTOZyTmcykfykTm8kJnM5TmcyknM5kJ/PZyJTeykTm8JTOZyTmcy
kfykTm8kJnM5TmcyknM5kJ/JTOZyTmcykPZyJTeykTm8TmcyknM5kJfykTm8kJnM5fykTm8kJnM5Tmcy
knM5kJ/kJnM5JTOZynM5kJPZyJT+TmcyknM5kJfykTm8kJnM5nM5kJPZyJT+kJnM5JTOZy/JTOZyTmcy
kPZyJTeykTm8TmcyknM5kJfykTm8kJnM5PZyJTeykTm8JTOZyTmcykfykTm8kJnM5TmcyknM5kJ/Tmcy
knM5kJfykTm8kJnM5nM5kJPZyJT+kJnM5JTOZyfykTm8kJnM5TmcyknM5kJ/kJnM5JTOZynM5kJPZyJT" = bt 12 : bool)
-- tt

[Mario Carneiro]

Yaël Dillies said:

bitstream = list bool or do you have something else in mind? Kyle mentioned that doing arithmetic on $\N$ might be the fastest because it has special support in the kernel.

I think that pulling bits from a list is faster than base conversion if you pull things of non-power-of-two sizes from the stream

[Mario Carneiro]

The fastest way to implement something that pulls directly from a base64 string is something like string.iterator * nat * nat where the pair of nat represents the last decoded number and the number of bits remaining in it