Declaring a function to be decidable

Stream: new members

[Kris Brown]

Hi, I didn't see anything in Chapter 11 of TPIL about taking a function (which Lean fails to synthesize "decidable" for) and specifying it is decidable.

import data.equiv.basic
open equiv -- "perm x" is "equiv x x" AKA "x ≃ x"

/-
Defining a predicate for a permutation on a finite set to be a k-cycle
Start at 0, and take k steps (which don't bring you to 0 until the last one)
-/
def cyclicrec : Π{n:ℕ}, ℕ → fin n → perm (fin n) → Prop
 | n 0        curr p := (p.to_fun curr).val = 0
 | n (succ m) curr p := ((p.to_fun curr).val > 0 )
                                            ∧ cyclicrec m (p.to_fun curr) p

def cyclic : Π{n:ℕ}, perm (fin n) → Prop
 | 0        _ := ff -- exclude 0-cycles
 | (succ m) p := cyclicrec m ⟨0, succ_pos'⟩ p

// something like: instance decidable {n:ℕ} {p: perm (fin n)} : (cyclic p) := ???

I'd like to make some unit tests to see if my definition is sane, so I construct a concrete instance like def cyc : perm (fin 3) := (0 1 2) and would like to do something like #eval cyclic cyc and see tt, and likewise for #eval cyclic not_cyc to show ff. Is there a way to do this in Lean?

[Jalex Stark]

for me your definitions fail at the equation compiler level

[Kris Brown]

Hm, I'm using Lean (version 3.16.2, commit 8f928c403cee, Release). I'd love to test it on the Lean Web Editor but it seems like you can't import from mathlib using that? (I get file 'data/equiv/basic' not found in the LEAN_PATH)

[Kris Brown]

I'm not exactly sure what failing at the equation compiler level specifically means - I thought the definition was valid because my VScode editor is not highlighting anything

[Bryan Gin-ge Chen]

Hmm, you might have to clear the library cache, because this works for me in the Lean web editor. To do so, click the (?) button and then scroll to the bottom and click the "Clear library cache and refresh" button.

[Bryan Gin-ge Chen]

Using VS Code is highly preferred to using the web editor, by the way.

[Kris Brown]

Sorry, I was using leanprover.github rather than leanprover-community.github.

[Bryan Gin-ge Chen]

That one imports a 2018 version of mathlib, I think.

[Bryan Gin-ge Chen]

OK, I made some slight tweaks, and this should work with the latest version of mathlib and the community web editor:

import data.equiv.basic
import data.nat.basic
open equiv nat -- "perm x" is "equiv x x" AKA "x ≃ x"

/-
Defining a predicate for a permutation on a finite set to be a k-cycle
Start at 0, and take k steps (which don't bring you to 0 until the last one)
-/
def cyclicrec : Π{n:ℕ}, ℕ → fin n → perm (fin n) → Prop
 | n 0        curr p := (p.to_fun curr).val = 0
 | n (succ m) curr p := ((p.to_fun curr).val > 0 )
                                            ∧ cyclicrec m (p.to_fun curr) p

def cyclic : Π{n:ℕ}, perm (fin n) → Prop
 | 0        _ := ff -- exclude 0-cycles
 | (succ m) p := cyclicrec m ⟨0, succ_pos'⟩ p

(I'm using a version of mathlib that's just a few days old, but still on Lean 3.16.3.)

[Kris Brown]

Thanks! So if you just add

def iden  : perm (fin 3) := 1 -- identity permutation
#eval if h: cyclic iden then 0 else 1

You'll see that it is not able to synthesize decidable for cyclic p.

Is the problem then that Lean doesn't know that iden is decidable, rather than an issue with cyclic?

[Kevin Buzzard]

A lot of stuff in mathlib was written by mathematicians, who are typically not bothered with decidability. Certainly this is decidable, indeed I can think of a really crap algorithm which decides it, but I can quite believe that nobody put it into mathlib. If you're interested in that kind of thing then there are two ways to go: either you do some super-inefficient general thing saying "clearly some brute force argument works, so done", or you write an algorithm which actually terminates in practice. Of course the latter is much harder, because you'll also have to formally verify that your algorithm works.

[Kevin Buzzard]

It would not surprise me if the corresponding thing were in Coq, they are far more concerned with these issues.

[Kevin Buzzard]

I am not really able to help more -- most Lean files I write start with assuming the axiom that everything is decidable -- I am more interested in proofs than algorithms. But there are certainly people here who could help (although they might not read #new members -- you could ask in #maths as this is a perfectly respectable question)

[Kris Brown]

Thanks, I appreciate the in-depth answer! I can post there too. Though I still don't understand what the actual problem I'm facing is. Is there some dependency (in data.{nat,equiv,fintype}.basic) that I'm implicitly using that's noncomputable (and I'd have to find it and replace with something computable)?

[Kevin Buzzard]

decidable is an inductive type. https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#decidable-propositions

[Kevin Buzzard]

If you want to make a term of type decidable p then you have two constructors available to you -- you either have to prove that p is true or that p is false.

[Kevin Buzzard]

I am not a computer scientist and I found the abstract description in TPIL quite hard to follow in this abstract setting. However when I looked at the proof that <= on nat was decidable in Lean it all made sense.

[Kevin Buzzard]

instance decidable_le : ∀ a b : ℕ, decidable (a ≤ b)
| 0     b     := is_true (zero_le b)
| (a+1) 0     := is_false (not_succ_le_zero a)
| (a+1) (b+1) :=
  match decidable_le a b with
  | is_true h  := is_true (succ_le_succ h)
  | is_false h := is_false (λ a, h (le_of_succ_le_succ a))
  end

[Kevin Buzzard]

This is a pretty sensible algorithm to work out if $a\leq b$ -- if one is 0 it's easy, and if they're both positive then subtract one and continue. Note that in this case you have to pass to Lean proofs of things like if $a\leq b$ then $a+1\leq b+1$ -- it's a formally verified algorithm.

[Kevin Buzzard]

For decidability of questions like cyclicity of a permutation, you could either attempt to write some sort of sensible algorithm like that, or you can perhaps (I am not strong in this area so take everything I say with a pinch of salt) just do it by magic -- say "it's a finite computation, so there's bound to be an algorithm"

[Kevin Buzzard]

There is an art to this, and some people (who don't read #new members ) are very good at it. Unfortunately I'm not one of those people, because I just cheat and add the axiom that all props are decidable whenever I run into an undecidability issue. I'm afraid I've now told you everything I know about decidability. You might want to ask in #maths .

[Kevin Buzzard]

But I think the answer to your question is that pretty much everything is implicitly undecidable, in the sense that most propositions in Lean won't have the decidable predicate proved for them, perhaps because of laziness -- it is not a high priority around here.

[Kris Brown]

Thanks! I wanted to take a crack at it before asking maths, but I can't even get the signature to typecheck:

instance decidable_cyclic : Π n : ℕ, Π p: perm (fin n), decidable (cyclic p)
  _     _     := sorry

Error

function expected at
  decidable (cyclic p)
term has type
  Type

This doesn't make sense to me since cyclic p is a Prop and decidable is Prop -> Type.

[Kris Brown]

Just pattern matching off the decidable_le example

[Kevin Buzzard]

instance decidable_cyclic : Π n : ℕ, Π p: perm (fin n), decidable (cyclic p)
:= sorry

def iden  : perm (fin 3) := 1 -- identity permutation
#check if h: cyclic iden then 0 else 1

[Kevin Buzzard]

The _s in the <= example are matching a and b, which you don't have (they're proving forall a b, ...)

[Kris Brown]

I see, ok think I've got enough info to try this now - thanks so much!

[Kevin Buzzard]

Good luck!

[Kevin Buzzard]

instance decidable_cyclic : Π n : ℕ, Π p: perm (fin n), decidable (cyclic p)
| _ _ := sorry

I just saw you had two inputs too -- sorry, was talking nonsense earlier. You were missing the bar.

[Kris Brown]

oops - good catch!

[Kevin Buzzard]

Thinking about this -- the order should be computable, and so should the sizes of the orbits, so if you had a theorem saying that the permutation was cyclic iff one orbit has size equal to the order and the others all have size 1 then dec_trivial might be able to tell that this is decidable.

[Kevin Buzzard]

Oh maybe our definitions are different. It's annoying that the derive handler can't do this though

[Alex J. Best]

Do I understand correctly that your definition of cyclic means that p should be an n-cycle? not just an arbitrary cycle?
In any case you might find decidable_of_iff usefull, you can then change to an equivalent proposition for which proving decidablity is easier.

[Mario Carneiro]

Kevin Buzzard said:

But I think the answer to your question is that pretty much everything is implicitly undecidable, in the sense that most propositions in Lean won't have the decidable predicate proved for them, perhaps because of laziness -- it is not a high priority around here.

As far as I know, this is not true. We've proved decidability for basically every predicate for which it makes sense

[Mario Carneiro]

But you mathematicians are moving fast and maybe not keeping this practice up for newly defined predicates

[Kevin Buzzard]

I'm sure you know a lot more about what's decidable than I do Mario!

[Mario Carneiro]

I believe the correct version of that statement would be decidable (cyclic A) given fintype A and decidable_eq A

[Mario Carneiro]

However this is not a very good implementation computation wise

[Mario Carneiro]

but it's better than nothing and it will probably suffice for groups of size 3 or so

[Mario Carneiro]

@Kris Brown Reading this thread more carefully, I notice that the definition of cyclic is not the usual mathematical style definition, but rather an explicit recursive function that could be used as the algorithm. In this case, there is a simple hack you can do to make it obviously decidable: change the return type from Prop to bool and let coercion do the rest

import data.equiv.basic
import data.nat.basic
open equiv nat -- "perm x" is "equiv x x" AKA "x ≃ x"

/-
Defining a predicate for a permutation on a finite set to be a k-cycle
Start at 0, and take k steps (which don't bring you to 0 until the last one)
-/
def cyclicrec : Π{n:ℕ}, ℕ → fin n → perm (fin n) → bool
 | n 0        curr p := (p.to_fun curr).val = 0
 | n (succ m) curr p := ((p.to_fun curr).val > 0 )
                                            ∧ cyclicrec m (p.to_fun curr) p

def cyclic : Π{n:ℕ}, perm (fin n) → bool
 | 0        _ := ff -- exclude 0-cycles
 | (succ m) p := cyclicrec m ⟨0, succ_pos'⟩ p

def iden  : perm (fin 3) := 1 -- identity permutation
#eval if h: cyclic iden then 0 else 1 -- 1

[Alistair Tucker]

Would you want PRs for any additional decidability proofs? I have

variables (α : Type*) (r : finset α → finset α → Prop) [decidable_rel r]

instance decidable_exists_of_subsets (s : finset α) : decidable (∃ t (ht : t ⊆ s), r t s) :=
decidable_of_iff (∃ t (hp : t ∈ s.powerset), r t s) $ by finish

variable [decidable_eq α]

instance decidable_exists_of_ssubsets (s : finset α) : decidable (∃ t (ht : t ⊂ s), r t s) :=
decidable_of_iff (∃ t (hp : t ∈ s.powerset) (hn : ¬ s ⊆ t), r t s) $ by finish

[Mario Carneiro]

Hm, that seems okay, although you can end up writing a lot of such functions without some guiding principles

[Mario Carneiro]

I don't mind asking people to craft their predicates in a particular way in order to make them more obviously decidable. In examples like this, it's just as possible that the real predicate isn't explicitly over a finset at all (or subsets or ssubsets of one) but rather the predicate r is false outside the finset s for some reason

[Mario Carneiro]

so you would have to insert some rewrite anyway

[Mario Carneiro]

(but if you are going to PR these functions you should do the forall version too)

[Mario Carneiro]

Also, r should not depend on s here, there is no reason for that dependency

[Alistair Tucker]

You are right, it still works without the explicit dependence on s. I guess Lean is smarter than I realised! I'm not sure I understand your first point though. Do you mean it should be made over a more general type sharing some of finset's properties?

[Alex J. Best]

Oh I just found completely by accident that there is a definition is_cycle in group_theory.perm.sign expressing the same notion, seems like there are a lot of lemmas for it there already.