Построение доказательств для решающей функции в Идрисе - PullRequest
Новая
       92

Построение доказательств для решающей функции в Идрисе

0 голосов
/ 11 июня 2018

Я пытаюсь создать решающую функцию для типа, представляющего два последовательных элемента в модульном пространстве.

(Этот код получен из этого превосходного ответа на мой предыдущий вопрос.) 

data PreceedsN : Nat -> Nat -> Nat -> Type where
    PreceedsS : {auto prf : S a `LT` m} -> PreceedsN m a (S a)
    PreceedsZ : {auto prf : S a = m} -> PreceedsN m a Z

doesPreceedN : (m : Nat) -> (a : Nat) -> (b : Nat) -> Dec (PreceedsN m a b)
doesPreceedN m a b with (S a `cmp` m)
    doesPreceedN (S a + S d) a b     | CmpLT d with (S a `decEq` b)
        doesPreceedN (S a + S d) a b | CmpLT d | Yes prf = Yes ?bIsSa
        doesPreceedN (S a + S d) a b | CmpLT d | No contra = No ?bNotSa
    doesPreceedN (S m) m b     | CmpEQ   with (b `decEq` 0)
        doesPreceedN (S m) m Z | CmpEQ | Yes prf = Yes PreceedsZ
        doesPreceedN (S m) m b | CmpEQ | No contra = No ?saIsmAndbIsNotZ
    doesPreceedN (S m) (m + (S d)) b | CmpGT d = No ?saCannotBeGTm

Я приложил все усилия, но я еще недостаточно осведомлен, чтобы самостоятельно построить необходимые доказательства, особенно доказательства противоречия.Не могли бы вы рассказать мне, как заполнить одну или несколько лунок в приведенном выше коде?

Кроме того, если вы используете какие-либо удобные инструменты, такие как absurd, impossible или тактика , не могли бы вы объяснить, как они работают и какую роль они играют в доказательстве?

1 Ответ

0 голосов
/ 11 июня 2018

В то время как prf s в PreceedsN -конструкторе требуется LTE доказательство (LT a b - это просто синоним LTE (S a) b), ваш первый cmp просто разделяет S a.Вместо этого вы должны прямо получить LTE доказательство: 

doesPreceedN m a b with (S (S a) `isLTE` m)

Если вам не нужно повторно использовать все переменные, пропуск повторения в случаях with делает вещи немного красивее.Итак, чтобы повторить вашу версию с LTE, у нас есть: 

  | (Yes lte) = case (decEq b (S a)) of
      Yes Refl => PreceedsS
      No notlte => No ?contra_notlte
  | (No notlte) with (decEq (S a) m)
    | Yes eq = case b of
      Z => Yes PreceedsZ
      (S b) => No ?contra_notZ
    | No noteq = No ?contra_noteq

Во всех этих случаях вам нужно доказать некоторую a -> Void, так что вы можете предположить, что у вас есть a.Вы можете создать лемму (для этого у вашего редактора могут быть привязки) или использовать лямбду с разделением регистра.Для коротких функций, как здесь, я предпочитаю последнее.Для ?contra_notZ: 

No (\contra => case contra of prec => ?contra_notZ)

Если вы разделите на prec, у вас будет: 

No (\contra => case contra of PreceedsS => ?contra_notZ)

Осматривая отверстие, вы увидите, что у вас есть: 

notlte : LTE (S (S b)) m -> Void
prf : LTE (S (S b)) m

prf является неявным аргументом PreceedsS, поэтому, чтобы получить его в области видимости, вы можете сопоставить его с: 

No (\contra => case contra of (PreceedsS {prf}) => notlte prf)

?contra_noteq можно решить аналогично.

Лямбда для ?contra_notlte: 

No notlte => No (\contra => case contra of
  PreceedsS => ?contra_notlte_1
  PreceedsZ => ?contra_notlte_2)

Проверка типов дает: 

:t ?contra_notlte_1
notlte : (S a = S a) -> Void
:t ?contra_notlte_2
lte : LTE (S (S a)) m
prf : S a = m

?contra_notlte_2 самая хитрая, потому что вы не можете просто применить notlte.Но вы можете видеть, что после lte : LTE (S m) m должно быть значение false, поэтому мы создаем для него функцию: 

notLTE : Not (LTE (S n) n)
notLTE LTEZero impossible
notLTE (LTESucc lte) = notLTE lte

Теперь у нас есть: 

PreceedsZ {prf} => notLTE ?contra_notlte_2
?contra_notlte_2 : LTE (S n) n

Я попытался заменить отверстие на(rewrite prf in lte), но это не сработало, потому что тактика не нашла подходящего свойства для перезаписи.Но мы можем быть явно об этом: 

PreceedsZ {prf} => notLTE (replace prf lte)

> Type mismatch between
        LTE (S (S a)) m
and
        P (S a)

Таким образом, мы устанавливаем P явно, устанавливая {P=(\x => LTE (S x) m)}.

Результат: 

doesPreceedN : (m : Nat) -> (a : Nat) -> (b : Nat) -> Dec (PreceedsN m a b)
doesPreceedN m a b with (S (S a) `isLTE` m)
  | (Yes lte) = case (decEq b (S a)) of
    Yes Refl => Yes PreceedsS
    No notlte => No (\contra => case contra of
      PreceedsS => notlte Refl
      PreceedsZ {prf} => notLTE  (replace prf {P=(\x => LTE (S x) m)} lte))
  | (No notlte) with (decEq (S a) m)
    | Yes eq = case b of
      Z => Yes PreceedsZ
      (S b) => No (\contra => case contra of (PreceedsS {prf}) => notlte prf)
    | No noteq = No (\contra => case contra of 
        PreceedsS {prf} => notlte prf
        PreceedsZ {prf} => noteq prf)

replace : (x = y) -> P x -> P y просто переписывает часть типа.Например, с (n + m = m + n) мы можем заменить n + m часть Vect (n + m) a на Vect (m + n) a.Здесь P=\to_replace => Vect to_replace a, поэтому P - это просто функция Type -> Type.

В doesPreceedN нам нужно было явно указать P.Большую часть времени rewrite … in … (тактика) может найти это P автоматически и применить replace.replace с другой стороны - это просто простая функция :printdef replace: 

replace : (x = y) -> P x -> P y
replace Refl prf = prf
...