<commit_before>module BinaryTreesEnumeration

open FStar.List

abstract val pairs_with_sum' : m:nat -> n:nat -> list (p: (nat * nat){fst p + snd p == m + n})
abstract let rec pairs_with_sum' m n =
  (m, n) ::
    (if m = 0
     then []
     else pairs_with_sum' (m - 1) (n + 1))

let pairs_with_sum (n: nat) : list (p: (nat * nat){fst p + snd p == n}) =
  pairs_with_sum' n 0

let product #a #b (l1: list a) (l2: list b) =
  List.Tot.concatMap (fun x1 -> List.Tot.map (fun x2 -> (x1, x2)) l2) l1

type bin_tree =
| Leaf
| Branch of bin_tree * bin_tree

let rec size bt : nat =
  match bt with
  | Leaf -> 0
  | Branch(l, r) -> 1 + size l + size r

(*> * Why do I need type annotations on [concatMap] and [map]?
    * When I reduce this definition I see that the lambda desugared to a match
      with 4 arguments (not 2). Why?
    * I had to eta-expand [Branch]; why?  Is it because there's a implicit cast
      from [bintree] to [bt: bin_tree{size bt == s}]?  If so, why is it not
      enough to add a coercion [Branch <: _ -> bt: bin_tree{size bt == s}]? *)
let rec trees_of_size (s: nat) : list (bt: bin_tree{size bt == s}) =
  if s = 0 then
    [Leaf]
  else
    List.Tot.concatMap #(p: (nat * nat){(fst p) + (snd p) == s - 1})
      (fun (s1, s2) ->
       List.Tot.map #((t1: bin_tree{size t1 == s1}) * (t2: bin_tree{size t2 == s2}))
                    #(bt: bin_tree{size bt == s})
         (fun (t1, t2) -> Branch (t1, t2))
         (product (trees_of_size s1) (trees_of_size s2)))
      (pairs_with_sum (s - 1))

(*> Why do I need to re-state the goal as an [assert] here? *)
abstract let rec pws'_complete (m d n: nat) :
  Lemma (List.memP (m, n + d) (pairs_with_sum' (m + d) n)) =
    if d = 0 then ()
    else begin
      assert (m + d <> 0);
      pws'_complete m (d - 1) (n + 1);
      assert (List.memP (m, n + d) (pairs_with_sum' (m + d - 1) (n + 1)));
      assert (List.memP (m, n + d) (pairs_with_sum' (m + d) n))
    end

(*> Why do I need to explicitly unfold [pairs_with_sum]? *)
let pws_complete (m n: nat) :
  Lemma (List.memP (m, n) (pairs_with_sum (m + n))) =
    assert (pairs_with_sum (m + n) == pairs_with_sum' (m + n) 0);
    pws'_complete m n 0
<commit_msg>Add an extra assert required on latest master<commit_after>module BinaryTreesEnumeration

open FStar.List

abstract val pairs_with_sum' : m:nat -> n:nat -> list (p: (nat * nat){fst p + snd p == m + n})
abstract let rec pairs_with_sum' m n =
  (m, n) ::
    (if m = 0
     then []
     else pairs_with_sum' (m - 1) (n + 1))

let pairs_with_sum (n: nat) : list (p: (nat * nat){fst p + snd p == n}) =
  pairs_with_sum' n 0

let product #a #b (l1: list a) (l2: list b) =
  List.Tot.concatMap (fun x1 -> List.Tot.map (fun x2 -> (x1, x2)) l2) l1

type bin_tree =
| Leaf
| Branch of bin_tree * bin_tree

let rec size bt : nat =
  match bt with
  | Leaf -> 0
  | Branch(l, r) -> 1 + size l + size r

(*> * Why do I need type annotations on [concatMap] and [map]?
    * When I reduce this definition I see that the lambda desugared to a match
      with 4 arguments (not 2). Why?
    * I had to eta-expand [Branch]; why?  Is it because there's a implicit cast
      from [bintree] to [bt: bin_tree{size bt == s}]?  If so, why is it not
      enough to add a coercion [Branch <: _ -> bt: bin_tree{size bt == s}]? *)
let rec trees_of_size (s: nat) : list (bt: bin_tree{size bt == s}) =
  if s = 0 then
    [Leaf]
  else
    List.Tot.concatMap #(p: (nat * nat){(fst p) + (snd p) == s - 1})
      (fun (s1, s2) ->
       List.Tot.map #((t1: bin_tree{size t1 == s1}) * (t2: bin_tree{size t2 == s2}))
                    #(bt: bin_tree{size bt == s})
         (fun (t1, t2) -> Branch (t1, t2))
         (product (trees_of_size s1) (trees_of_size s2)))
      (pairs_with_sum (s - 1))

(*> * Why do I need to re-state the goal as an [assert]?
    * Why do I need to re-state the lemma as an [assert]? *)
abstract let rec pws'_complete (m d n: nat) :
  Lemma (List.memP (m, n + d) (pairs_with_sum' (m + d) n)) =
    if d = 0 then ()
    else begin
      assert (m + d <> 0);
      pws'_complete m (d - 1) (n + 1);
      assert (List.memP (m, (n + 1) + (d - 1)) (pairs_with_sum' (m + (d - 1)) (n + 1)));
      assert (List.memP (m, n + d) (pairs_with_sum' (m + d) n))
    end

(*> Why do I need to explicitly unfold [pairs_with_sum]? *)
let pws_complete (m n: nat) :
  Lemma (List.memP (m, n) (pairs_with_sum (m + n))) =
    assert (pairs_with_sum (m + n) == pairs_with_sum' (m + n) 0);
    pws'_complete m n 0

{'fraction_non_alphanumeric': 0.1592683470890029, 'fraction_numerical': 0.018737452598706225, 'mean_word_length': 2.5987158908507224, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3625781', 'n_tokens_mistral': 1856, 'n_tokens_neox': 1788, 'n_words': 647}