时间戳

首页 > 解决方案 > 关于 `mod` 的 Idris 证明

idris - 关于 `mod` 的 Idris 证明

问题描述

我试图在 Idris 中写一个关于以下基于减法的 mod 运算符的证明：

mod : (x, y : Nat) -> Not (y = Z) -> Nat
mod x Z p = void (p Refl)
mod x (S k) _ = if lt x (S k) then x else helper x (minus x (S k)) (S k)
  where total
        helper : Nat -> Nat -> Nat -> Nat
        helper Z x y = x
        helper (S k) x y = if lt x y then x else helper k (minus x y) y

我想证明的定理是上面“mod”产生的余数总是小于除法器。即，

mod_prop : (x, y : Nat) -> (p : Not (y=0))-> LT (mod x y p) y

我构建了一个证明，但被最后一个洞卡住了。我的完整代码粘贴在下面

    mod : (x, y : Nat) -> Not (y = Z) -> Nat
    mod x Z p = void (p Refl)
    mod x (S k) _ = if lt x (S k) then x else helper x (minus x (S k)) (S k)
      where total
            helper : Nat -> Nat -> Nat -> Nat
            helper Z x y = x
            helper (S k) x y = if lt x y then x else helper k (minus x y) y
    
    lteZK : LTE Z k
    lteZK {k = Z} = LTEZero
    lteZK {k = (S k)} = let ih = lteZK {k=k} in
                        lteSuccRight {n=Z} {m=k} ih 
    
    lte2LTE_True : True = lte a b -> LTE a b
    lte2LTE_True {a = Z} prf = lteZK
    lte2LTE_True {a = (S _)} {b = Z} Refl impossible
    lte2LTE_True {a = (S k)} {b = (S j)} prf = 
      let ih = lte2LTE_True {a=k} {b=j} prf in LTESucc ih

    
    lte2LTE_False : False = lte a b -> GT a b
    lte2LTE_False {a = Z} Refl impossible
    lte2LTE_False {a = (S k)} {b = Z} prf = LTESucc lteZK
    lte2LTE_False {a = (S k)} {b = (S j)} prf = 
      let ih = lte2LTE_False {a=k} {b=j} prf in (LTESucc ih)
    
    total
    mod_prop : (x, y : Nat) -> (p : Not (y=0))-> LT (mod x y p) y
    mod_prop x Z p = void (p Refl)
    mod_prop x (S k) p with (lte x k) proof lxk
      mod_prop x (S k) p | True  = LTESucc (lte2LTE_True lxk)
      mod_prop Z (S k) p | False = LTESucc lteZK 
      mod_prop (S x) (S k) p | False with (lte (minus x k) k)  proof lxk'
        mod_prop (S x) (S k) p | False | True = LTESucc (lte2LTE_True lxk')
        mod_prop (S x) (S Z) p | False | False  = LTESucc ?hole

运行类型检查器后，该孔的描述如下：

- + Main.hole [P]
 `--          x : Nat
              p : (1 = 0) -> Void
            lxk : False = lte (S x) 0
           lxk' : False = lte (minus x 0) 0
     --------------------------------------------------------------------------
      Main.hole : LTE (Main.mod, helper (S x) 0 p x (minus (minus x 0) 1) 1) 0

我不熟悉idris-holes窗口中Main.mod, helper (S x) 0 p x (minus (minus x 0) 1) 1给出的语法。我猜是“mod”的三个参数，而“mod”的本地“helper”函数的三个参数是？(S x) 0 p(minus (minus x 0) 1) 1

似乎是时候利用归纳假设了。但是我怎样才能用归纳法完成证明呢？

标签： idristheorem-proving

解决方案

(Main.mod, helper (S x) 0 p x (minus (minus x 0) 1) 1)

可以读作

  • Main.mod, helper- 函数的限定名称，在helper函数的where子句中定义mod（Main是模块名称）；
  • 其中的参数mod也传递给helper-(S x)和0（p参见文档）：

在外部范围内可见的任何名称在 where 子句中也可见（除非它们已被重新定义，例如此处的 xs）。仅出现在类型中的名称如果是其中一种类型的参数，则将在 where 子句的范围内，即它在整个结构中是固定的。

  • 自身的参数helper-x和。(minus (minus x 0) 1)1

下面还有另一个实现，mod它使用Fin ntype 作为除以的余数n。事实证明更容易推理，因为 的任何值Fin n总是小于n：

import Data.Fin

%default total


mod' : (x, y : Nat) -> {auto ok: GT y Z} -> Fin y
mod' Z (S _) = FZ
mod' (S x) (S y) with (strengthen $ mod' x (S y))
    | Left _ = FZ
    | Right rem = FS rem

mod : (x, y : Nat) -> {auto ok: GT y Z} -> Nat
mod x y = finToNat $ mod' x y

finLessThanBound : (f : Fin n) -> LT (finToNat f) n
finLessThanBound FZ = LTESucc LTEZero
finLessThanBound (FS f) = LTESucc (finLessThanBound f)

mod_prop : (x, y : Nat) -> {auto ok: GT y Z} -> LT (mod x y) y
mod_prop x y = finLessThanBound (mod' x y)

这里为方便起见，我使用自动隐式来证明y > 0.

推荐阅读