function doesn't reduce

Stream: maths

[Jakub Kądziołka]

#eval as_fib_sum 0 prints {}, but refl doesn't see that. What gives?

import data.nat.fib.basic

open_locale big_operators
namespace nat

private def rep0 {n : ℕ} (h : n < 1) : (∅ : finset ℕ).sum fib = n := sorry

def as_fib_sum_aux : Π (n i : ℕ), n < fib i.succ → { S : finset ℕ // S.sum fib = n }
| n 0 h := ⟨∅, rep0 h⟩
| n 1 h := ⟨∅, rep0 h⟩
| n (i + 2) h := if Hcmp : fib (i + 2) ≤ n then
    have h' : n - fib (i + 2) < fib i.succ := sorry,
    let ⟨S, _⟩ := as_fib_sum_aux (n - fib (i + 2)) i h' in
    ⟨insert (i + 2) S, sorry⟩
  else
    as_fib_sum_aux n (i + 1) (lt_of_not_ge' Hcmp)

lemma fib_between (n : ℕ) : ∃ k : ℕ, fib k ≤ n ∧ n < fib k.succ := sorry

def as_fib_sum (n : ℕ) : { S : finset ℕ // S.sum fib = n } :=
  as_fib_sum_aux n (nat.find (fib_between n)) (nat.find_spec (fib_between n)).elim_right

example : (as_fib_sum 0).val = ∅ := rfl

end nat

[Jakub Kądziołka]

Looks like the problem is with nat.find, which uses well-founded recursion. How do I force Lean to evaluate that?

[Eric Wieser]

Do you need rfl to work?

[Eric Wieser]

Lean will have generated an equation lemma for you that proves that statement

[Kyle Miller]

lemma find_fib_between_0 : nat.find (fib_between 0) = 0 :=
begin
  rw ← nonpos_iff_eq_zero,
  apply nat.find_min',
  simp,
end

example : (as_fib_sum 0).val = ∅ := begin
  unfold as_fib_sum as_fib_sum_aux,
  simp_rw [find_fib_between_0],
  refl,
end

[Kyle Miller]

#eval isn't a predictor of what refl can do, since it's evaluating things by a completely different mechanism (the untrusted VM interpreter). Closer would be #reduce as_fib_sum 0, which gives a pretty big term full of things like acc.rec.

[Jakub Kądziołka]

Would it be possible to modify norm_num or something to teach it how to compute nat.find? If so, any pointers on how to go about doing that?

[Kyle Miller]

This might be enough:

@[simp]
lemma nat.find_true {p : ℕ → Prop} [decidable_pred p] (h : ∃ n, p n)
  (hp : p 0) :
  nat.find h = 0 :=
by simp [hp]

@[simp]
lemma nat.find_false {p : ℕ → Prop} [decidable_pred p] (h : ∃ n, p n)
  (hp : ¬ p 0) :
  nat.find h =
  (nat.find (begin obtain ⟨n, hn⟩ := h, obtain _|_ := n, contradiction, exact ⟨_, hn⟩, end : ∃ n, p (n + 1))) + 1 :=
by rw find_comp_succ h _ hp

example : (as_fib_sum 0).val = ∅ := by norm_num [as_fib_sum, as_fib_sum_aux]

[Kyle Miller]

It depends on simp/norm_num being able to evaluate the predicate, though.

[Kyle Miller]

It gets stuck at the next case:

example (s : finset ℕ) : (as_fib_sum 1).val = s :=
begin
  norm_num [as_fib_sum, as_fib_sum_aux],
  generalize_proofs a b,
  generalize_proofs at b,
/-
a : ∃ (n : ℕ), fib (n + 1 + 1) ≤ 1 ∧ 1 < fib (n + 1 + 1).succ,
b : 1 - fib (nat.find a + 2) < fib (nat.find a).succ
⊢ ↑(dite (fib (nat.find a + 2) ≤ 1)
         (λ (Hcmp : fib (nat.find a + 2) ≤ 1),
            as_fib_sum_aux._match_1 1 (nat.find a) ((1 - fib (nat.find a + 2)).as_fib_sum_aux (nat.find a) b))
         (λ (Hcmp : ¬fib (nat.find a + 2) ≤ 1), 1.as_fib_sum_aux (nat.find a).succ _)) =
    s
-/
end

(The s is a trick to use norm_num when you don't know what it is supposed to equal.)