Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+โ Ctrl+โ to navigate,
Ctrl+๐ฑ๏ธ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
! This file was ported from Lean 3 source module data.nat.size
! leanprover-community/mathlib commit 18a5306c091183ac90884daa9373fa3b178e8607
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Pow
import Mathlib.Data.Nat.Bits
/-! Lemmas about `size`. -/
namespace Nat
/-! ### `shiftl` and `shiftr` -/
section
set_option linter.deprecated false
theorem shiftl_eq_mul_pow ( m ) : โ n , shiftl m n = m * 2 ^ n
| 0 => ( Nat.mul_one : โ (n : โ ), n * 1 = n _ ). symm : โ {ฮฑ : Sort ?u.139} {a b : ฮฑ }, a = b b = a symm
| k + 1 => by
show bit0 : {ฮฑ : Type ?u.308} โ [inst : Add ฮฑ ฮฑ โ ฮฑ ( shiftl m k ) = m * ( 2 ^ k * 2 )
rw [ bit0_val , shiftl_eq_mul_pow m k , mul_comm 2 , mul_assoc : โ {G : Type ?u.791} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ]
#align nat.shiftl_eq_mul_pow Nat.shiftl_eq_mul_pow : โ (m n : โ ), shiftl m n = m * 2 ^ n
theorem shiftl'_tt_eq_mul_pow ( m ) : โ n , shiftl' true m n + 1 = ( m + 1 ) * 2 ^ n
| 0 => by simp [ shiftl , shiftl' , pow_zero : โ (n : โ ), n ^ 0 = 1 , Nat.one_mul : โ (n : โ ), 1 * n = n ]
| k + 1 => by
change bit1 : {ฮฑ : Type ?u.1700} โ [inst : One ฮฑ [inst : Add ฮฑ ฮฑ โ ฮฑ ( shiftl' true m k ) + 1 = ( m + 1 ) * ( 2 ^ k * 2 )
rw [ bit1_val ]
change 2 * ( shiftl' true m k + 1 ) = _
rw [ shiftl'_tt_eq_mul_pow m k , 2 * ((m + 1 * 2 ^ k )= (m + 1 * (2 ^ k * 2 mul_left_comm , (m + 1 * (2 * 2 ^ k = (m + 1 * (2 ^ k * 2 mul_comm 2 (m + 1 * (2 ^ k * 2 = (m + 1 * (2 ^ k * 2 ]
#align nat.shiftl'_tt_eq_mul_pow Nat.shiftl'_tt_eq_mul_pow
end
theorem one_shiftl ( n ) : shiftl 1 n = 2 ^ n :=
( shiftl_eq_mul_pow _ _ ). trans : โ {ฮฑ : Sort ?u.2590} {a b c : ฮฑ }, a = b b = c a = c trans ( Nat.one_mul : โ (n : โ ), 1 * n = n _ )
#align nat.one_shiftl Nat.one_shiftl
@[ simp ]
theorem zero_shiftl ( n ) : shiftl 0 n = 0 :=
( shiftl_eq_mul_pow _ _ ). trans : โ {ฮฑ : Sort ?u.2651} {a b c : ฮฑ }, a = b b = c a = c trans ( Nat.zero_mul : โ (n : โ ), 0 * n = 0 _ )
#align nat.zero_shiftl Nat.zero_shiftl
theorem shiftr_eq_div_pow ( m ) : โ n , shiftr m n = m / 2 ^ n
| 0 => ( Nat.div_one : โ (n : โ ), n / 1 = n _ ). symm : โ {ฮฑ : Sort ?u.2814} {a b : ฮฑ }, a = b b = a symm
| k + 1 =>
( congr_arg : โ {ฮฑ : Sort ?u.2923} {ฮฒ : Sort ?u.2922} {aโ aโ : ฮฑ } (f : ฮฑ โ ฮฒ aโ = aโ f aโ = f aโ div2 ( shiftr_eq_div_pow m k )). trans : โ {ฮฑ : Sort ?u.2931} {a b c : ฮฑ }, a = b b = c a = c trans <| by
rw [ div2_val , Nat.div_div_eq_div_mul : โ (m n k : โ ), m / n / k = m / (n * k , Nat.pow_succ ]
#align nat.shiftr_eq_div_pow Nat.shiftr_eq_div_pow : โ (m n : โ ), shiftr m n = m / 2 ^ n
@[ simp ]
theorem zero_shiftr ( n ) : shiftr 0 n = 0 :=
( shiftr_eq_div_pow _ _ ). trans : โ {ฮฑ : Sort ?u.3189} {a b c : ฮฑ }, a = b b = c a = c trans ( Nat.zero_div : โ (b : โ ), 0 / b = 0 _ )
#align nat.zero_shiftr Nat.zero_shiftr
theorem shiftl'_ne_zero_left ( b ) { m } ( h : m โ 0 ) ( n ) : shiftl' b m n โ 0 := by
induction n <;> simp [ bit_ne_zero , shiftl' , *]
#align nat.shiftl'_ne_zero_left Nat.shiftl'_ne_zero_left
theorem shiftl'_tt_ne_zero ( m ) : โ { n }, ( n โ 0 ) โ shiftl' true m n โ 0
| 0 , h => absurd : โ {a : Prop } {b : Sort ?u.3574}, a โ ยฌ a b rfl : โ {ฮฑ : Sort ?u.3577} {a : ฮฑ }, a = a h
| succ _, _ => Nat.bit1_ne_zero _
#align nat.shiftl'_tt_ne_zero Nat.shiftl'_tt_ne_zero
/-! ### `size` -/
@[ simp ]
theorem size_zero : size 0 = 0 := by simp [ size ]
#align nat.size_zero Nat.size_zero : size 0 = 0
@[ simp ]
theorem size_bit { b n } ( h : bit b n โ 0 ) : size ( bit b n ) = succ ( size n ) := by
rw [ size ]
conv =>
lhs
rw [ binaryRec : {C : โ โ Sort ?u.4003C 0 ((b : Bool ) โ (n : โ ) โ C n C (bit b n ) โ (n : โ ) โ C n ]
simp [ h ]
rw [ div2_bit ]
#align nat.size_bit Nat.size_bit
section
set_option linter.deprecated false
@[ simp ]
theorem size_bit0 { n } ( h : n โ 0 ) : size ( bit0 : {ฮฑ : Type ?u.4844} โ [inst : Add ฮฑ ฮฑ โ ฮฑ n ) = succ ( size n ) :=
@ size_bit false n ( Nat.bit0_ne_zero : โ {n : โ }, n โ 0 bit0 n โ 0 h )
#align nat.size_bit0 Nat.size_bit0
@[ simp ]
theorem size_bit1 ( n ) : size ( bit1 : {ฮฑ : Type ?u.4929} โ [inst : One ฮฑ [inst : Add ฮฑ ฮฑ โ ฮฑ n ) = succ ( size n ) :=
@ size_bit true n ( Nat.bit1_ne_zero n )
#align nat.size_bit1 Nat.size_bit1
@[ simp ]
theorem size_one : size 1 = 1 :=
show size ( bit1 : {ฮฑ : Type ?u.5073} โ [inst : One ฮฑ [inst : Add ฮฑ ฮฑ โ ฮฑ 0 ) = 1 by rw [ size_bit1 , size_zero ]
#align nat.size_one Nat.size_one
end
@[ simp ]
theorem size_shiftl' { b m n } ( h : shiftl' b m n โ 0 ) : size ( shiftl' b m n ) = size m + n := by
induction' n with n IH <;> simp [ shiftl' ] at h โข
rw [ size_bit h , Nat.add_succ ]
by_cases s0 : shiftl' b m n = 0 <;> [ skip ; rw [ IH s0 ] ]
rw [ s0 ] at h โข
cases b ; ยท exact absurd : โ {a : Prop } {b : Sort ?u.5887}, a โ ยฌ a b rfl : โ {ฮฑ : Sort ?u.5890} {a : ฮฑ }, a = a h
have : shiftl' true m n + 1 = 1 := congr_arg : โ {ฮฑ : Sort ?u.5998} {ฮฒ : Sort ?u.5997} {aโ aโ : ฮฑ } (f : ฮฑ โ ฮฒ aโ = aโ f aโ = f aโ (ยท + 1) s0
rw [ shiftl'_tt_eq_mul_pow ] at this
obtain rfl := succ.inj ( eq_one_of_dvd_one : โ {n : โ }, n โฃ 1 n = 1 โจ _ , this : (m + 1 * 2 ^ n = 1 this . symm : โ {ฮฑ : Sort ?u.6144} {a b : ฮฑ }, a = b b = a โฉ)
simp only [ zero_add , one_mul ] at this : (0 + 1 * 2 ^ n = 1 this
obtain rfl : n = 0 :=
Nat.eq_zero_of_le_zero : โ {n : โ }, n โค 0 n = 0
( le_of_not_gt fun hn => ne_of_gt : โ {a b : โ }, b < a a โ b ( pow_lt_pow_of_lt_right : โ {x : โ }, 1 < x โ {i j : โ }, i < j x ^ i < x ^ j ( by decide ) hn ) this )
rfl
#align nat.size_shiftl' Nat.size_shiftl'
@[ simp ]
theorem size_shiftl { m } ( h : m โ 0 ) ( n ) : size ( shiftl m n ) = size m + n :=
size_shiftl' ( shiftl'_ne_zero_left _ h _ )
#align nat.size_shiftl Nat.size_shiftl
theorem lt_size_self ( n : โ ) : n < 2 ^ size n := by
rw [ โ one_shiftl ]
have : โ { n }, n = 0 โ n < shiftl 1 ( size n ) := by simp
apply binaryRec : โ {C : โ โ Sort ?u.7322C 0 (โ (b : Bool ) (n : โ ), C n C (bit b n ) โ โ (n : โ ), C n _ _ : โ (b : Bool ) (n : โ ), ?m.7323 n ?m.7323 (bit b n n
ยท apply this rfl : โ {ฮฑ : Sort ?u.7331} {a : ฮฑ }, a = a
intro b n IH
by_cases h : bit b n = 0
ยท apply this h
rw [ size_bit h , shiftl_succ ]
exact bit_lt_bit0 _ IH
#align nat.lt_size_self Nat.lt_size_self : โ (n : โ ), n < 2 ^ size n
theorem size_le { m n : โ } : size m โค n โ m < 2 ^ n :=
โจ fun h => lt_of_lt_of_le : โ {ฮฑ : Type ?u.7547} [inst : Preorder ฮฑ a b c : ฮฑ }, a < b b โค c a < c ( lt_size_self _ ) ( pow_le_pow_of_le_right : โ {n : โ }, n > 0 โ {i j : โ }, i โค j n ^ i โค n ^ j ( by decide ) h ), by
rw [ โ one_shiftl ] ; revert n
apply binaryRec : โ {C : โ โ Sort ?u.7689C 0 (โ (b : Bool ) (n : โ ), C n C (bit b n ) โ โ (n : โ ), C n _ _ : โ (b : Bool ) (n : โ ), ?m.7690 n ?m.7690 (bit b n m
ยท intro n
simp
ยท intro b m IH n h
by_cases e : bit b m = 0
ยท simp [ e ]
rw [ size_bit e ]
cases' n with n
ยท exact e . elim : โ {a : Prop } {ฮฑ : Sort ?u.8385}, ยฌ a a โ ฮฑ ( Nat.eq_zero_of_le_zero : โ {n : โ }, n โค 0 n = 0 ( le_of_lt_succ h ))
ยท apply succ_le_succ ( IH _ )
apply lt_imp_lt_of_le_imp_le : โ {ฮฑ : Type ?u.8413} {ฮฒ : Type ?u.8414} [inst : LinearOrder ฮฑ inst_1 : Preorder ฮฒ a b : ฮฑ } {c d : ฮฒ },
(a โค b c โค d d < c b < a ( fun h' => bit0_le_bit _ h' ) h โฉ
#align nat.size_le Nat.size_le
theorem lt_size { m n : โ } : m < size n โ 2 ^ m โค n := by
rw [ โ not_lt , Decidable.iff_not_comm , not_lt , size_le ]
#align nat.lt_size Nat.lt_size
theorem size_pos { n : โ } : 0 < size n โ 0 < n := by rw [ lt_size ] ; rfl
#align nat.size_pos Nat.size_pos
theorem size_eq_zero { n : โ } : size n = 0 โ n = 0 := by
have := @ size_pos n ; simp [ pos_iff_ne_zero ] at this ; exact Decidable.not_iff_not . 1 : โ {a b : Prop }, (a โ b a โ b this
#align nat.size_eq_zero Nat.size_eq_zero
theorem size_pow { n : โ } : size ( 2 ^ n ) = n + 1 :=
le_antisymm ( size_le . 2 : โ {a b : Prop }, (a โ b b โ a <| pow_lt_pow_of_lt_right : โ {x : โ }, 1 < x โ {i j : โ }, i < j x ^ i < x ^ j ( by decide ) ( lt_succ_self _ ))
( lt_size . 2 : โ {a b : Prop }, (a โ b b โ a <| le_rfl )
#align nat.size_pow Nat.size_pow
theorem size_le_size { m n : โ } ( h : m โค n ) : size m โค size n :=
size_le . 2 : โ {a b : Prop }, (a โ b b โ a <| lt_of_le_of_lt : โ {ฮฑ : Type ?u.10397} [inst : Preorder ฮฑ a b c : ฮฑ }, a โค b b < c a < c h ( lt_size_self _ )
#align nat.size_le_size Nat.size_le_size
theorem size_eq_bits_len ( n : โ ) : n . bits . length = n . size := by
induction' n using Nat.binaryRec' : {C : โ โ Sort u_1C 0 ((b : Bool ) โ (n : โ ) โ (n = 0 b = true C n C (bit b n ) โ (n : โ ) โ C n with b n h ih ; ยท simp
rw [ size_bit , bits_append_bit _ _ h ]
ยท simp [ ih ]
ยท simpa [ bit_eq_zero_iff ]
#align nat.size_eq_bits_len Nat.size_eq_bits_len
end Nat