How to 'prove by direct computation'?

Stream: general

[Icaro Costa]

I am trying to prove a combinatorial problem in lean, and I would like it to prove that the lhs equals rhs by directly computing it. Here is the code for context: lean shell.

I tried to do calc, but then I need some tactic to justify it, bit I don't know which

[Aaron Liu]

Since generate_binary_lists.aux is done by well-founded recursion it's irreducible

[Aaron Liu]

you will have to unfold it manually

[Edward van de Meent]

your code seems to have syntax issues... can you use sorry to make sure it at least compiles?

[Kenny Lau]

do you have a mathematical proof?

[Aaron Liu]

import Mathlib
open Nat
open List

--Made with llama4
def generate_binary_lists (k : Nat) (m : Nat) : List (List Nat) :=
  let rec aux (ones_left : Nat) (zeros_left : Nat) (current : List Nat) : List (List Nat) :=
    if ones_left = 0 && zeros_left = 0 then
      [current]
    else
      (if ones_left > 0 then aux (ones_left - 1) zeros_left (current ++ [1]) else [])
      ++ (if zeros_left > 0 then aux ones_left (zeros_left - 1) (current ++ [0]) else [])
  aux k m []

#eval length (generate_binary_lists 0 0)

#check factorial

theorem comb_fixed_ones (k m : ℕ) : length (generate_binary_lists k m) = (factorial (k + m))/((factorial k)*(factorial m)) := by
  have hm := Nat.factorial_ne_zero m
  have hk := Nat.factorial_ne_zero k
  induction k with
  | zero =>
    rw [← add_choose, zero_add, choose_self]
    induction m with
    | zero =>
      rw [generate_binary_lists, generate_binary_lists.aux]
      simp
    | succ => sorry
  | succ => sorry

[Icaro Costa]

Sorry, what do you mean by "unfolding"? @Aaron Liu

[Aaron Liu]

Icaro Costa said:

Sorry, what do you mean by "unfolding"? Aaron Liu

It's when you replace a constant by its definition

[Icaro Costa]

Kenny Lau said:

do you have a mathematical proof?

It is just how many combinations are there for shuffles of a binary string with a fixed amount of ones and zeros

[Icaro Costa]

@Aaron Liu How would I go about doing this manually then?

[Aaron Liu]

I've just showed you in the code block I posted at #general > How to 'prove by direct computation'? @ 💬

[Icaro Costa]

Oh, sorry

[Aaron Liu]

You can click on the link in the top right corner of the code block and it will take you to the online playground

[Icaro Costa]

I managed to see it, I think I see what you mean by doing it manually. Thank you very much!

[Johannes Tantow]

You can also try with this formulation

def generate_binary_lists' (k : Nat) (m : Nat) : List (List Nat) :=
  go k m []
where
  go (k m : Nat) (curr : List Nat) :=
  match k, m with
  | zero, zero => [curr]
  | succ n, zero => go n m (curr ++ [1])
  | zero, succ n => go 0 n (curr ++ [0])
  | succ n, succ l => go n (succ l) (curr ++ [1]) ++ go (succ n) l (curr ++ [0])

[Aaron Liu]

Unfortunately it's still using well-founded recursion :(

[Aaron Liu]

You'll have to wrap it in two levels of auxiliary function to do structural recursion

[Johannes Tantow]

Really? What am I missing that makes this not structural?

[Aaron Liu]

it's not structural in k and it's not structural in m

[Aaron Liu]

since neither is strictly decreasing

[Aaron Liu]

you can probably make it structural in k + m

[Johannes Tantow]

Ok, makes sense

[Aaron Liu]

actually probably not since addition is asymmetric

[Robin Arnez]

This works without 'prove by direct computation'?

import Mathlib

def generate_binary_lists (k : Nat) (m : Nat) : List (List Nat) :=
  go k m []
where
  go (k m : Nat) (curr : List Nat) :=
    match k, m with
    | .zero, .zero => [curr]
    | .succ n, .zero => go n m (curr ++ [1])
    | .zero, .succ n => go 0 n (curr ++ [0])
    | .succ n, .succ l => go n (.succ l) (curr ++ [1]) ++ go (.succ n) l (curr ++ [0])

theorem comb_fixed_ones (k m : ℕ) : (generate_binary_lists k m).length = ((k + m).factorial)/(k.factorial * m.factorial) := by
  rw [generate_binary_lists]
  generalize [] = l
  fun_induction generate_binary_lists.go with
  | case1 => simp
  | case2 l n ih => simp_all [Nat.div_self, Nat.factorial_pos]
  | case3 l n ih => simp_all [Nat.div_self, Nat.factorial_pos]
  | case4 l k m ih ih' =>
    simp only [Nat.succ_eq_add_one] at ih ih'
    simp only [Nat.succ_eq_add_one, List.length_append, ih, ih', ← Nat.add_choose]
    simp +arith [Nat.choose_succ_succ]

[Aaron Liu]

I've figured out a version which is structurally recursive

def generateBinaryLists (k : Nat) (m : Nat) : List (List Nat) :=
  go k m []
where
  goZero (k : Nat) (curr : List Nat) : List (List Nat) :=
    match k with
    | 0 => [curr]
    | n + 1 => goZero n (curr ++ [1])
  goSucc (k : Nat) (prev : Nat → List Nat → List (List Nat)) (curr : List Nat) : List (List Nat) :=
    match k with
    | 0 => prev 0 (curr ++ [0])
    | n + 1 => goSucc n prev (curr ++ [1]) ++ prev (n + 1) (curr ++ [0])
  go (k m : Nat) (curr : List Nat) : List (List Nat) :=
    match m with
    | 0 => goZero k curr
    | l + 1 => goSucc k (fun k curr => go k l curr) curr

[Aaron Liu]

it gives the same result

[Aaron Liu]

but you need more definitions