如何证明复杂表达式和“真”之间的命题相等？

编程问答 2022-04-22

问题描述

我有一些看起来像这样的代码：

allLessthan : Ord t => (v1 : Vect n t) -> (v2 : Vect n t) -> Bool
allLessthan v1 v2 = all (\(x,y) => x < y) (zip v1 v2)

unravelIndexUnsafe : (order : ArrayOrder) ->
                     (shape : ArrayShape (S n)) ->
                     (position : Vect (S n) Nat) ->
                     Nat
unravelIndexUnsafe order shape position = ?someImplementation

unravelIndexSafe : (order : ArrayOrder) ->
                   (shape : ArrayShape (S n)) ->
                   (position : Vect (S n) Nat) ->
                   {auto 0 prfPositionValid : (allLessthan position shape) = True} ->
                   Nat
unravelIndexSafe order shape position = unravelIndexUnsafe order shape position

unravelIndex : (order : ArrayOrder) ->
               (shape : ArrayShape (S n)) ->
               (position : Vect (S n) Nat) ->
               Maybe Nat
unravelIndex order shape position =
  case allLessthan position shape of
    True => Just $ unravelIndexSafe order shape position
    False => nothing

我省略了 unravelIndexUnsafe 的实现，我认为这与问题无关。

我在 unravelIndex 的定义中遇到类型错误，说它找不到 prfPositionValid 与 unravelIndexSafe* 一起使用的实现。

这让我感到惊讶，因为我在 allLessthan position shape 上明确区分大小写，并且只在 unravelIndexSafe 分支中调用 True。我希望 Idris 能够从这些信息中推断出命题 (allLessthan position shape) = True 成立。

有没有直接的方法来解决这个问题？也许我可以显式构造并传递 prfPositionValid 隐式参数？或者我应该在这里使用完全不同的方法吗？我是否需要以不同的方式表达 prfPositionValid 或 allLessthan？我需要rewrite什么吗？

* 更准确地说，它找不到prfPositionValid这个可怕的“完全扩展”版本的实现：

foldl (\acc,elem => acc && Delay (case block in allLessthan (S n) Nat (MkOrd (\{arg:354},{arg:355} => compare arg arg) (\{arg:356},{arg:357} => == (compare arg arg) LT) (\{arg:358},{arg:359} => == (compare arg arg) GT) (\{arg:360},{arg:361} => not (== (compare arg arg) GT)) (\{arg:362},{arg:363} => not (== (compare arg arg) LT)) (\{arg:364},{arg:365} => if == (compare arg arg) GT then x else y) (\{arg:366},{arg:367} => if == (compare arg arg) LT then x else y)) shape position elem)) True (zipwith (\{__leftTupleSection:0},{__infixTupleSection:0} => (__leftTupleSection,__infixTupleSection)) position shape) = True

解决方法

解决方案：使用可判定等式

答案是使用“可判定的平等”，因为伊德里斯不像人类那么聪明。

请注意，特殊的 = 语法等效于内置运算符 (===)，它等效于类型 Equal。 Equal 的构造函数是 Refl。为了证明 Equal a b 形式的命题，Idris 必须能够弄清楚 a 和 b 实际上是同一件事（称之​​为 c）。如果您可以使用类型 Refl c 调用 Equal a b，那么您已经证明了 Equal a b。相反，获得 Equal a b 实例的唯一方法是调用 Refl c。

Idris 2 不能通过 case-splitting 推断命题相等。我，一个人类，知道我们试图证明 allLessThan position shape 在命题上等于 True。在 Idris 中，这意味着我们希望能够编写 Refl True。 allLessThan position shape 上的大小写拆分确实会导致 Bool，但这本身并不构成对 Refl True 类型的 Equal (allLessThan position shape) True 调用。因此，原始代码中的大小写拆分不足以让 Idris 推断出 Equal (allLessThan position shape) True 的证明。

我们知道 allLessThan position shape 是一个可判定谓词，因此我们可以使用 decEq 来获得我们需要的证明/实现。因此我们可以将 unravelIndex 写成：

unravelIndex : (order : ArrayOrder) ->
               (shape : ArrayShape (S n)) ->
               (position : Vect (S n) Nat) ->
               Maybe Nat
unravelIndex order shape position =
  case decEq (allLessThan position shape) True of
    Yes proof => Just $ unravelIndexSafe order shape position
    No contra => Nothing

proof 中的 Yes proof 正是我们要寻找的 Refl True，它实现了 Equal (allLessThan position shape) True。因此，Idris 将能够为 prfPositionValid 自动隐式推断一个值，因为在范围内可以使用正确类型的值。

您也可以用 _ 代替 proof 和 contra，因为证明在代码中的任何地方都没有明确使用，因此它们不需要名称。

重构

请注意，此 allLessThan position shape 有点临时。特别是，说明属性的条件需要程序员记住特定的表达式。但是我们想编写一个更简洁的 API，其中程序员可以调用函数 isPositionValidForShape 来检查有效性，并使用类型 IndexValidForShape 来表示“有效”状态。

allLessThan : Ord t => (v1 : Vect n t) -> (v2 : Vect n t) -> Bool
allLessThan v1 v2 = all (\(x,y) => x < y) (zip v1 v2)

IndexValidForShape : (shape : ArrayShape ndim) ->
                     (position : ArrayIndex ndim) ->
                     Type
IndexValidForShape shape position =
  let isValid = allLessThan position shape
  in Equal isValid True

isIndexValidForShape : (shape : ArrayShape (S n)) ->
                       (position : ArrayIndex (S n)) ->
                       Dec (IndexValidForShape shape position)
isIndexValidForShape shape position =
  decEq (allLessThan position shape) True

unravelIndexUnsafe : (order : ArrayOrder) ->
                     (shape : ArrayShape (S n)) ->
                     (position : ArrayIndex (S n)) ->
                     Nat
unravelIndexUnsafe order shape position =
  sum $ zipWith (*) (strides order shape) position

unravelIndexSafe : (order : ArrayOrder) ->
                   (shape : ArrayShape (S n)) ->
                   (position : ArrayIndex (S n)) ->
                   {auto 0 prfIndexValid : IndexValidForShape shape position} ->
                   Nat
unravelIndexSafe order shape position =
  unravelIndexUnsafe order shape position

unravelIndex : (order : ArrayOrder) ->
               (shape : ArrayShape (S n)) ->
               (position : ArrayIndex (S n)) ->
               Maybe Nat
unravelIndex order shape position =
  case isIndexValidForShape shape position of
    Yes _ => Just $ unravelIndexSafe order shape position
    No _ => Nothing

现在，最终用户不必知道或关心 IndexValidForShape 究竟意味着什么，或者您需要使用 allLessThan 来检查它。

事实上，我们现在可以改变索引“有效”的含义，主要是不影响下游代码用户；也许我想实施额外的检查，只有在我发现逻辑错误后才能了解。

或者，应该可以将 IndexValidForShape 重新设计为更加“结构化”，其中您可以归纳地定义表示所需属性的数据类型。例如，请参阅类型驱动开发第 9 章中的 Data.Vect.Elem 及其说明。

词汇表

  • decidable：“如果您始终可以说出该属性是否适用于某些特定值，那么该属性就是可判定的”（引自类型驱动开发，第 245 页）。
  • Dec：表示可判定属性有效性的类型。它的构造函数是：
    • Yes : property -> Dec property - property 持有。
    • No : (property -> Void) -> Dec property - property 是一个矛盾。
  • DecEq：数据类型的接口，其相等性可以确定为可判定属性。
  • decEq：DecEq 的方法，用于确定两个事物是否可确定相等。它的类型是 DecEq t => (x1 : t) -> (x2 : t) -> Dec (Equal x1 x2)。

参考资料和进一步阅读

dependent-typeidrisidrisidristheorem-proving