Understanding which Decidable instances are computable

Stream: mathlib4

[Alex Meiburg]

I was frustrated that the decide tactic couldn't handle docs#Multiset.decidableForallMultiset, or most decidability instances involving Multisets -- and a result, anything about Finset, Fintype, etc. It's built on docs#Quot.recOnSubsingleton , which uses Eq.ndrec. I wanted to try to write a better decidability instance, but I kept running into the same problem.

Ultimately everything ends with having something like Decidable (p (q : @Quotient T s)) and I know it's equivalent to Decidable (p' q.unquot). But, I can't write that of course. The only thing I can figure out how to write is using some kind of Quotient.lift.decidablePred, but then that all ultimately boils down to Quot.ind giving some proof and Eq.rec.

I would like to be able to Quot.lift a DecidablePred up, but Decidable has data, so Quot.lift doesn't actually apply here.

Of course, this is all fine for native_decide, because it just looks at the VM internal representation. But I can't for the life of me find a way to make this work.... is there a way to make decide works with quotients, at all?

[Yuyang Zhao]

I think we can write a Bool value decision function using Quot.lift first.

[Eric Wieser]

I dispute the use of "bad" to describe decidable instances like this. Decidable instances are useful both for computation and for reduction, and supporting just one of these doesn't make the instance bad.

[Eric Wieser]

(supporting neither is probably a good candidate for the label "bad")

[Yuyang Zhao]

Are there any examples that decide failed?

[Eric Wieser]

Yeah, this works fine:

import Mathlib

example : ∀ a ∈ ({1, 2, 3} : Multiset Nat), a < 4 := by decide

[Alex Meiburg]

Oh, I made a very silly mistake. That is a computable ("good", with apologies to Eric) decidability instance. I was reading the logs wrong. The issue was with a different instance, one I had defined locally that was also getting mixed up in there. I was thrown off because (1) the Multiset instance was at the end, and (2)

#reduce @Multiset.decidableForallMultiset

prints

fun {α} {m} {p} [inst : (a : α) → Decidable (p a)] ↦
  ⋯ ▸
    (Quot.lift
        (fun a ↦
          ⟨Quot.mk List.Perm a,
            Decidable.rec (fun h ↦ isFalse ⋯) (fun h ↦ isTrue ⋯)
              (List.rec ⟨isTrue ⋯, PUnit.unit⟩
                  (fun head tail tail_ih ↦
                    ⟨Decidable.rec (fun h ↦ isFalse ⋯)
                        (fun h ↦ Decidable.rec (fun h ↦ isFalse ⋯) (fun h_1 ↦ isTrue ⋯) tail_ih.1) (inst head),
                      tail_ih⟩)
                  a).1⟩)
        ⋯ m).2

so, that looked to me like it was starting right off with Eq.rec. Why _is_ that a computable instance, then, when it reduces to that?

[Alex Meiburg]

(My original question is moot -- I'll change the topic and, if anyone can answer my sillier follow-up question which is purely out of curiosity, I'll close the topic)

[Eric Wieser]

I claim that #reduce and decide are nothing to do with whether a Decidable instance is computable

[Alex Meiburg]

You're probably right and I'm probably using the words wrong then. :) So I'll try to ask more questions.
(1) What is the word for "this Decidable instance plays nicely with decide"? I guess it's not "computable".
(2) How do I recognize if a Decidable instance will play nicely with decide? I thought (part of) it is that if you end up at an Eq.rec at the head, then you're in trouble, because this won't reduce any more to either True or False. And this is why we should avoid rw in Decidable instances. And so I thought #reduce was a good check to see if this was the case or not.

[Eric Wieser]

1) Kernel-reducible
2) Eq.rec is fine if the equality passed to it is rfl (aka the two sides of the equality are defeq)

[Kyle Miller]

Try using native_decide to see whether the instance is computable. If that fails, then decide almost surely can't work.

[Kyle Miller]

There's also decide +kernel for using kernel reduction (or maybe it's still decide! in this release). decide by itself uses elaborator reduction, which can get stuck for various additional reasons.

[Kyle Miller]

The issue with Eq.rec at the head is that reduction doesn't usually reduce types, which is necessary to detect whether the proof is defeq to rfl. To get reduction to work with decide, yes, it's bets to avoid rw/simp/etc. in the "data part" of a Decidable instance. The decide tactic gives hints about how to do rewrites instead: use one of the iff theorems that transform the proposition into another one. These push the Eq.rec into the proof, so reduction can't get stuck.

[Mario Carneiro]

I don't think that's quite right; the issue is that the Eq.rec is usually over propositions that are not defeq (or otherwise the rewrite wouldn't have been necessary), and the proof is not rfl, it is propext applied to some proof term. This is genuinely a stuck term in the type theory

[Mario Carneiro]

axioms in general break "canonicity"

[Mario Carneiro]

To restore canonicity, you need a type theory that can compute propext (aka univalence for Prop), i.e. cubical type theory

[Mario Carneiro]

or just follow the instructions and use decidable_of_iff instead of rw on Decidable values

[Kyle Miller]

(Thanks, when it comes to this theory I don't really know what I'm talking about. Someone once told me that for closed terms, the Eq.recs should all be reducible, but surely that can't be true when there are axioms.)

[Mario Carneiro]

If rw/simp was better at using iff directly instead of just applying propext then they could generate terms that reduce

[Mario Carneiro]

(this is related to "generalized rewrite")

[Alex Meiburg]

ohboyohboy this is rapidly going over my head.
Well in this case I just brainfarted last night and accidentally used simp_rw even when I should have known I wasn't supposed to. And not doing that and using decidable_of_iff (like I knew I should) fixed everything just fine.

But I would still like to understand, maybe, why Multiset.decidableForallMultiset works when it "looks" to my naive eye like it shouldn't. The Eq that it's recing on is

Quot.liftIndepPr1 (fun a ↦ (fun l ↦ decidable_of_iff (∀ a ∈ l, p a) (Multiset.decidableForallMultiset.proof_2 l)) a)
  (Quot.recOnSubsingleton.proof_1 fun l ↦ decidable_of_iff (∀ a ∈ l, p a) (Multiset.decidableForallMultiset.proof_2 l))
  m
:
(Quot.lift (Quot.indep fun a ↦ (fun l ↦ decidable_of_iff (∀ a ∈ l, p a) ⋯) a) ⋯ m).fst = m

That proof_2 in turn uses propext and Quot.sound. And these use Quot.ind and Quot.lift, which I know aren't axioms per-se but also don't seem like something that should be reducible exactly? Or is that somehow special here?

[Kyle Miller]

Where are you seeing the Eq.rec? I was just looking at Multiset.decidableForallMultiset, and what I'm seeing is that Quotient.recOnSubsingleton extracts the underlying List l out of the Multiset and then evaluates the decidable instance for ∀ a ∈ l, p a, with all the proofs safely tucked away using decidable_of_iff

[Kyle Miller]

Quotient.recOnSubsingleton is also "reduction-safe" because in the end it's Quot.rec, and the proof doesn't need to reduce to reduce Quot.rec.

[Alex Meiburg]

That's just what I got from #reduce @Multiset.decidableForallMultiset. The result started with Eq.rec. I thought this output would reflect what decide would end up with. I guess I was wrong. I don't understand your comment about Quot.rec being "safe", or what the proof needs to reduce or not.

(If I'm asking questions that are too far afield and there's somewhere I should go to read up on this better without bothering y'all, do let me know!)

[Kyle Miller]

Oh, so it does. It looks like Quot.rec starts with a rewrite, huh. I was misremembering, thinking that Quot.rec was more low-level.