## Stream: new members

### Topic: Declaring a function to be decidable

#### Kris Brown (Jun 19 2020 at 17:00):

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 (Jun 19 2020 at 17:58):

for me your definitions fail at the equation compiler level

#### Kris Brown (Jun 19 2020 at 18:25):

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 (Jun 19 2020 at 18:28):

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 (Jun 19 2020 at 18:28):

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 (Jun 19 2020 at 18:29):

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

#### Kris Brown (Jun 19 2020 at 18:29):

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

#### Bryan Gin-ge Chen (Jun 19 2020 at 18:30):

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

#### Bryan Gin-ge Chen (Jun 19 2020 at 18:31):

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 (Jun 19 2020 at 18:37):

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 (Jun 19 2020 at 18:42):

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 (Jun 19 2020 at 18:43):

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

#### Kevin Buzzard (Jun 19 2020 at 18:43):

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 (Jun 19 2020 at 18:53):

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 (Jun 19 2020 at 18:54):

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

#### Kevin Buzzard (Jun 19 2020 at 18:55):

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 (Jun 19 2020 at 18:56):

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 (Jun 19 2020 at 18:56):

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 (Jun 19 2020 at 18:58):

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 (Jun 19 2020 at 18:59):

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 (Jun 19 2020 at 19:01):

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 (Jun 19 2020 at 19:02):

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 (Jun 19 2020 at 19:09):

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 (Jun 19 2020 at 19:09):

Just pattern matching off the decidable_le example

#### Kevin Buzzard (Jun 19 2020 at 19:17):

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 (Jun 19 2020 at 19:18):

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

#### Kris Brown (Jun 19 2020 at 19:19):

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

Good luck!

#### Kevin Buzzard (Jun 19 2020 at 19:20):

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 (Jun 19 2020 at 19:25):

oops - good catch!

#### Kevin Buzzard (Jun 19 2020 at 19:48):

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 (Jun 19 2020 at 19:52):

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

#### Alex J. Best (Jun 19 2020 at 19:52):

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 (Jun 19 2020 at 20:46):

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 (Jun 19 2020 at 20:47):

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

#### Kevin Buzzard (Jun 19 2020 at 20:47):

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

#### Mario Carneiro (Jun 19 2020 at 20:47):

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

#### Mario Carneiro (Jun 19 2020 at 20:49):

However this is not a very good implementation computation wise

#### Mario Carneiro (Jun 19 2020 at 20:49):

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

#### Mario Carneiro (Jun 19 2020 at 20:56):

@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 (Jun 19 2020 at 20:57):

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 (Jun 19 2020 at 21:00):

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

#### Mario Carneiro (Jun 19 2020 at 21:02):

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 (Jun 19 2020 at 21:03):

so you would have to insert some rewrite anyway

#### Mario Carneiro (Jun 19 2020 at 21:03):

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

#### Mario Carneiro (Jun 19 2020 at 21:04):

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

#### Alistair Tucker (Jun 19 2020 at 21:19):

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 (Jun 19 2020 at 21:41):

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.

Last updated: May 16 2021 at 05:21 UTC