Idiomatic way to split into cases 0, 1, and 2≤

Stream: lean4

[Markus Schmaus]

A couple of times now I had n : ℕ and wanted to split my proof into three cases, n = 0, n = 1, and 2 ≤ n. I can get there using multiple by_cases, but I wonder if there is a more idiomatic way to get there. The most recent case also works as an mwe

import Mathlib

theorem Nat.log2_eq_size_pred (n : Nat) : log2 n  = size n - 1 := by
  induction n using Nat.binaryRec with
  | z => rfl
  | f b n ih =>
    unfold log2
    sorry

In this case I want to split into the three cases for bit b n.

[Markus Schmaus]

This mwe uses Mathlib (due to docs#Nat.size), but I would assume that splitting into those three cases could be done without relying on Mathlib.

[Henrik Böving]

You can use the normal programming match in tactics as well to pattern match on some number arbitrarily

[Damiano Testa]

Also, rcases n with _|_|n may get you to the right place (untested).

[Markus Schmaus]

I tried match, and I can split it into three cases, but how to I get the hypothesis 2 ≤ bit b n in the last case?

import Mathlib

theorem Nat.log2_eq_size_pred (n : Nat) : log2 n  = size n - 1 := by
  induction n using Nat.binaryRec with
  | z => rfl
  | f b n ih =>
    unfold log2
    match m : bit b n with
    | 0 => rfl
    | 1 => rfl
    | x =>
      rw [← m]
      sorry

[Henrik Böving]

import Mathlib

theorem Nat.log2_eq_size_pred (n : Nat) : log2 n  = size n - 1 := by
  induction n using Nat.binaryRec with
  | z => rfl
  | f b n ih =>
    unfold log2
    match h : bit b n with
    | 0 => rfl
    | 1 => rfl
    | x + 2 => -- note that we explicitly match on x + 2 here and lean understands that the other cases are not possible
      -- You could explicitly derive it now but we can also just do
      simp
      sorry

[Markus Schmaus]

This is how I completed the proof using match, rcases n with _|_|n works as well.

import Mathlib

namespace Nat

@[simp]
theorem bit_div_two {b : Bool} {n : Nat} : bit b n / 2 = n := by
  cases b <;> simp only [bit_false, bit_true, Nat.bit1_div_two, Nat.bit0_div_two]

@[simp]
theorem bit_true_zero : bit true 0 = 1 := rfl

@[simp]
theorem bit_false_zero : bit false 0 = 0 := rfl

theorem log2_eq_size_pred (n : Nat) : log2 n  = size n - 1 := by
  induction n using Nat.binaryRec with
  | z => rfl
  | f b n ih =>
    unfold log2
    match hm : bit b n with
    | 0 => rfl
    | 1 => rfl
    | x + 2 =>
      simp only [ge_iff_le, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceIte]
      simp only [succ_eq_add_one] at hm
      rw [← hm]
      have : Nat.bit b n ≠ 0 := by omega
      simp only [bit_div_two, ih, Nat.size_bit this, succ_eq_add_one, add_tsub_cancel_right]
      match n with
      | 0 =>
        induction b <;> simp at hm
      | m + 1 =>
        apply Nat.sub_add_cancel
        apply Nat.size_le_size (m := 1)
        omega

[Eric Wieser]

Are you looking for docs#Nat.binaryRec' (the primed one)?

[Markus Schmaus]

I see that docs#Nat.binaryRec' allows me to replace the induction b <;> simp at hm line by a simple simp_all, but I don't see how it would have helped me with any of the case distinctions I made.

[Yuyang Zhao]

import Mathlib

theorem Nat.log2_eq_size_pred (n : Nat) : log2 n = size n - 1 := by
  induction n using Nat.binaryRecFromOne with
  | z₀ | z₁ => rfl
  | f b n n0 ih =>
    have : 2 ≤ bit b n := by
      rw [bit_val]; omega
    sorry