Доказательство Идриса о моде - PullRequest
Новая
       92

Доказательство Идриса о моде

0 голосов
/ 03 октября 2018

Я пытался написать в Idris доказательство относительно следующего оператора модуляции на основе вычитания: 

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_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

Я не знаком с приведенным синтаксисом Main.mod, helper (S x) 0 p x (minus (minus x 0) 1) 1в окне idris-hole .Я думаю, (S x) 0 p - это три параметра «mod», а (minus (minus x 0) 1) 1 - это три параметра локальной «вспомогательной» функции «mod»?

Кажется, пришло время использовать гипотезу индукции.Но как я могу закончить доказательство, используя индукцию?

1 Ответ

0 голосов
/ 08 октября 2018 
(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 nдля остатка в делении на 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)

Здесь для удобства я использовал auto implicits для доказательств того, чтоy > 0.

...