Computability for sets?

Stream: mathlib4

[David J. Webb]

Right now the computability library deals with functions/predicates/relations, but in my own work on the subject, I often find myself needing basic facts about computable (or primitive/partial recursive) sets - closure under union/intersection/complement/etc. Would these be a good potential addition to Mathlib?

[Eric Wieser]

I think your set is almost docs#PrimrecPred ?

[David J. Webb]

Oh true - I wrote that definition a while ago and hadn't thought more about it, just the lemmas that followed. Perhaps something like Primrec.set X := PrimrecPred (λ x ↦ (x ∈ X) = True) would be cleaner

[Aaron Liu]

You don't need the = True part

[Aaron Liu]

just PrimrecPred fun x => x ∈ X

[David J. Webb]

I thought about that, but I get

failed to synthesize
  DecidablePred fun x ↦ x ∈ X

So I was including = True to avoid needing that as a hypothesis. If there's a better way to get around that error, I'm happy to implement that!

[Aaron Liu]

If you put = True this doesn't actually let you skip DecidablePred fun x ↦ x ∈ X as a hypothesis

[Aaron Liu]

what you should do is add it as an assumption to every theorem you prove

[Aaron Liu]

or, if you know you will never compute with this, you can wrap it in a new definition that uses the classical decidability instance

[David J. Webb]

I can add that the sets under consideration have decidable membership, that's the most reasonable path forward

[Aaron Liu]

however, if the theorem statement does not need decidability, then you can use the classical instance inside the proof

[Aaron Liu]

if a definition needs decidability, you should still add it as a hypothesis

[Aaron Liu]

this is to ensure you don't get diamonds

[David J. Webb]

Ohhhh, okay. Good to know!

Refactoring the definition this way makes many of the proofs much shorter :smiley:

[David J. Webb]

Actually, maybe I'm still misunderstanding something. I have made the definition

def set (X : Set ℕ) [DecidablePred fun x ↦ x ∈ X] : Prop := PrimrecPred (λ x ↦ x ∈ X)

which lets me prove closure for union/intersection/set difference much more slickly than before. But some proofs run into difficulties - for example, when I go to prove

theorem symmdiff (hX : set X) (hY : set Y) [DecidablePred fun x ↦ x ∈ X ∆ Y] : set (X ∆ Y)

the intuitive proof breaks immediately. In the ∃ (f : ℕ → Bool) formalism, it was as simple as

  apply union
  <;> simp [sdiff, hX, hY]

but with this definition I get an error instead

Tactic apply failed: could not unify the conclusion of @union
@set (?X ∪ ?Y) fun a ↦ decidableUnion ?X ?Y a
with the goal
@set (X ∆ Y) inst✝

I had a similar problem with proving that finite sets are primitive recursive - in both cases, I can get around the difficulty by using the fact that this new definition is equivalent to the old one, which seems to defeat the point of the new one!

I figure I've either mis-implemented things, or there is some way to avoid this trouble that I am just unaware of.

[Aaron Liu]

oh no this is a bit complicated

[Yaël Dillies]

Why does docs#PrimrecPred assume DecidablePred?

[Ruben Van de Velde]

I thought it didn't anymore

[Ruben Van de Velde]

Or is that in an open pr?

[Ruben Van de Velde]

#27076

[Ruben Van de Velde]

Reviewed by @Yaël Dillies :innocent:

[Yaël Dillies]

Ahaha

[David J. Webb]

Aaron Liu said:

oh no this is a bit complicated

Music to my ears, I was starting to think I was even worse at Lean than I thought :sweat_smile:

I'll keep an eye on that PR and revisit this refactor after it goes through

[Aaron Liu]

David J. Webb said:

Aaron Liu said:

oh no this is a bit complicated

Music to my ears, I was starting to think I was even worse at Lean than I thought :sweat_smile:

I'll keep an eye on that PR and revisit this refactor after it goes through

So the correct thing to do here is to assume [decXY : DecidablePred fun x ↦ x ∈ X ∆ Y] in your statement, and then in the proof do

  have decX := Classical.decPred fun x ↦ x ∈ X
  have decY := Classical.decPred fun x ↦ x ∈ Y
  obtain rfl := Subsingleton.elim decXY (clear% decXY; inferInstance)

which should hopefully fix all your decidability issues

[David J. Webb]

But this theorem wants set X and set Y as hypotheses, which I cannot even state without having decX and decY already declared. Plus inferInstance fails to synthesize DecidablePred fun x ↦ x ∈ X ∆ Y.

Or is this for after the PR goes through? (If it does)

[Aaron Liu]

David J. Webb said:

But this theorem wants set X and set Y as hypotheses, which I cannot even state without having decX and decY already declared. Plus inferInstance fails to synthesize DecidablePred fun x ↦ x ∈ X ∆ Y.

This has become twice the amount of headache with two sentences

[David J. Webb]

David J. Webb said:

I'll keep an eye on that PR and revisit this refactor after it goes through

Now that it has, I no longer need DecidablePred as a hypothesis (thank goodness)!