All decidable

Stream: new members

[Patrick Johnson]

Is there a way to specify that everything I am working with in a lemma is decidable (prop_decidable, decidable_pred, nat.decidable_lt, etc). I am facing weird situation where if I add letI := nat.decidable_lt then the first half of the proof cannot unify, but if I remove it, then the second half of the proof cannot unify.

[Patrick Johnson]

BTW, I am totally confused about how decidability instances work :/

[Eric Wieser]

#mwe?

[Patrick Johnson]

import tactic
import data.list

open nat
open list
open classical

open_locale classical

def quicksort : list ℕ → list ℕ
| [] := []
| (x :: xs) :=
  quicksort (filter (λy, y ≤ x) xs) ++
  [x] ++
  quicksort (filter (λy, x < y) xs)
using_well_founded { dec_tac := `[sorry] }

def sorted : list ℕ → Prop
| [] := true
| [x] := true
| (x :: y :: ys) := x ≤ y ∧ sorted (y :: ys)

lemma filter_length {f : ℕ → Prop} {xs : list ℕ} :
  (filter f xs).length ≤ xs.length :=
begin
  sorry,
end

lemma sorted_append {xs ys : list ℕ}
  (h₁ : sorted xs)
  (h₂ : sorted ys)
  (h₃ : ∀ (x ∈ xs) (y ∈ ys), x ≤ y) :
  sorted (xs ++ ys) :=
begin
  sorry,
end

-- set_option pp.all true

lemma qs_correct {xs xs' : list ℕ}
  (h : xs' = quicksort xs) :
  sorted xs' ∧ (xs : multiset ℕ) = xs' :=
begin
  letI := decidable_pred,
  letI := prop_decidable,
  letI := nat.decidable_lt, -- comment out this line
  subst h,
  split,
  { generalize len_def : length xs = len,
    induction len using nat.strong_induction_on
      with len h₁ generalizing xs,
    dsimp at h₁,
    cases xs with x xs,
    { simp_rw quicksort },
    { simp_rw quicksort,
      apply sorted_append,
      sorry,
      { apply h₁,
        change length (filter (has_lt.lt x) xs) < len,
        simp_rw length at len_def,
        subst len_def,
        apply lt_succ_of_le,
        { apply filter_length },
        { refl }},
      sorry }},
  sorry,
  sorry,
end

[Kyle Miller]

I haven't really looked at the mwe, but tactic#classical is a way to introduce all the classical decidable instances inside a tactic proof. (This doesn't make decidable things classical, though. tactic#convert and tactic#convert_to can be helpful.)

[Eric Wieser]

Removing open_locale classical should make that easier for you, IMO

[Apurva Nakade]

This reminds me of a question I have always had but never quite got to asking here: why do we have to specify decidability at all? Is there any interesting math that is beyond decidability? Why isn't decidability just one of the core axioms in mathlib?

[Yakov Pechersky]

Decidability is innately linked to computation. Decidability means you have an algorithm that provides the resolution of some proposition. Decidability is a core axiom in mathlib, accessed by the open_locale classical. But to say that everything is decidable is to say that the halting problem is not a problem. If everything is decidable, then given an arbitrary calculation (represented by a Turing machine), we can know for sure whether it halts or whether it goes on forever. But Turing proved that this is not the case for arbitrary Turing machines.

Another example is decidable equality of real numbers represented as Cauchy sequences. If I give you two possibly infinite lists, where each one represents the Cauchy sequence, and I promise that both converge to some number, but possibly not the same one, can you decide whether the two sequences actually converge to the same number? It's very easy to say that whether these two sequences are different -- just keep checking each pair of terms until you hit a pair that has two different terms in it. That means that you know that the sequences are different in at least one place. However, to prove that the sequences really do converge to the same number, you would have to check an infinite number of pairs of terms. And that's not possible. You could say "OK I'll check until some radius of convergence, and say they're equal to some epsilon difference", which is useful(!) but not true equality.

[Apurva Nakade]

Ah, interesting, thanks a lot! So from what I understand, the decidability criterion is here because Lean is not able to check proofs but also do computations and decidability helps keep track of which functions are computable and which aren't. This clarifies things a lot!

[Kyle Miller]

@Apurva Nakade Complementing Yakov's explanation:

Decidability also has to do with wanting to make definitions of things computable. There are two sorts of types, Prop and Type*. Objects whose type is an inductive type in Type* all have some algorithm backing them, and you're able to figure out which constructor created the object in finite time (so you're able to match on them). Objects whose type is in Prop (propositions) don't have this property.

The decidable system is a way to match on specific Props, and one of the main interfaces is if p then ... else .... A decidable p instance is essentially a function you can compute that returns a concrete boolean for whether or not p is true. That way you can create things in Type* that depend on the truth of a proposition, which you otherwise can't do.

Even though every Prop is definitely equal to true or false, there's no general algorithm to evaluate which it is (that's the incompleteness theorem), so Lean/mathlib instead has this decidability system.

This is useful for when you write programs in Lean (like tactics) since then you can use Props for conditions. It can also be nice to know mathematically whether a proposition is decidable, since it means you've reduced a problem to rote computation.

[Apurva Nakade]

Thanks! I'll look at the uses of decidability in Lean again. I guess we just power through computations in math a lot and worry about decidability or computability as needed as an afterthought. But we really do use it implicitly every single time we do a computation!

[Kyle Miller]

Another use for decidable is that you can use dec_trivial to automatically prove things that are decidable (though this seems to have been intentionally weakened recently to make it easier to port mathlib to Lean 4).

[Mario Carneiro]

not sure what you mean, dec_trivial still works in lean 4 although it is now spelled by decide

[Kyle Miller]

@Mario Carneiro I could be wrong, but doesn't lean#562 make it so that decidability instances depending on well-founded recursion no longer work?

[Mario Carneiro]

yes, but they didn't work even before that

[Mario Carneiro]

previously it would unfold the WF lemma, which was hit or miss because it only works if the lemma was proved without axioms (and the majority of even simple theorems use at least propext). After lean#562 lemmas are not unfolded, so these fail reliably instead of working or failing unpredictably