Why does decide fail after applying iff in this example?

Stream: lean4

[Mario Weitzer]

def f_pos_nz (f : Nat → Nat) (h : ∃ n, f n ≠ 0) := Nat.find h
def f_pos_nz' (f : Nat → Nat) (h : f ≠ 0) := Nat.find (Function.ne_iff.mp h)

example : f_pos_nz (λ n => n) ⟨1, Nat.one_ne_zero⟩ = 1 := by decide
-- Works fine.
example : f_pos_nz' (λ n => n) (Function.ne_iff.mpr ⟨1, Nat.one_ne_zero⟩) = 1 := by decide
/-
Tactic `decide` failed for proposition
  f_pos_nz' (fun n ↦ n) ⋯ = 1
because its `Decidable` instance
  instDecidableEqNat (f_pos_nz' (fun n ↦ n) ⋯) 1
did not reduce to `isTrue` or `isFalse`.

After unfolding the instances `instDecidableEqNat`, `Classical.propDecidable`, and `Nat.decEq`, reduction got stuck at the `Decidable` instance
  match h : (f_pos_nz' (fun n ↦ n) ⋯).beq 1 with
  | true => isTrue ⋯
  | false => isFalse ⋯
-/

[Ruben Van de Velde]

Looks like there's a broken instance

[Ruben Van de Velde]

Not sure what it might be though

[Eric Wieser]

Nat.find is not reducible, I think?

[Mario Weitzer]

But why does it work in one case but not the other? And how can I make it work in both cases? Is there a reducible version of Nat.find?

[Bbbbbbbbba]

Maybe it is the same reason why rfl could close this? Never mind, I guess this does not strip off any complexity...

example : f_pos_nz (λ n => n) ⟨1, Nat.one_ne_zero⟩ = 1 := by
  apply of_decide_eq_true
  -- ⊢ decide (f_pos_nz (fun n ↦ n) ⋯ = 1) = true
  rfl

[Bbbbbbbbba]

Well, this shows a difference:

example : f_pos_nz (λ n => n) ⟨1, Nat.one_ne_zero⟩ = 1 := by
  apply of_decide_eq_true
  conv => lhs; rhs; lhs; reduce  -- 1
  rfl

example : f_pos_nz' (λ n => n) (Function.ne_iff.mpr ⟨1, Nat.one_ne_zero⟩) = 1 := by
  apply of_decide_eq_true
  conv => lhs; rhs; lhs; reduce  /-
  (Acc.rec
    (fun x₁ h ih al ↦
      Decidable.rec (fun h ↦ ih x₁.succ ⋯ ⋯) (fun h ↦ ⟨x₁, ⋯⟩)
        ((fun {q} motive dq h_1 h_2 ↦ Decidable.rec (fun h ↦ h_2 h) (fun h ↦ h_1 h) dq)
          (fun dp ↦ Decidable ¬(fun n ↦ n) x₁ = 0 x₁)
          ((fun motive x h_1 h_2 ↦ Bool.rec (motive := fun x_1 ↦ x = x_1 → motive x_1) h_2 h_1 x ⋯)
            (fun x ↦ Decidable ((fun n ↦ n) x₁ = 0 x₁)) (x₁.beq Nat.zero) (fun h ↦ isTrue ⋯) fun h ↦ isFalse ⋯)
          (fun hp ↦ isFalse ⋯) fun hp ↦ isTrue hp))
    ⋯ ⋯).1
  -/
  sorry

[Bbbbbbbbba]

Silly me, I just realized that the first example could already be closed by rfl, so this is more of a defeq thing than a decide thing

[Mario Weitzer]

I see, thanks for the explanations so far. But this leaves the question on how to make Nat.find reduce in these situations. Or is there another function I could use that would work here?

[Bbbbbbbbba]

My guess would be that it needs to see an explicit witness of existence (thus an upper bound). Can you always specify one in your use case?

[Mario Weitzer]

Bbbbbbbbba said:

My guess would be that it needs to see an explicit witness of existence (thus an upper bound). Can you always specify one in your use case?

No, I can't, but I still don't get why this is an issue. If I know that f n will be nonzero eventually, why can't I tell Lean to just keep looking no matter how long it takes? I find it frustrating to convince Lean that something is decidable only to find out that it will refuse to decide anyway. Is there no way to tell Lean that it should just decide based on the fact that there is a proof of decidability?

[Edward van de Meent]

No. That wouldn't work, because docs#Classical.propDecidable is a theorem

[Edward van de Meent]

(because if what you're arguing is possible, we would be able to prove (for example) FLT by using choice to create the decidable instance, then calling by decide.)

[Bbbbbbbbba]

But it would be nice to have a tactic that tries to decide up to a limit, and fails otherwise

[Bbbbbbbbba]

Could be used for e.g. sanity check by trying to find small counterexamples

[Edward van de Meent]

What does 'tries to decide' mean? There is no general algorithm for 'trying to decide', afaik...

[Aaron Liu]

do you mean like plausible, which tries to find counterexamples

[Aaron Liu]

note that you can never prove something with plausible, you can only find counterexamples

[Edward van de Meent]

Let me emphasize that the Issue here is not with decide, it's with docs#Nat.find not reducing depending on what proof is passed

[Mario Weitzer]

Edward van de Meent said:

Let me emphasize that the Issue here is not with decide, it's with docs#Nat.find not reducing depending on what proof is passed

I understand, but how can I tell from the outset if a certain function (like Nat.find in this case) will or won't reduce and how can I force it to reduce or implement it in such a way that I can be sure it will reduce?

[Edward van de Meent]

Usually, things which aren't noncomputable reduce. There are exceptions which usually involve explicit calls to WellFounded.fix or Acc.rec, which aren't noncomputable but still might not reduce.

[Bbbbbbbbba]

Aaron Liu said:

note that you can never prove something with plausible, you can only find counterexamples

In OP's use case, they may be able to use the counterexample as an explicit existence proof so that decide goes through :thinking:

[Shubakur Mitra]

This can be decided using the method proposed in https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Proofs.20by.20computation/near/556707383

Eval.lean

import Mathlib

variable {α β γ : Type*}

class Eval (x : α) (y : outParam α) : Prop where
  eq : x = y

@[simp] def C := @id
@[simp] def D := @id

theorem evalC {x y : α} [H : Eval (C x) y] : C x = y := H.eq
theorem evalD {x y : α} [H : Eval (D x) y] : D x = y := H.eq

open Classical in @[simp] noncomputable
def ite' (p : Prop) (x y : α) : α :=
  if p then x else y

open Classical in noncomputable
def find' (p : ℕ → Prop) (n : ℕ) : ℕ :=
  if h : ∃ k, n ≤ k ∧ p k then Nat.find h else 0

@[simp]
theorem eval_iff {x y : α} : Eval x y ↔ x = y :=
  ⟨λ h => h.1, λ h => ⟨h⟩⟩

instance : Eval (D True) True := ⟨rfl⟩
instance : Eval (D False) False := ⟨rfl⟩
instance : Eval (D ¬True) False := by simp
instance : Eval (D ¬False) True := by simp

instance {p : Prop} [Decidable p] {x y : α} :
  Eval (C $ if p then x else y) (C $ ite' p x y) := by simp [ite']
instance {x y : α} {p : Prop} : Eval (C $ ite' p x y) (C $ D $ ite' (C p) x y) := ⟨rfl⟩
instance {x y : α} : Eval (D $ ite' True x y) x := by simp
instance {x y : α} : Eval (D $ ite' False x y) y := by simp
instance : Eval (C (0 : ℕ)) 0 := ⟨rfl⟩
instance {n : ℕ} : Eval (C ofNat(n + 1)) n.succ := ⟨rfl⟩
instance {n m : ℕ} : Eval (C $ n = m) (D $ C n = C m) := ⟨rfl⟩
instance : Eval (D $ 0 = 0) True := ⟨by simp⟩
instance {n : ℕ} : Eval (D $ 0 = n.succ) False := ⟨by simp⟩
instance {n : ℕ} : Eval (D $ n.succ = 0) False := ⟨by simp⟩
instance {n m : ℕ} : Eval (D $ n.succ = m.succ) (D $ n = m) := ⟨by simp⟩
instance {n m : ℕ} : Eval (C $ n + m) (D $ C n + C m) := ⟨rfl⟩
instance {n : ℕ} : Eval (D $ n + 0) n := ⟨rfl⟩
instance {n m : ℕ} : Eval (D $ n + ofNat(m + 1)) (D $ n + m).succ := ⟨rfl⟩
instance {p : Prop} : Eval (C ¬p) (D ¬C p) := ⟨rfl⟩
instance {x : α} : Eval (C $ (0 : α → ℕ) x) (C 0) := ⟨rfl⟩

attribute [simp] instOfNatNat
instance {n : ℕ} : Eval (D $ 0 = ofNat(n + 1)) False := ⟨by simp⟩
instance {n : ℕ} : Eval (D $ ofNat(n + 1) = 0) False := ⟨by simp⟩
instance {n m : ℕ} : Eval (D $ ofNat(n + 1) = ofNat(m + 1)) (D $ n = m) := ⟨by simp⟩
instance {n m : ℕ} : Eval (C $ n < m) (D $ C n < C m) := ⟨by simp⟩
instance {n : ℕ} : Eval (D $ n < 0) False := ⟨by simp⟩
instance {n : ℕ} : Eval (D $ 0 < n.succ) True := ⟨by simp⟩
instance {n m : ℕ} : Eval (D $ n.succ < m.succ) (D $ n < m) := ⟨by simp⟩
instance {n : ℕ} : Eval (D $ 0 < ofNat(n + 1)) True := ⟨by simp⟩
instance {n m : ℕ} : Eval (D $ ofNat(n + 1) < ofNat(m + 1)) (D $ n < m) := ⟨by simp⟩
attribute [-simp] instOfNatNat

instance {p : ℕ → Prop} [hp : DecidablePred p] {h : ∃ n, p n} :
  Eval (C $ Nat.find h) (C $ find' p 0) := by constructor; simp [find']; grind

instance {p : ℕ → Prop} {n} : Eval (C $ find' p n) $ C $ ite' (p n) n $ find' p n.succ := by
  classical
  simp; split_ifs with h₁
  · rw [find', dif_pos, Nat.find_eq_iff] <;> grind
  · rw [find']; split_ifs with h₂ <;> rw [find']
    · rw [dif_pos]; congr; all_goals grind
    · rw [dif_neg $ by grind]

attribute [-simp] C D

import Eval

def f_pos_nz' (f : Nat → Nat) (h : f ≠ 0) := Nat.find (Function.ne_iff.mp h)

example : f_pos_nz' (λ n => n) (Function.ne_iff.mpr ⟨1, Nat.one_ne_zero⟩) = 1 := by
  change C _; simp only [f_pos_nz', evalC, evalD]