dec_trivial fails with instances using `rw`

Stream: general

[Scott Morrison]

Observe the following two decidable instances, one of which uses a rewrite, and fails on most inputs, and one which avoids using the rewrite, and works just fine.

inductive T : ℕ → Prop
| t : Π {L : ℕ}, T L

def good : decidable_pred T
| L := decidable.is_true T.t

lemma T_iff (L : ℕ) : T L ↔ true :=
⟨λ h, trivial, λ h, T.t⟩

def bad : decidable_pred T
| L := by { rw T_iff, apply_instance, }

section good
local attribute [instance] good

example : T 0 := dec_trivial
end good

section bad
local attribute [instance] bad

example : T 0 := dec_trivial  -- FAILS
end bad

[Scott Morrison]

I suspect that this, rather than any timeout issues, is actually the root cause of most of the failures I see in trying to use dec_trivial.

[Scott Morrison]

Can someone explain what is going on?

[Scott Morrison]

(Obviously this is a minimised example; I hit this problem "in the wild", with a decidability instance where it was more painful to avoid using rewrite.)

[Keeley Hoek]

If you print them, you get

def good._main : @decidable_pred nat T :=
λ (a : nat), id_rhs (decidable (T a)) (@decidable.is_true (T a) (@T.t a))

vs

def bad._main : @decidable_pred nat T :=
λ (a : nat), id_rhs (decidable (T a))
    (@eq.mpr (decidable (T a)) (decidable true)
       (@id (@eq Type (decidable (T a)) (decidable true))
          (@eq.rec Prop (T a) (λ (_a : Prop), @eq Type (decidable (T a)) (decidable _a))
             (@eq.refl Type (decidable (T a)))
             true
             (@propext (T a) true (T_iff a))))
       decidable.true)

[Keeley Hoek]

The first one gives an is_true of the right type, along with a proof.
The second one proves that what we are deciding is the same as just deciding true, and then just says "true".

[Keeley Hoek]

Of course, both actually decide the question...

[Keeley Hoek]

The underlying problem is that

example : @ite _ (good 0) _ true false := trivial

but

example : @ite _ (bad 0)  _ true false := trivial

doesn't. I don't know if that's really any simpler, since an ite is just a rec on decidable.

[Keeley Hoek]

Interestingly, if I replace the ite with its definition in either of those lines, both fail.

[Scott Morrison]

It turns out this problem is the underlying cause of decidable instances for combinatorial games not working.

[Scott Morrison]

I could fix the decidable instances for the integer-valued games, but domineering seems to intrinsically involve non-definitional equations in the construction of short instances, so dec_trivial is still broken there.

[Chris Hughes]

It's to do with the fact that the proof of equality uses propext, and isn't a definitional equality, so the eq.rec application can't be iota reduced because the resulting expression won't type check.

[Mario Carneiro]

the moral of the story is to always use decidable_of_iff instead of rw to prove decidable instances. (It doesn't matter how you prove the iff)

[Scott Morrison]

@Mario Carneiro, I think it's worse than that. I've been investigating the decidability instances in the combinatorial games PR. By carefully avoiding rw I can now prove (0 : pgame) < 1 := dec_trivial, but dec_trivial still fails on everything involving domineering.

[Scott Morrison]

https://github.com/leanprover-community/mathlib/blob/surreal/src/set_theory/game/domineering.lean#L131

[Mario Carneiro]

The other problem I think you will run into with surreals and games is the use of well founded recursion

[Mario Carneiro]

You may be able to make it compute, but everything in the proof of well foundedness needs to be able to reduce, i.e. it can't be marked theorem even if it's a proof

[Scott Morrison]

ooh, I never knew that defining something propositional using def was any different from defining it using theorem!

[Mario Carneiro]

You rewrote in a proof of short? This is a bad idea and there is even a comment that says as much

[Scott Morrison]

You mean the unfold domineering {single_pass:=tt}?

[Mario Carneiro]

yes

[Mario Carneiro]

It's not clear to me why short is not a proposition

[Mario Carneiro]

at the very least you should prove it's a subsingleton

[Scott Morrison]

I need to get the fintypes back out of it at various points, I think.

[Scott Morrison]

And if I make it a Prop I can't eliminate anymore.

[Mario Carneiro]

is it preserved by equivalence?

[Scott Morrison]

Yes

[Scott Morrison]

oh ...

[Scott Morrison]

not obviously

[Scott Morrison]

sorry, no, it's not preserved under equivalence, I think!

[Scott Morrison]

You can just add infinitely many irrelevant options

[Mario Carneiro]

Oh but I see you have relabelling for this

[Mario Carneiro]

and possibly restriction too

[Mario Carneiro]

so you may be able to prove restriction x y -> short y -> short x

[Mario Carneiro]

wait no, restriction does a different thing on the left and right

[Scott Morrison]

restriction says that things are better for Left, and worse for Right

[Scott Morrison]

(err, maybe other way round)

[Scott Morrison]

I proved short is a subsingleton.

[Scott Morrison]

Why is it that you're interested in whether short is preserved by equivalence?

[Scott Morrison]

I think it really doesn't descend to the quotient; you could define short on the quotient by asking that there exists a pgame representative that is short.

[Scott Morrison]

@Mario Carneiro, do you have any advice on diagnosing non-computable problems in dec_trivial? I don't even know how to track down "the proof that is blocking reduction" in any example. (That is, all I know how to do is read everything that might be involved and look for bad smells.)

[Mario Carneiro]

You can use #reduce to find out what you got that isn't of_true ... or of_false ...

[Mario Carneiro]

In the literature they call this "canonicity", and lean doesn't have it because of axioms and irreducible proofs

[Mario Carneiro]

irreducible proofs aren't usually a problem because of proof irrelevance, but subsingleton eliminators like acc use a proof as their major premise, so we have to be able to reduce that proof to a constructor

[Mario Carneiro]

In fact whnf is sufficient, in case #reduce times out

[Scott Morrison]

What is it that I should be passing to whnf?

[Scott Morrison]

run_cmd tactic.whnf `(domineering.L ≤ 1) >>= tactic.trace

[Scott Morrison]

I'm missing a ...?

[Mario Carneiro]

the proof of decidable (domineering.L ≤ 1)

[Scott Morrison]

So

run_cmd tactic.whnf `(by apply_instance : decidable (domineering.L ≤ 1)) >>= tactic.trace

[Scott Morrison]

?

[Mario Carneiro]

yes, I think that should work

[Mario Carneiro]

does it?

[Scott Morrison]

Yes

[Scott Morrison]

it's a little long

[Mario Carneiro]

If it is successful, you will get a term that starts with decidable.of_true. Otherwise, you should look for the "active" part of the term; that's the head of the term unless it's a recursor, in which case you should look at the active part of the major premise, and recurse until you find something that's not a recursor

[Mario Carneiro]

In this case we have a recursor, decidable.rec, applied to fintype.decidable_forall_fintype in the major premise (at the end)

[Mario Carneiro]

so the question is, why isn't that reducing? You may need to turn on pp.implicit

[Scott Morrison]

pp.implicit and pp.max_steps gives me: (message too long, truncated at 262144 characters)

[Scott Morrison]

I guess that's what the command line is for.

[Mario Carneiro]

I weep for lean

[Keeley Hoek]

Mario, you mean is_true and is_false in your comment up there right?

[Mario Carneiro]

yes, I always forget the names

[Scott Morrison]

Hmm, the full output with pp.implicit is now at https://gist.github.com/semorrison/56f6f878a3d60d8aaee93184146fff08

[Scott Morrison]

but I can't find the "active part" anymore.

[Scott Morrison]

Unfortunately there are now 6 different appearances of fintype.decidable_forall_fintype

[Scott Morrison]

counting brackets tells me it's now at line 7590. :-)

[Keeley Hoek]

This is the worst __most fun__ thing ever

[Mario Carneiro]

The way I would analyze this is by manipulating the expr from lean, i.e. get the 6th subterm of the decidable.rec application, and print it

[Mario Carneiro]

Even without knowing the arguments to fintype.decidable_forall_fintype, it's strange to me that this would be the active term, because it's a definition. It should have unfolded

[Scott Morrison]

Curiously, the output has exactly four instances of eq.mpr. I think I know how to get rid of them.

[Mario Carneiro]

The very last thing printed is an underscore, though, suggesting that it may be stuck on a proof

[Scott Morrison]

Hmm, got rid of the eq.mprs, but that didn't help. Now trying pp.proofs...

[Scott Morrison]

Interestingly, shrinking the domineering board to a single cell causes it to reduce to is_true.