Playing with Decidable

Stream: new members

[Adam Langley]

(I hope somewhat silly questions are ok here—if I'm off topic please just say!)

I wanted to play around with Lean to contrast with Coq (which I also don't really know). As an experiment, I tried to define a Decidable instance for propositions ∀ (x : Fin 256), f x)—since the domain of Fin is finite, one can just do proof by computation. With some sorry'ing of things that I think I could prove, that seems doable (https://pastebin.com/raw/ixKU7J31). Then I define a couple of test predicates and their DecideablePred instances and #eval decide (∀ (x : Fin 256), test_p_true x) says true, which sounds promising. But then using by decide fails(*) and apply of_decide_eq_true ; rfl seems to hang Lean (or at least VS Code). Trying to #eval around with Decidable.rec only says failed to elaborate eliminator, expected type is not available.

Have I done something dumb? Perhaps I need to fill out all the sorrys when needing to evaluate an expression rather than just inhabit a Prop?

(*) failed to reduce to 'true': Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h) instDecidableForAllFinOfNatNatInstOfNatNat

[Mario Carneiro]

Here's a version that seems to perform fairly well:

def all (f : Fin n → Bool) : ∀ i, i ≤ n → Bool
  | 0, _ => true
  | i+1, h => f ⟨i, h⟩ && all f i (Nat.le_of_lt h)

theorem all_iff (f : Fin n → Prop) [DecidablePred f] :
    all (f ·) n (Nat.le_refl _) ↔ (∀ (x : Fin n), f x) := sorry

instance (f : Fin n → Prop) [DecidablePred f] : Decidable (∀ (x : Fin n), f x) :=
  decidable_of_decidable_of_iff (all_iff f)

def test_p_true : Fin 256 -> Prop
| x => x = x

def test_p_false : Fin 256 -> Prop
| x => x = 42

instance : DecidablePred test_p_true := by intro x; unfold test_p_true; apply decEq
instance : DecidablePred test_p_false := by intro x; unfold test_p_false; apply decEq

#eval (inferInstance : Decidable ((∀ (x : Fin 256), test_p_true x) ))
#eval decide (∀ (x : Fin 256), test_p_true x)

[Adam Langley]

Gosh, decidable_of_decidable_of_iff does indeed work much better than my mess! Thank you!

example : ∀ (x : Fin 256), test_p_true x := by decide still fails, however. Although apply of_decide_eq_true ; rfl _does_ work.

[Mario Carneiro]

Oh, that's interesting. I guess it's because this is a fairly linear computation it's blowing the stack. The recommended suggestion of set_option maxRecDepth 1000 does seem to work

[Eric Wieser]

Does writing this in a tail-recursive way help at all? Or does lean 4 only handle that in the VM / not optimize it at all?

[Mario Carneiro]

Note that we don't usually use kernel computation like this in lean, unlike coq which leans heavily on it. The preferred way is to construct a proof term

[Mario Carneiro]

I was thinking about that, but the tail recursion of interest would be in the kernel whnf computation

[Adam Langley]

Ah, I hadn't considered that the default depth limit might legitimately be too small but it's in the prelude, and it's only 512.

[Mario Carneiro]

There isn't really any room for "optimization" when it comes to kernel computation, that would entail replacing the expr by a different one

[Mario Carneiro]

and it's not obvious how to do that without changing defeqs

[Eric Wieser]

Could the kernel not unify for tall-recursive cases in an order that requires constant rather than linear stack space?

[Mario Carneiro]

it's a reasonable question. I don't know that much about how it unfolds specifically seeing as it has basically been untouched for as long as I have been around

[Eric Wieser]

I'm sure you know more than me

[Eric Wieser]

I suppose even if it did use constant space, maxDepth could end up counting the syntactic recursion

[Mario Carneiro]

Actually, I recall gabriel mentioning that there is a way to get whnf to evaluate one step at a time; I want to make a user command to display the evaluation sequence now

[Mario Carneiro]

although that's the elaborator and not the kernel so there could be some discrepancies

[Mario Carneiro]

Actually, this kind of works:

import Lean
open Lean Meta Elab

def whnf1 (e : Expr) : MetaM Expr :=
  whnfEasyCases e fun e => do
    let e' ← whnfCore e
    if let some v ← reduceNat? e' then return v
    if let some v ← reduceNative? e' then return v
    if let some v ← unfoldDefinition? e' then return v
    return e'

elab tk:"#whnf_seq" e:term depth:((":" num)?) : command => do
  Command.runTermElabM fun _ => do
    let mut e ← Elab.Term.elabTermAndSynthesize e none
    let depth := depth.raw[1].isNatLit?.getD 1000
    let mut msg := m!""
    for _ in [:depth] do
      msg := msg ++ m!"• {MessageData.nest 2 e}\n"
      let e' ← whnf1 e
      if e' == e then logInfoAt tk msg; return
      e := e'
    logInfoAt tk (msg ++ "...")

[Mario Carneiro]

#whnf_seq all (test_p_true ·) 3 (by decide)

• all (fun x => decide (test_p_true x)) 3 (_ : 3 ≤ 256)
• (fun x => decide (test_p_true x)) { val := 2, isLt := (_ : 3 ≤ 256) } &&
    all (fun x => decide (test_p_true x)) 2 (_ : 2 ≤ 256)
• match (fun x => decide (test_p_true x)) { val := 2, isLt := (_ : 3 ≤ 256) } with
  | false => false
  | true => all (fun x => decide (test_p_true x)) 2 (_ : 2 ≤ 256)
• (fun x => decide (test_p_true x)) { val := 1, isLt := (_ : 2 ≤ 256) } &&
    all (fun x => decide (test_p_true x)) 1 (_ : 1 ≤ 256)
• match (fun x => decide (test_p_true x)) { val := 1, isLt := (_ : 2 ≤ 256) } with
  | false => false
  | true => all (fun x => decide (test_p_true x)) 1 (_ : 1 ≤ 256)
• (fun x => decide (test_p_true x)) { val := 0, isLt := (_ : 1 ≤ 256) } &&
    all (fun x => decide (test_p_true x)) 0 (_ : 0 ≤ 256)
• match (fun x => decide (test_p_true x)) { val := 0, isLt := (_ : 1 ≤ 256) } with
  | false => false
  | true => all (fun x => decide (test_p_true x)) 0 (_ : 0 ≤ 256)
• true

[Mario Carneiro]

This one doesn't though, it seems to do the whole subcomputation in one step:

#whnf_seq decide (all (test_p_true ·) 3 (by decide))

• decide (all (fun x => decide (test_p_true x)) 3 (_ : 3 ≤ 256) = true)
• Decidable.casesOn (instDecidableEqBool (all (fun x => decide (test_p_true x)) 3 (_ : 3 ≤ 256)) true) (fun x => false)
    fun x => true
• true

[Adam Langley]

I did manage to reproduce the original issue, even with the better code. Changing the valid test function from x = x to x &&& 1 < 2 causes the by decide to fail again with

failed to reduce to 'true'
  Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h)
    (instDecidableForAllFin fun x => test_p_true x)

... even though the evals are both still happy.

Here's the tweaked, failing code:

def all (f : Fin n → Bool) : ∀ i, i ≤ n → Bool
  | 0, _ => true
  | i+1, h => f ⟨i, h⟩ && all f i (Nat.le_of_lt h)

theorem all_iff (f : Fin n → Prop) [DecidablePred f] :
    all (f ·) n (Nat.le_refl _) ↔ (∀ (x : Fin n), f x) := sorry

instance (f : Fin n → Prop) [DecidablePred f] : Decidable (∀ (x : Fin n), f x) :=
  decidable_of_decidable_of_iff (all_iff f)

def test_p_true : Fin 256 -> Prop
| x => x &&& 1 < 2

instance : DecidablePred test_p_true := by intro x; unfold test_p_true; apply Nat.decLt

#eval (inferInstance : Decidable ((∀ (x : Fin 256), test_p_true x) ))
#eval decide (∀ (x : Fin 256), test_p_true x)

example : ∀ (x : Fin 256), test_p_true x := by decide

[Adam Langley]

x &&& 0 < 2 is happy though.

[Mario Carneiro]

&&& is bitwise and, you don't need it for Bool

[Adam Langley]

Indeed, but x &&& 1 < 2 is _true_ for all Fin 256 though (just as a dummy example). I had expected that if decide returns true then by decide would produce a proof.

[Mario Carneiro]

I'm guessing that it's just too expensive to compute this in the kernel currently. If you use #reduce instead of #eval (which is what this code amounts to), it hits both the maxRecDepth limit and the maxHeartbeats limit

[Mario Carneiro]

by decide doesn't produce a proof, it just asserts that the statement is true and the kernel has to work out why

[Mario Carneiro]

and the kernel isn't particularly good at that job, comparatively

[Adam Langley]

Ah, I see. Thanks!

[Mario Carneiro]

using by native_decide uses #eval instead, which scales much better but is also "cheating" in some sense

[Adam Langley]

native_decide brings a lot more into the set of trusted code, I assume?

[Mario Carneiro]

quite so

[Mario Carneiro]

The tools for doing this with proofs are still under construction in mathlib4 but hopefully we will have something soon that can do this

[Adam Langley]

It was fun to play around with, thank you!