English
If n > 0 and n < b, then Nat.digits b n = [n] and 1 < b and 0 < n.
Русский
Если n > 0 и n < b, то Nat.digits b n = [n] и 1 < b и 0 < n.
LaTeX
$$$\\forall b,n\\in\\mathbb{N},\\; n > 0 \\land n < b \\Rightarrow Nat.digits\\; b\\; n = [n] \\land 1 < b \\land 0 < n$$$
Lean4
theorem digits_one (b n) (n0 : 0 < n) (nb : n < b) : Nat.digits b n = [n] ∧ 1 < b ∧ 0 < n :=
by
have b2 : 1 < b := lt_iff_add_one_le.mpr (le_trans (add_le_add_right (lt_iff_add_one_le.mp n0) 1) nb)
refine ⟨?_, b2, n0⟩
rw [Nat.digits_def' b2 n0, Nat.mod_eq_of_lt nb, Nat.div_eq_zero_iff.2 <| .inr nb, Nat.digits_zero]
/-
Porting note: this part of the file is tactic related.
open Tactic
-- failed to format: unknown constant 'term.pseudo.antiquot'
/-- Helper function for the `norm_digits` tactic. -/ unsafe
def
eval_aux
( eb : expr ) ( b : ℕ ) : expr → ℕ → instance_cache → tactic ( instance_cache × expr × expr )
|
en , n , ic
=>
do
let m := n / b
let r := n % b
let ( ic , er ) ← ic . ofNat r
let ( ic , pr ) ← norm_num.prove_lt_nat ic er eb
if
m = 0
then
do
let ( _ , pn0 ) ← norm_num.prove_pos ic en
return
(
ic
,
q( ( [ $ ( en ) ] : List Nat ) )
,
q( digits_one $ ( eb ) $ ( en ) $ ( pn0 ) $ ( pr ) )
)
else
do
let em ← expr.of_nat q( ℕ ) m
let ( _ , pe ) ← norm_num.derive q( ( $ ( er ) + $ ( eb ) * $ ( em ) : ℕ ) )
let ( ic , el , p ) ← eval_aux em m ic
return
(
ic
,
q( @ List.cons ℕ $ ( er ) $ ( el ) )
,
q(
digits_succ
$ ( eb ) $ ( en ) $ ( em ) $ ( er ) $ ( el ) $ ( pe ) $ ( pr ) $ ( p )
)
)
/-- A tactic for normalizing expressions of the form `Nat.digits a b = l` where
`a` and `b` are numerals.
```
example : Nat.digits 10 123 = [3,2,1] := by norm_num
```
-/
@[norm_num]
unsafe def eval : expr → tactic (expr × expr)
| q(Nat.digits $(eb) $(en)) => do
let b ← expr.to_nat eb
let n ← expr.to_nat en
if n = 0 then return (q(([] : List ℕ)), q(Nat.digits_zero $(eb)))
else
if b = 0 then do
let ic ← mk_instance_cache q(ℕ)
let (_, pn0) ← norm_num.prove_ne_zero' ic en
return (q(([$(en)] : List ℕ)), q(@Nat.digits_zero_succ' $(en) $(pn0)))
else
if b = 1 then do
let ic ← mk_instance_cache q(ℕ)
let s ← simp_lemmas.add_simp simp_lemmas.mk `list.replicate
let (rhs, p2, _) ← simplify s [] q(List.replicate $(en) 1)
let p ← mk_eq_trans q(Nat.digits_one $(en)) p2
return (rhs, p)
else do
let ic ← mk_instance_cache q(ℕ)
let (_, l, p) ← eval_aux eb b en n ic
let p ← mk_app `` And.left [p]
return (l, p)
| _ => failed
-/
