Skip to content

Instantly share code, notes, and snippets.

@ChrisHughes24
Created July 10, 2020 10:45
Show Gist options
  • Save ChrisHughes24/84ffdb76b8009134a9f42e7a08a92ac5 to your computer and use it in GitHub Desktop.
Save ChrisHughes24/84ffdb76b8009134a9f42e7a08a92ac5 to your computer and use it in GitHub Desktop.
import data.nat.digits
lemma nat.div_lt_of_le : ∀ {n m k : ℕ} (h0 : n > 0) (h1 : m > 1) (hkn : k ≤ n), k / m < n
| 0 m k h0 h1 hkn := absurd h0 dec_trivial
| 1 m 0 h0 h1 hkn := by rwa nat.zero_div
| 1 m 1 h0 h1 hkn :=
have ¬ (0 < m ∧ m ≤ 1), from λ h, absurd (@lt_of_lt_of_le ℕ
(show preorder ℕ, from @partial_order.to_preorder ℕ (@linear_order.to_partial_order ℕ nat.linear_order))
_ _ _ h1 h.2) dec_trivial,
by rw [nat.div_def_aux, dif_neg this]; exact dec_trivial
| 1 m (k+2) h0 h1 hkn := absurd hkn dec_trivial
| (n+2) m k h0 h1 hkn := begin
rw [nat.div_def_aux],
cases decidable.em (0 < m ∧ m ≤ k) with h h,
{ rw [dif_pos h],
refine nat.succ_lt_succ _,
refine nat.div_lt_of_le (nat.succ_pos _) h1 _,
cases m with m,
{ exact absurd h.1 dec_trivial },
{ cases m with m,
{ exact absurd h1 dec_trivial },
{ clear h1 h,
induction m with m ih,
{ cases k with k,
{ exact nat.zero_le _ },
{ cases k with k,
{ exact nat.zero_le _ },
{ rw [nat.sub_succ, nat.sub_succ, nat.sub_zero, nat.pred_succ,
nat.pred_succ],
exact @linear_order.le_trans ℕ nat.linear_order _ _ _
(nat.le_succ k) (nat.le_of_succ_le_succ hkn) } } },
{ cases k with k,
{ rw [nat.zero_sub], exact nat.zero_le _ },
{ rw [nat.succ_sub_succ],
refine @linear_order.le_trans ℕ nat.linear_order _ _ _ _ ih,
refine nat.sub_le_sub_right _ _,
exact nat.le_succ _ } } } } },
{ rw dif_neg h,
exact nat.succ_pos _ }
end
lemma nat.div_lt_self'' {n m : ℕ} (h0 : n > 0) (hm : m > 1) : n / m < n :=
nat.div_lt_of_le h0 hm (le_refl _)
def f : ℕ → ℕ
| n :=
if h : 0 < n
then have n - 1 < n, from nat.sub_lt h zero_lt_one,
f (n - 1)
else 0
def digits_aux' (b : ℕ) (h : 2 ≤ b) : ℕ → list ℕ
| 0 := []
| (n+1) :=
have (n+1)/b < n+1 := nat.div_lt_self'' (nat.succ_pos _) h,
(n+1) % b :: digits_aux' ((n+1)/b)
def digits' : ℕ → ℕ → list ℕ
| 0 := digits_aux_0
| 1 := digits_aux_1
| (b+2) := digits_aux' (b+2) dec_trivial
theorem test (b n : ℕ) : digits' (b+2) (n+1) = (n+1)%(b+2) :: digits' (b+2) ((n+1)/(b+2)) := rfl -- works
theorem test' : digits' (0+2) (1+1) = (1+1)%(0+2) :: digits' (0+2) ((1+1)/(0+2)) := rfl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment