Анализ случая в доказательствах Идриса - PullRequest
Новая
       27

Анализ случая в доказательствах Идриса

0 голосов
/ 10 февраля 2019

Итак, я написал следующий тип, чтобы доказать некоторые свойства целых чисел: 

data Number : Type where
    PosN : Nat -> Number
    Zero : Number
    NegN : Nat -> Number

plusPosNeg : Nat -> Nat -> Number
plusPosNeg n m with (cmp n m)
    plusPosNeg (k + S d) k  | CmpGT d = PosN d
    plusPosNeg k k          | CmpEQ = Zero
    plusPosNeg k (k + S d)  | CmpLT d = NegN d

plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = plusPosNeg k j
plus (NegN k) (PosN j) = plusPosNeg j k

Теперь я хотел бы доказать, что Zero является нейтральным элементом сложения, что вполне очевидно изопределение plus.И действительно, Идрис принимает следующее доказательство: 

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l = Zero} = Refl
plusRZeroNeutral {l = PosN _} = Refl
plusRZeroNeutral {l = NegN _} = Refl

Но отвергает более короткую версию, которую я впервые придумала: 

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l} = Refl

Мой вопрос: почему это так?Глядя на определение plus, может показаться, что компилятор должен знать, что конструктор, переданный в качестве правого аргумента plus, не имеет значения, если левый аргумент равен Zero (и наоборот).Возможно, это ошибка, или я что-то упустил?

1 Ответ

0 голосов
/ 11 февраля 2019

Если все, что вы знаете о l, это то, что это, ну, в общем, l (то есть некоторый произвольный параметр), тогда вы не сможете уменьшить plus l Zero дальше, так как вы застряли на какой ветви plus принять.

Когда вы сопоставляете шаблон, например, с l = Zero, тип правой стороны теперь уточняется до plus Zero Zero = Zero, который может быть уменьшен (через определение plus) до Zero = Zero.Тип конструктора Refl легко объединяется с этим уточненным типом результата, и поэтому проверка типов plusRZeroNeutral {l = Zero} = Refl проверяется.

Другие ветви аналогично обрабатываются другими пунктами вашего первого определения plusRZeroNeutral.

...