where to read about `decide`

Stream: new members

[rzeta0]

I can't seem to find any online intro / guide to decide.

I'd welcome pointers.

(or if it is truly simple to understand, perhaps a paragraph here might suffice?)

[Niels Voss]

https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#decidable-propositions

[Kyle Miller]

Here's the basic level:

Thanks to Gödel, we know that there is no algorithm that can, in general, decide whether or not any given proposition is true (in the sense of finding a proof). However, this does not mean that every proposition is undecidable. For example, 1 < 100 is decidable, since there is an algorithm that can evaluate natural number inequalities.

Lean has a system to create a patchwork of decision algorithms, using the Decidable typeclass. People can define Decidable "instances" that extend the bounds of what is decidable.

The decide tactic makes use of these instances to try to resolve goals. Given the goal, it tries to create a decision algorithm using the available instances. This might immediately fail with a "failed to synthesize Decidable ..." error, meaning there is no algorithm known to Lean. Then it evaluates the procedure, and there are three options: succeeds with true, fails with false, or indeterminate. In the success case, the goal is closed, in the failure case the tactic tells you the goal is actually false, and in the indeterminate case, the procedure was too complicated for Lean to evaluate (or it's fundamentally non-computable; this can happen if decide is used inside the classical tactic).

[Kyle Miller]

There is no clear definition for when decide succeeds or fails.

I think, basically, if you think it might work, it doesn't hurt trying it. If it doesn't work and you think it should, then (1) maybe the instance you need is in some un-imported module, (2) maybe the instance you need hasn't been written yet, or (3) maybe the goal is too complex to ever expect decide to be able to handle it.

[rzeta0]

@Kyle Miller thanks - this is helpful.

Is exhaust a simpler form of decide which only applies to propositions with no variables?

[Kyle Miller]

You remind me of one last point about decide that I didn't mention:

The decide prefers not having any variables in the goal (though variables defined with let are OK). It will give you an error if there are any. (The rough reason why is that there are two things decide could try to do: symbolically evaluate the algorithm, or universally quantify the variable. Not only are there two options, but both can be unexpectedly expensive, so decide decides 'no'.)

If you do want to work with goals that have variables, the decide +revert option causes the variables to become universally quantified. It's like it does revert with all the variables that currently appear in the goal.

[Kyle Miller]

Is exhaust a simpler form of decide which only applies to propositions with no variables?

A number of tactics tend to be custom decision algorithms for some sub-area of mathematics or logic. For example, tauto can decide anything that is purely propositional logic.

The decide tactic is actually a very simple tactic (so long as you are comfortable with Lean's typeclass system). It makes no promises to be able to decide anything in particular, just whatever is "plugged-in" via the Decidable instances. (Just to re-emphasize a point: decide is user-extensible by anyone who is comfortable writing instances.)

exhaust is significantly more complicated tactic than decide. It makes use of duper to resolve goals involving equalities and propositions. (That's my understanding; I've never used exhaust, which is a MoP tactic, and unfortunately I haven't used duper yet.) Note that it does allow variables, just no quantifiers:

example {x : Nat} (h1 : x = 0 ∨ x = 1) (h2 : x = 0 ∨ x = 2) : x = 0 := by exhaust

It's a "saturation-based automated theorem prover", and it's not comparable to decide. I'm sure there are things each can do that the other cannot.

[Kyle Miller]

Example: It's possible to configure decide to prove tautologies by evaluating the entire truth table.

The goal is to get this to work:

example (p q r : Prop) : (p → q) ∧ (q → r) → (p → r) := by
  decide +revert

The effect of +revert is that the goal decide will try to prove is ∀ (p q r : Prop), (p → q) ∧ (q → r) → (p → r).

The only thing we need to do is "teach" decide how to prove statements that are universally quantified over propositions.

Strategy: To prove above forall, if we can evaluate the truth of both ∀ (q r : Prop), (True → q) ∧ (q → r) → (True → r) and ∀ (q r : Prop), (False → q) ∧ (q → r) → (False → r), then we can evaluate the truth of ∀ (p q r : Prop), (p → q) ∧ (q → r) → (p → r). (And we do this recursively to with q and r.)

To do this, we can define a Decidable instance that does the job. I won't walk you through the details. The point is that it is possible to do.

instance (Q : Prop → Prop) [Decidable (Q True)] [Decidable (Q False)] :
    Decidable (∀ p : Prop, Q p) :=
  if h : Q True ∧ Q False then
    isTrue <| by
      intro p
      by_cases hp : p
      · rw [← eq_true hp] at h
        exact h.1
      · rw [← eq_false hp] at h
        exact h.2
  else
    isFalse <| by
      rw [not_and_or] at h
      push_neg
      obtain h | h := h
      · exact ⟨True, h⟩
      · exact ⟨False, h⟩

With this block of code placed before the example, you can observe that decide +revert does indeed prove the tautology.

[rzeta0]

thanks again - I will need to re-read this last comment a few time for it to sink in.

[Rado Kirov]

I am also getting my head around this, and I feel the confusion comes from the word "decidable" conflating two distinctly different things - 1) abstractly something in logic (or computability theory) 2) something more specific in Lean that has to do with the Decidable typeclass.

For example, 1 < 100 is decidable

This is a clear statement of abstract logic. But in Lean we can prove it by norm_num, linarith, simp and decide. AFAIKT, decide is the most generic tactic that uses type classes to "plug in" specific implementations. simp is also pluggable but through a different mechanism [@simp] which is confusing and norm_num and linarith are not.

What I am missing is why aren't all statements that are known to be decidable (in theory) proved in Lean by using decide tactic - is it for performance or style?

[Ruben Van de Velde]

Performance can definitely be an issue, yeah

[Kyle Miller]

Maybe reflect could be a better name for the tactic. What it does is it takes a Prop and uses the Decidable to turn it into (essentially) a Bool (a process known as "reflection"). It then reduces that boolean, and, if it gets true, it's able to extract a proof of the original proposition.

This depends on

• Can typeclass inference match the Props involved to create a Decidable instance?
• Can these Decidable instances be robust enough that propositions will be reliably matched?
• Is the algorithm it synthesizes good enough to be evaluated using term reduction?

Tactics in particular domains can often come up with much better algorithms. They can run native code to calculate some details about a situation and then choose an efficient proof after the fact too.

A tactic like ring can be implemented using decide-like reflection (it's not currently), but implementing it using the typeclass system is probably too much to expect, and, if it's even possible, likely to be very fragile.

Rado Kirov said:

For example, 1 < 100 is decidable

This is a clear statement of abstract logic

In particular I mean that it's decidable in the sense that for all concrete naturals n and m, we can calculate n < m by reducing Nat.blt n m to (hopefully) true, and using this result to justify that n < m. (Another way it could be implemented is to calculate 100 - 1 and see that it is not 0.)

Rado Kirov said:

simp is also pluggable but through a different mechanism [@simp] which is confusing and norm_num and linarith are not.

What are you finding confusing about @[simp]? The tactic uses a giant database of rewrite rules, and when you annotate a lemma with @[simp] it adds the rule to that database.

Note that you can write norm_num plugins to get norm_num to be able to evaluate new functions. These are programs that generate a value and a proof that the original expression evaluates to this value.

[Rado Kirov]

What are you finding confusing about @[simp]? The tactic uses a giant database of rewrite rules, and when you annotate a lemma with @[simp] it adds the rule to that database.

I am confused why there are two "extensibility mechanisms" for making powerful tactics - type classes and annotations and what are the tradeoffs. Two powerful tactics - decide and simp use each. And I mean confusing for newcomers like me, likely it will become clear as I learn more.

[Kyle Miller]

@Rado Kirov It's all annotations ("attributes") in the end. Instances are definitions with the @[instance] attribute.

The decide tactic is pretty much the only tactic that use instances in such a direct way. It's a very imperfect tactic too. It's nice that it can reuse the typeclass system, but it also means it's limited by the way the typeclass system works. Maybe a future decide won't use instances so directly, letting people plug in more powerful decision procedures.

[Rado Kirov]

I see, thanks for elaborating. Lean's type system is basically the fanciest type system I have seen, so surprising to see that it is still limiting in some ways, but the more I think of it it makes sense, at some point you don't want to go through the type class dispatch and just take 1 < 100 and run a custom procedure.

[Kyle Miller]

Decidable also has the limitation that it's not appropriate for problems that are semidecidable. For example, ring can prove ring equalities, but it can't disprove them (maybe the ring has additional relations; ring can't use them, it can only prove what's universally true, in a polynomial ring).

[Rado Kirov]

Are there tactics that try to find concrete instances of existentials? Like if I give it exists p \in Prime, 2^p -1 is composite it grinds some small primes for a bit and outputs 11 (or gives up)? It can use type classes to match the type with a generator something like https://en.wikipedia.org/wiki/QuickCheck but done at type-checking not test run time.

[Kyle Miller]

Yes, Lean's QuickCheck is known as Plausible