Iverson bracket in Lean

Stream: general

[suhr]

I'd like to coerce decidable propositions to natural numbers, so I could write expressions like in https://en.wikipedia.org/wiki/Iverson_bracket.

I tried to do this naively:

instance (p : Prop) [h : Decidable p]: Coe p Nat := (decide p).toNat

Unfortunately this does not work:

cannot find synthesization order for instance «instCoeNatOfDecidable_external:file:///MathlibDemo/MathlibDemo.lean» with type
  (p : Prop) → [h : Decidable p] → Coe p Nat
all remaining arguments have metavariables:
  Decidable ?p

Is there a way to fix this?

[suhr]

Of course I can just define def chi (p : Prop) [h : Decidable p] : Nat := (decide p).toNat, but chi (x > i) is a bit annoying compared to just (x > i).

[Edward van de Meent]

there's two issues here; the first is that Coe p Nat means "i can turn any element of p into an element of Nat". in other words, this will choose a constant function from proofs of p (not the veracity or not of p) to natural numbers. The second is that as the error suggests, since lean won't be able to infer p just from Nat, the synth order has to be the other way, meaning that you want to implement the CoeOut typeclass instead

[Edward van de Meent]

you might be interested in this:

instance (p : Prop) [Decidable p]: CoeDep Prop p Nat where
  coe := (decide p).toNat