Decidable List.cons?

Stream: lean4

[Bjørn Kjos-Hanssen]

I'm not sure what to do here. apply? gives a suggestion exact inst✝ (a :: w) that doesn't work.

instance (P: List (Fin 2) → Prop) [DecidablePred P]
  (w : List (Fin 2)) (a : Fin 2)
  :
Decidable (P (a :: w)) := sorry

[Ruben Van de Velde]

Does inferInstance work?

[Damiano Testa]

There was a discussion somewhere about what should exact?/apply? do about inaccessible identifiers. If you need this to work, you can work around it like this:

Decidable (P (a :: w)) := by
  rename_i h
  exact h (a :: w)

[Damiano Testa]

Ruben, your suggestion work as well! As does by solve_by_elim.

[Bjørn Kjos-Hanssen]

Nice!
(I hadn't realized that inst✝: DecidablePred P being inaccessible was the problem.)

[Kyle Miller]

By the way, because inferInstance works on its own, you shouldn't need to write this instance

[Bjørn Kjos-Hanssen]

Can I import inferInstance?

[Yury G. Kudryashov]

In which sense "import"?

[Yury G. Kudryashov]

[DecidablePred P] means (reducibly) [∀ x, Decidable (P x)], so you don't need x-specific instances for Decidable (P x).

[Bjørn Kjos-Hanssen]

Yury G. Kudryashov said:

In which sense "import"?

Never mind, I see it now.

[Bjørn Kjos-Hanssen]

Kyle Miller said:

By the way, because inferInstance works on its own, you shouldn't need to write this instance

Perhaps we shouldn't even have to write := inferInstance :smile: at all

[Kim Morrison]

Do you want to show us your example where you need it?

[Bjørn Kjos-Hanssen]

Scott Morrison said:

Do you want to show us your example where you need it?

It's for an implementation of recursive backtracking in Lean. I can already use that method to count the number of squarefree words of a given length, but I wanted to generalize it to arbitrary decidable properties P. I can share shortly...

[Bjørn Kjos-Hanssen]

Scott Morrison said:

Do you want to show us your example where you need it?

https://github.com/bjoernkjoshanssen/bay/blob/main/Backtracking.lean

[Eric Wieser]

Could you put a lakefile.lean and lean-toolchain in that repository so that we can run the code in it?

[Eric Wieser]

Otherwise we have to guess the mathlib version, which guarantees that it won't work in future

[Eric Wieser]

I was able to paste it into the web editor and it worked ok

[Eric Wieser]

Kyle Miller said:

By the way, because inferInstance works on its own, you shouldn't need to write this instance

Kyle is correct; you can simply delete both instances and it keeps working

[Bjørn Kjos-Hanssen]

Eric Wieser said:

Kyle Miller said:

By the way, because inferInstance works on its own, you shouldn't need to write this instance

Kyle is correct; you can simply delete both instances and it keeps working

Oops, that's because I shared a working version without the generalization. But basically I want to replace squarefree by an arbitrary (monotone, decidable) predicate on List (Fin 2).

[Eric Wieser]

I think the remark still remains

[Bjørn Kjos-Hanssen]

Eric Wieser said:

I think the remark still remains

I have fixed the code now so it works for an arbitrary "monotone" predicate and updated the github. And indeed, those two instances could be safely deleted.

[Bjørn Kjos-Hanssen]

The main point is illustrated in line 85: example : count_those_with_suffix SQF myvec = 1 := by decide
Squarefree binary words form a somewhat trivial example but it is easy to adapt to cover any "forbidden pattern", for instance cubefree words. Anyway, thanks for the help!