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

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

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 (и наоборот). Возможно, это ошибка, или я что-то упустил?


pattern-matching idris proof
person Sventimir    schedule 10.02.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

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

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

person Cactus    schedule 11.02.2019
comment
Тем не менее, несмотря на то, что есть только один шаблон соответствия plus l Zero, чем бы это l было? Питти. В любом случае, спасибо за объяснение. - person Sventimir; 11.02.2019
comment
Но plus l Zero может соответствовать либо первому предложению plus (если l = Zero), либо второму, поскольку предложения сопоставления с образцом упорядочены. - person Cactus; 11.02.2019
comment
Ах, теперь я понял! Спасибо :) - person Sventimir; 11.02.2019