Why does using `sorry` for my lemma affect `simp` later?

Stream: new members

[Bbbbbbbbba]

When trying to make a MWE for my problem, I encountered another confusing (to me) phenomenon:

import Mathlib

def dec_lemma {b : ℕ+} {x : ℕ} : 0 < x → Nat.log b x < x ∧ 0 < x / b ^ Nat.log b x ∧ x - b ^ Nat.log b x * (x / b ^ Nat.log b x) < x := by
  intro hx
  -- exact sorry
  exact ⟨sorry, sorry, sorry⟩

def nat_to_ord (b : ℕ+) (x : ℕ) :=
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    have ⟨_, n_pos, _⟩ : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h
    ONote.oadd (nat_to_ord b e) (⟨n, n_pos⟩ : ℕ+) (nat_to_ord b (x - b ^ e * n : ℕ))
  else 0
  termination_by x

lemma nat_to_ord_cmp_lt (b : ℕ+) (hlt: x0 < x1) : (nat_to_ord b x0).cmp (nat_to_ord b x1) = Ordering.lt := by
  unfold nat_to_ord
  have h1 : 0 < x1 := Nat.zero_lt_of_lt hlt
  if h : 0 < x0 then
    let e0 := Nat.log b x0;
    let n0 := x0 / b ^ e0;
    let e1 := Nat.log b x1;
    let n1 := x1 / b ^ e1;
    have ⟨_, _, _⟩ : e0 < x0 ∧ 0 < n0 ∧ x0 - b ^ e0 * n0 < x0 := dec_lemma h
    simp [h, h1]
    simp [ONote.cmp] -- Works with "exact ⟨sorry, sorry, sorry⟩"; doesn't wotk with "exact sorry"
    sorry
  else
    sorry

[Bbbbbbbbba]

Uncommenting exact sorry and commenting exact ⟨sorry, sorry, sorry⟩ seems to change whether simp [ONote.cmp] will work.

[Kevin Buzzard]

dec_lemma seems like a proof to me. Does this weirdness still occur if you change def to theorem? In a mathlib PR a linter would stop you from pushing dec_lemma.

[Kevin Buzzard]

In general sorrying data and then changing it eg by filling in the sorrys can cause proofs to break, and I'm wondering if this is an edge case of that.

[Bbbbbbbbba]

Oh right I shouldn't have used def. But after changing it to lemma, the simp [ONote.cmp] never works :upside_down:

[Bbbbbbbbba]

I guess the problem is how I deconstructed the output of dec_lemma to get n_pos, since this works the way I want:

import Mathlib

theorem dec_lemma {b : ℕ+} {x : ℕ} : 0 < x → Nat.log b x < x ∧ 0 < x / b ^ Nat.log b x ∧ x - b ^ Nat.log b x * (x / b ^ Nat.log b x) < x := sorry

def nat_to_ord (b : ℕ+) (x : ℕ) :=
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    have hh : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h
    ONote.oadd (nat_to_ord b e) (⟨n, hh.right.left⟩ : ℕ+) (nat_to_ord b (x - b ^ e * n : ℕ))
  else 0
  termination_by x
  decreasing_by repeat sorry

lemma nat_to_ord_cmp_lt (b : ℕ+) (hlt: x0 < x1) : (nat_to_ord b x0).cmp (nat_to_ord b x1) = Ordering.lt := by
  unfold nat_to_ord
  have h1 : 0 < x1 := Nat.zero_lt_of_lt hlt
  if h : 0 < x0 then
    let e0 := Nat.log b x0;
    let n0 := x0 / b ^ e0;
    let e1 := Nat.log b x1;
    let n1 := x1 / b ^ e1;
    have ⟨_, _, _⟩ : e0 < x0 ∧ 0 < n0 ∧ x0 - b ^ e0 * n0 < x0 := dec_lemma h
    simp [h, h1]
    simp [ONote.cmp] -- Works with "exact ⟨sorry, sorry, sorry⟩"; doesn't wotk with "exact sorry"
    sorry
  else
    sorry

[Kevin Buzzard]

I would be interested to know whether filling in the sorry in the theorem makes any difference to the phenomenon of behaviour changing when you switch from def to lemma (but probably those who know how lean actually works might instantly know the answer to this question)

[Bbbbbbbbba]

Filling in everything (ending with exact ⟨h1, h2, h3⟩) behaves just like exact ⟨sorry, sorry, sorry⟩ does, and I have a guess why

[Bbbbbbbbba]

My guess is that have ⟨_, n_pos, _⟩ : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h is pattern matching, and when doing the matching, definitions are expanded but not lemmas

[Bbbbbbbbba]

If dec_lemma h is not expanded or is expanded into sorry, the pattern matching doesn't work and the whole matching expression is returned, which messes up simp