Any tricks to get rid of boilerplate when constructing proofs of absurd predicate on enums?

Question

Let's say I have

data Fruit = Apple | Banana | Grape | Orange | Lemon | {- many others -}

and a predicate on that type,

data WineStock : Fruit -> Type where
    CanonicalWine : WineStock Grape
    CiderIsWineToo : WineStock Apple

which doesn't hold for Banana, Orange, Lemon and others.

It can be said that this defines WineStock as a predicate on Fruit; WineStock Grape is true (since we can construct a value/proof of that type: CanonicalWine) as well as WineStock Apple, but WineStock Banana is false, since that type is not inhabited by any values/proofs.

---

Then, how can I go about using effectively Not (WineStock Banana), Not (WineStock Lemon), etc? It seems that for each Fruit constructor besides Grape and Apple, I can't help but have to code up a case split over WineStock, somewhere, full of impossibles:

instance Uninhabited (WineStock Banana) where
    uninhabited CanonicalWine impossible
    uninhabited CiderIsWineToo impossible

instance Uninhabited (WineStock Lemon) where
    uninhabited CanonicalWine impossible
    uninhabited CiderIsWineToo impossible

instance Uninhabited (WineStock Orange) where
    uninhabited CanonicalWine impossible
    uninhabited CiderIsWineToo impossible

Note that:

• the code is repetitive,
• LoC will explode when the predicate definition grows, gaining more constructors. Just imagine the Not (Sweet Lemon) proof, assuming there're many sweet alternatives in the Fruit definition.

So, this way doesn't quite seem satisfying, almost impractical.

Are there more elegant approaches?

Hebrew

Many of the old Haskell idioms don't change in dependently-typed systems. "Make illegal states unrepresentable" holds at the type-level too: I don't think you should even be able to construct those impossible types. I'd probably structure this example as (something roughly like) a type of fruits that can make wine data WineFruit = Grape | Apple and other fruits data Fruit = WineFruit WineFruit | Banana | Orange | Lemon – Monovalent

@BenjaminHodgson, that approach starts to fall apart when you want to add PieFruit, SaladFruit, WeaponFruit, etc. – Bil

Given that you're in idris, why are you defining a datatype for WineStock? Can't you just define isWineStock as a value level function and use it in proofs where appropriate? – Sadoc

Answer 1

@slcv is right: using a function that computes whether a fruit satisfies a property or not rather than building various inductive predicates will allow you to get rid of this overhead.

Here is the minimal setup:

data Is : (p : a -> Bool) -> a -> Type where
  Indeed : p x = True -> Is p x

isnt : {auto eqF : p a = False} -> Is p a -> b
isnt {eqF} (Indeed eqT) = case trans (sym eqF) eqT of
                            Refl impossible

Is p x ensures that the property p holds of the element x (I used an inductive type rather than a type alias so that Idris doesn't unfold it in the context of a hole; it's easier to read this way).

isnt prf dismisses the phoney proof prf whenever the typechecker is able to generate a proof that p a = False automatically (via Refl or an assumption in the context).

Once you have these, you can start defining your properties by only enumerating the positive cases and adding a catchall

wineFruit : Fruit -> Bool
wineFruit Grape = True
wineFruit Apple = True
wineFruit _     = False

weaponFruit : Fruit -> Bool
weaponFruit Apple  = True
weaponFruit Orange = True
weaponFruit Lemon  = True
weaponFruit _      = False

You can define your original predicates as type aliases calling Is with the appropriate decision function:

WineStock : Fruit -> Type
WineStock = Is wineFruit

And, sure enough, isnt allows you to dismiss the impossible cases:

dismiss : WineStock Orange -> Void
dismiss = isnt

Ferrate