How to track down which prop is undecidable?

Stream: new members

[aron]

I'm getting this error in my definition of a function:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.propDecidable', which is 'noncomputable'

I do indeed switch on 2 props in if expressions but I have defined Decidable instances for both kinds of props I am switching on. Is there a way to get Lean to tell me more precisely about which prop decidable it has a problem with? Atm the error is on the top-level function which is not very helpful for debugging purposes

[Aaron Liu]

just don't have Classical.propDecidable as an instance?

[Robin Arnez]

Did you open Classical somewhere? Try removing that

[aron]

No? not as far as I know?

[aron]

I suppose I do reference Classical.exists_or_forall_not somewhere, but I haven't opened the Classical namespace anywhere

[Robin Arnez]

Hmm, what does your definition look like?

[Robin Arnez]

Maybe it's something else in the function?

[aron]

instance ResolvableUniVarInTy.decide (ctx : List TyMaybe') (ty : Ty') (uv : Nat) : Decidable (ResolvableUniVarInTy ctx ty uv) := by
  if h : uv < ctx.length then
    let target := ctx.reverseGet uv h
    have iari : IsAtRevIndex uv ctx target := IsAtRevIndex.reverseGet_from_prf h
    cases' htarget : target with uvTy
    · rw [htarget] at iari
      if hh : uv ∈ ty then
        if hhh : TyResolved ctx uvTy then
          refine .isTrue ?_
          refine .mk hh iari hhh
        else
          refine .isFalse ?_
          intro ruvit
          cases ruvit
          expose_names
          have := iari.injective h_2
          subst_eqs
          contradiction
      else
        refine .isFalse ?_
        intro ruvit
        cases ruvit
        contradiction
    · refine .isFalse ?_
      intro ruvit
      cases' ruvit with target hin iariconc
      · rw [htarget] at iari
        have := iari.injective iariconc
        contradiction
  else
    refine .isFalse ?_
    intro ruvit
    cases' ruvit with target hin iari
    absurd h
    refine iari.isLt

and I have both:

instance Ty'.dec_mem_uniVar (ty: Ty') (i : Nat) : Decidable (i ∈ ty)

and

instance TyResolved.decide (ctx : List TyMaybe') (ty : Ty') {prf : ∀ i ∈ ty, i < ctx.length} : Decidable (TyResolved ctx ty)

[aron]

Hm could it be that TyResolved.decide requiring an extra param {prf : ∀ i ∈ ty, i < ctx.length} is getting in the way of decidability?

[aron]

Yeah I think it was that. I don't know if there's a way to pass in an implicit param needed by my Decidable instance to the if expression so I replaced the:

if hhh : TyResolved ctx uvTy then

with a:

have : ∀ i ∈ uvTy, i < ctx.length := by ...

match @TyResolved.decide ctx uvTy this with
| .isTrue prf => ...
| .isFalse contra => ...

i.e. I explicitly call the decide function with all needed params and then match on the cases, the error goes away :tada:

[Robin Arnez]

Oh, you defined it with tactics. I wouldn't recommend that because, among other things, that makes it open Classical in the conditions. Try something like this:

instance ResolvableUniVarInTy.decide (ctx : List TyMaybe') (ty : Ty') (uv : Nat) : Decidable (ResolvableUniVarInTy ctx ty uv) :=
  if h : uv < ctx.length then
    let target := ctx.reverseGet uv h
    have iari : IsAtRevIndex uv ctx target := IsAtRevIndex.reverseGet_from_prf h
    match target with
    | .whatever_your_thing_is_called uvTy =>
      if hh : uv ∈ ty then
        if hhh : TyResolved ctx uvTy then
          isTrue (.mk hh iari hhh)
        else
          isFalse ?case1
      else
        isFalse ?case2
    | .the_other_thing_you_have =>
      isFalse ?case3
  else
    isFalse ?case4
where finally
  case case1 =>
    intro ruvit
    cases ruvit
    expose_names
    have := iari.injective h_2
    subst_eqs
    contradiction
  case case2 =>
    intro ruvit
    cases ruvit
    contradiction
  case case3 =>
    intro ruvit
    cases' ruvit with target hin iariconc
    · rw [htarget] at iari
      have := iari.injective iariconc
      contradiction
  case case4 =>
    intro ruvit
    cases' ruvit with target hin iari
    absurd h
    refine iari.isLt

A lot easier to read because of the definition/proof separation and more robust (this version should give you the Decidable error)

[aron]

oh interesting :thinking: I haven't seen this pattern before

[Robin Arnez]

It's quite recent but it's also a very good tool for definition readability

[aron]

mm yeah it's nice

[aron]

ok yeah I'm now getting the error at the right place!

failed to synthesize
  Decidable (TyResolved ctx uvTy)

[aron]

but although I can now see the error in the right place I still need to call TyResolved.decide explicitly I think. So I can pass in the implicit param correctly

[aron]

Is there a way to pass in the implicit param with the if h : <myProp> then syntax?

[aron]

Robin Arnez said:

because, among other things, that makes it open Classical in the conditions.

why does it do this btw? seems like an odd choice

[aron]

(...no pun intended)

[Robin Arnez]

It's just notation for by_cases and you usually don't want to see decidability errors in your proofs

[Kenny Lau]

basically try to avoid using tactics in definitions