在枚举上构造荒谬谓词的证明时,有什么技巧可以摆脱样板吗？

Question

让我说我有

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

和该类型的谓词,

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

这并不适用于Banana,Orange,Lemon和其他人.

它可以说,这定义WineStock为上一个谓语Fruit; WineStock Grape是真的(因为我们可以构造该类型的值/证明:) CanonicalWine以及WineStock Apple但是WineStock Banana是假的,因为该类型不是任何值/证明所居住的.

---

那么,我该怎么去使用有效Not (WineStock Banana),Not (WineStock Lemon)等等？似乎对于每个Fruit构造函数除了Grape和Apple,我不得不编写一个案例分裂WineStock,某处,充满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

注意:

• 代码是重复的,
• 当谓词定义增长时,LoC将爆炸,获得更多构造函数.想象一下这个Not (Sweet Lemon)证明,假设Fruit定义中有许多甜蜜的选择.

所以,这种方式似乎并不令人满意,几乎不切实际.

有更优雅的方法吗？

Answer 1

@slcv 是对的：使用计算水果是否满足属性的函数而不是构建各种归纳谓词将允许您摆脱这种开销。

这是最小的设置：

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确保属性p保留元素x（我使用归纳类型而不是类型别名，以便 Idris 不会在孔的上下文中展开它；这样更容易阅读）。

isnt prfprf每当类型检查器能够p a = False自动生成证明（通过Refl上下文中的假设）时，就会驳回虚假证明。

一旦有了这些，您就可以通过仅枚举正面案例并添加一个包罗万象的方式来开始定义您的属性

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

您可以将原始谓词定义为使用Is适当的决策函数调用的类型别名：

WineStock : Fruit -> Type
WineStock = Is wineFruit

果然，它isnt可以让你忽略不可能的情况：

dismiss : WineStock Orange -> Void
dismiss = isnt