Strictly increasing finite sequence

Stream: new members

[Way Yan Win]

Given a term f : fin n → ℕ, how do I formalise the notion that f is strictly increasing? I tried something of the form ∀ k, k < n → ..., but I have trouble converting k into a term of type fin n.

[Patrick Johnson]

def strictly_increasing {n : ℕ} (f : fin n → ℕ) : Prop :=
∀ {k₁ k₂ : ℕ} {h₁ : k₁ < n} {h₂ : k₂ < n},
k₁ < k₂ → f ⟨k₁, h₁⟩ < f ⟨k₂, h₂⟩

Untested, since it wasn't a #mwe

[Way Yan Win]

ah right that works, thanks

[Scott Morrison]

That's very cumbersome in a few ways! First, no need to quantify over natural numbers: fin n itself already has a < operation. Perhaps look at mathlib's existing docs#order_embedding.

[Scott Morrison]

Or just docs#strict_mono.

[Scott Morrison]

But if you want to "do it yourself"

def strictly_increasing {n : ℕ} (f : fin n → ℕ) : Prop :=
∀ k₁ k₂, k₁ < k₂ → f k₁ < f k₂

should be all you need.

[Way Yan Win]

Ah that's useful to know. Let me elaborate on my original question though. The condition I'm formalising is actually stronger than strictly increasing: namely f k.succ > f k + 1 for all k. What would be the idiomatic way to write this?

[Yaël Dillies]

Why not write it like that? The only thing you need to know about fin addition is that it's circling around (and we might at some point make it saturating instead), so in your case you must avoid n - 1 + 1 = 0.

example {k : fin n} (hk : k < n - 1) : f k + 1 < f (k + 1) :=

[Way Yan Win]

I tried your example, but Lean gives a

failed to synthesize type class instance for
n : ℕ,
x : fin n
⊢ has_one (fin n)

I'm aware that the error goes away if I replace fin n with fin n.succ, but is there a better way to go about it?

[Johan Commelin]

You somehow need to write down a definition that works for fin 0 (which is empty).

[Johan Commelin]

Doing this in a unified way seems not so straightforward

[Johan Commelin]

@Yaël Dillies Does fin n already have a succ : fin n → fin n?

[Way Yan Win]

Johan Commelin said:

You somehow need to write down a definition that works for fin 0 (which is empty).

Ah I think I'll try this out then

[Yaël Dillies]

No idea, but there's no succ_order instance at least.

[Reid Barton]

You could use Scott's definition but add + 1 to the right hand side, since that's equivalent to what you want

[Reid Barton]

I wouldn't recommend using + on fin.

[Way Yan Win]

Hopefully it's ok for me to post this since it's a continuation of the previous question.
What I'm trying to do is to prove Zeckendorf's theorem, and here's the code I have so far:

import data.nat.fib
import algebra.big_operators.basic
open_locale big_operators

def is_zeckendorf_rep {k : ℕ} (kpos : k > 0) (f : fin k → ℕ) : Prop :=
  f ⟨0, kpos⟩ > 1 ∧ ∀ m n, m > n → f m > f n + 1

def has_zeckendorf_rep (n : ℕ) : Prop :=
  ∃ (k : ℕ) (kpos : k > 0) (f : fin k → ℕ),
    is_zeckendorf_rep kpos f ∧ ∑ (i : fin k), nat.fib (f i) = n

theorem zeckendorf_existence (n : ℕ) : n = 0 ∨ has_zeckendorf_rep n :=
begin
  apply nat.strong_induction_on,
  sorry
end

[Way Yan Win]

But on the line with apply nat.strong_induction_on, Lean throws a

invalid apply tactic, failed to unify
  n = 0 ∨ has_zeckendorf_rep n
with
  ?m_1 ?m_2

[Way Yan Win]

This puzzles me, because there was no error when I removed the disjunction. So how do I get Lean to recognise the disjunction as a single proposition?

[Way Yan Win]

I could move the n = 0 condition into has_zeckendorf_rep, but I find that to be a hacky solution.

[Kevin Buzzard]

Lean can't guess what you're inducting on. apply nat.strong_induction_on n works.

[Way Yan Win]

Ah I see, thanks

[Way Yan Win]

I finally managed to formalise the existence part of Zeckendorf's theorem, so I thought I'd share here. I still don't know much about Lean so the proof is probably quite inefficient...

import data.nat.fib
import data.fin.tuple
import data.fintype.card
import algebra.big_operators.basic
import algebra.big_operators.order
open_locale big_operators
open classical nat
local attribute [instance] prop_decidable

def is_zeckendorf_rep {k : ℕ} (kpos : k > 0) (f : fin k → ℕ) : Prop :=
  f ⟨0, kpos⟩ > 1 ∧ ∀ m n, m > n → f m > f n + 1

def has_zeckendorf_rep (n : ℕ) :=
  ∃ (k : ℕ) (kpos : k > 0) (f : fin k → ℕ),
    is_zeckendorf_rep kpos f ∧ ∑ (i : fin k), fib (f i) = n

lemma trivial_rep_is_zeckendorf (f : fin 1 → ℕ) (h : f ⟨0, by norm_num⟩ > 1) :
  is_zeckendorf_rep (by norm_num) f :=
begin
  split,
  { assumption },
  { intros m n hmn,
    exfalso,
    have hm0 : m = 0 := fin.eq_zero m,
    have hn0 : n = 0 := fin.eq_zero n,
    subst hn0,
    exact (ne_of_gt hmn) hm0 }
end

lemma fib_three : fib 3 = 2 := begin
  rw fib_succ_succ, ring
end

lemma eq_last_of_not_lt {k : ℕ} {m : fin k.succ} (h : ¬↑m < k) : ↑m = k :=
  le_antisymm (fin.is_le m) (le_of_not_gt h)

lemma fib_inv_strict_mono {m n : ℕ} (h : fib m < fib n) : m < n :=
begin
  by_contra h1, exact not_lt.mpr (fib_mono (not_lt.mp h1)) h,
end

theorem zeckendorf_existence (n : ℕ) : n = 0 ∨ has_zeckendorf_rep n :=
begin
  apply nat.strong_induction_on n,
  clear n,
  intros n hm,

  -- Trivial cases
  by_cases n_eq_0 : n = 0,
    left, assumption,

  by_cases n_eq_1 : n = 1,
  { right,
    use [1, by norm_num, (λ i, 2)], -- 1 = fib 2
    split,
    { exact trivial_rep_is_zeckendorf _ (by norm_num) },
    { rw [fintype.sum_unique, n_eq_1, fib_two] } },

  by_cases n_eq_2 : n = 2,
  { right,
    use [1, by norm_num, (λ i, 3)], -- 2 = fib 3
    split,
    { exact trivial_rep_is_zeckendorf _ (by norm_num) },
    { rw [fintype.sum_unique, n_eq_2, fib_three] } },

  -- Induction step
  have n_ge_2 : n > 2,
  { refine lt_of_le_of_ne _ (ne.symm n_eq_2),
    rw nat.succ_le_iff,
    refine lt_of_le_of_ne _ (ne.symm n_eq_1),
    rw nat.succ_le_iff,
    rwa pos_iff_ne_zero },
  clear n_eq_0 n_eq_1 n_eq_2,
  right,

  set fibs := λ i, ∃ k, i = fib k with hfibs,
  -- F = fib l is the greatest Fibonacci number ≤ n
  set F := nat.find_greatest fibs n with hF,

  have two_le_F : 2 ≤ F,
  { refine nat.le_find_greatest (le_of_lt n_ge_2) _,
    use 3, rw fib_three },
  have : ∃ m, m ≤ n ∧ ∃ k, m = fib k,
    use [1, one_le_of_lt n_ge_2, 1], rw fib_one,
  have F_fib := nat.find_greatest_spec this,
  clear this,
  cases F_fib with l hl,

  have l_gt_1 : l > 1,
  { by_contra h,
    replace h := fib_mono (not_lt.mp h),
    rw [fib_one, ←hl, ←hfibs, ←hF] at h,
    replace h := not_lt.mpr h,
    exact h (succ_le_iff.mp two_le_F) },

  have nF_lt_n : n - F < n,
  { refine nat.sub_lt _ (nat.succ_le_iff.mp (le_of_succ_le two_le_F)),
    exact pos_of_gt n_ge_2 },
  have F_le_n : F ≤ n := nat.find_greatest_le,
  have hnF := hm (n - F) nF_lt_n,

  cases hnF with nF0 hnF,
  -- n = F is a Fibonacci number, thus has trivial Zeckendorf representation
  { have n_eq_F : n = F :=
      nat.le_antisymm (nat.le_of_sub_eq_zero nF0) F_le_n,
    clear nF_lt_n nF0,

    use [1, by norm_num, (λ i, l)],
    split,
    { exact trivial_rep_is_zeckendorf _ l_gt_1 },
    { rw fintype.sum_unique, rw [n_eq_F, ←hl] } },

  -- Otherwise, add F to the Zeckendorf representation of n - F
  { rcases hnF with ⟨k, kpos, f, ⟨f0, frest⟩, fsum⟩,
    use [k.succ, succ_pos k,
      λ (i : fin k.succ), if h : ↑i < k then f (i.cast_lt h) else l],
    split,
    -- This is indeed a Zeckendorf representation
    { split,
      { convert f0, dsimp, rw dif_pos, refl },
      { intros m' n' hmn',
        change n' < m' at hmn',
        dsimp,
        split_ifs with h1 h2 h3,

        -- n < m < k → use the hypothesis
        { apply frest,
          change n'.cast_lt h2 < m'.cast_lt h1,
          rwa fin.lt_iff_coe_lt_coe at ⊢ hmn' },

        -- m > n, m < k = n → contradiction
        { exfalso,
          rw fin.lt_iff_coe_lt_coe at hmn',
          have : ¬↑n' < ↑m' := nat.lt_asymm (nat.lt_of_lt_of_le h1 (not_lt.mp h2)),
          exact this hmn' },

        -- n < k = m → the interesting case
        { have ha : n-F < fib (l-1),
          { by_contra h,
            replace h := not_lt.mp h,
            rw ←nat.add_le_to_le_sub (fib (l-1)) F_le_n at h,
            rw [hF, hfibs, hl] at h,
            have l_sub_add : l-1+1 = l := nat.sub_add_cancel (le_of_lt l_gt_1),
            conv_lhs at h { congr, skip, rw ←l_sub_add },
            rw ←fib_succ_succ at h,
            change fib (l-1+1).succ ≤ n at h,
            rw (succ_inj'.mpr l_sub_add) at h,

            have contra : fib l.succ ≤ nat.find_greatest fibs n :=
              nat.le_find_greatest h (by use l.succ),
            rw [hfibs, hl, ←nat.sub_add_cancel l_gt_1] at contra,
            replace contra := not_lt_of_le contra,
            exact contra (fib_add_two_strict_mono (lt_add_one (l - 2))) },

          have hb : fib (f (n'.cast_lt h3)) < fib (l-1),
          { suffices h : fib (f (n'.cast_lt h3)) ≤ n - F,
            exact gt_of_gt_of_ge ha h,

            rw ←fsum,
            change (fib ∘ f) (n'.cast_lt h3) ≤ ∑ (i : fin k), (fib ∘ f) i,
            refine finset.single_le_sum _ _,
            { intros i hi_univ,
              change fib (f i) ≥ 0,
              exact zero_le _ },
            apply finset.mem_univ },

          replace hb := fib_inv_strict_mono hb,
          exact lt_tsub_iff_right.mp hb },

        -- m > n, m = k, n = k → contradiction
        { exfalso,
          replace h1 := eq_last_of_not_lt h1,
          replace h3 := eq_last_of_not_lt h3,
          rw fin.lt_iff_coe_lt_coe at hmn',
          rw [h1, h3] at hmn',
          exact nat.lt_asymm hmn' hmn' } } },

    -- It sums up to n
    { rw [←nat.sub_add_cancel F_le_n, ←fsum, hF, hfibs, hl],
      rw fin.sum_univ_cast_succ,
      dsimp,
      have sum_eq_of_eqs : ∀ (a b c d : ℕ), a = c → b = d → a + b = c + d,
        intros a b c d hac hbd, rw [hac, ←hbd],
      apply sum_eq_of_eqs,
      { refine fintype.sum_equiv (equiv.cast rfl) _ _ _,
        intro x, rw dif_pos, simp, apply fin.is_lt },
      { rw dif_neg, apply irrefl } } }
end

[Johan Commelin]

Congrats on finishing a non-trivial Lean proof! Enjoy the dopamine rush (-;