Как вы оперируете зависимыми парами в доказательстве? - PullRequest
Новая
       6

Как вы оперируете зависимыми парами в доказательстве?

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

Это продолжение до этого вопроса .Благодаря Кварцу у меня теперь есть состояние предложения, если b делит a, то b делит a * c для любого целого числа c, а именно: 

alsoDividesMultiples : (a, b, c : Integer) ->
                       DivisibleBy a b ->
                       DivisibleBy (a * c) b

Теперь цель состояла в том, чтобы доказать это утверждение.Я понял, что не понимаю, как действовать на зависимых парах.Я попробовал более простую задачу, которая показала, что каждое число делится на 1. После постыдного количества размышлений об этом, Я думал Я нашел решение: 

-- All numbers are divisible by 1.
DivisibleBy a 1 = let n = a in
  (n : Integer ** a = 1 * n)

Это компилируется, но у меня были сомнения, что это действительно.Чтобы убедиться, что я был неправ, он немного изменил его на: 

-- All numbers are divisible by 1.
DivisibleBy a 1 = let n = a in
  (n : Integer ** a = 2 * n)

Это также компилирует, что означает, что моя «английская» интерпретация, безусловно, неверна, поскольку я бы интерпретировал это как «Все числа делятся на однопоскольку каждое число в два раза больше другого целого числа ".Таким образом, я не совсем уверен, что я демонстрирую этим заявлением.Итак, я вернулся и попробовал более традиционный способ постановки проблемы: 

oneDividesAll : (a : Integer) ->
                (DivisibleBy a 1)
oneDividesAll a = ?sorry

Для реализации oneDividesAll Я не совсем уверен, как «внедрить» тот факт, что (n = a).Например, я бы написал (на английском языке) это доказательство как:

Мы хотим показать, что 1 |а.Если это так, из этого следует, что a = 1 * n для некоторого n.Пусть n = a, затем a = a * 1, что верно для идентичности.

Я не уверен, как на самом деле сказать: «Подумайте, когда n = a».Насколько я понимаю, тактика rewrite требует доказательства того, что n = a.

Я попытался адаптировать свое ошибочное доказательство: 

oneDividesAll : (a : Integer) ->
                (DivisibleBy a 1)
oneDividesAll a = let n = a in (n : Integer ** a = b * n)

Но это дает: 

   |
12 | oneDividesAll a = let n = a in (n : Integer ** a = b * n)
   |                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of oneDividesAll with expected type
        DivisibleBy a 1

Type mismatch between
        Type (Type of DPair a P)
and
        (n : Integer ** a = prim__mulBigInt 1 n) (Expected type)

Любая помощь / подсказки будут оценены.

1 Ответ

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

Прежде всего, если вы хотите доказать свойства по числу, вы должны использовать Nat (или другие индуктивные типы).Integer использует примитивы, которые аргумент не может аргументировать дальше, чем prim__mulBigInt : Integer -> Integer -> Integer;что вы передаете два Integer, чтобы получить один.Компилятор не знает ничего как выглядит полученный Integer, поэтому он не может доказать что-либо об этом.

Так что я пойду с Nat: 

DivisibleBy : Nat -> Nat -> Type
DivisibleBy a b = (n : Nat ** a = b * n)

Опять же, это утверждение, а не доказательство.DivisibleBy 6 0 является допустимым типом, но вы не найдете proof : Divisible 6 0.Таким образом, вы были правы с 

oneDividesAll : (a : Nat) ->
                (DivisibleBy a 1)
oneDividesAll a = ?sorry

С этим вы можете генерировать доказательства вида oneDividesAll a : DivisibleBy a 1.Итак, что входит в отверстие ?sorry?:t sorry дает нам sorry : (n : Nat ** a = plus n 0) (что является DivisibleBy a 1 разрешенным, насколько может Идрис).Вы запутались в правой части пары: x = y - это тип, но теперь нам нужно значение - вот на что намекает ваше последнее зашифрованное сообщение об ошибке).= имеет только один конструктор, Refl : x = x.Таким образом, нам нужно привести обе стороны равенства к одному значению, чтобы результат выглядел примерно так: (n ** Refl).

Как вы и думали, нам нужно установить n в a: 

oneDividesAll a = (a ** ?hole)

Для необходимой тактики переписывания мы проверим :search plus a 0 = a, и увидим, что plusZeroRightNeutral имеет правильный тип. 

oneDividesAll a = (a ** rewrite plusZeroRightNeutral a in ?hole)

Теперь :t hole дает нам hole : a = a, поэтому мы можем простоавтозаполнение до Refl: 

oneDividesAll a = (a ** rewrite plusZeroRightNeutral a in Refl)

Хороший учебник по доказательству теорем (где также объясняется, почему plus a Z не уменьшает) находится в Idris Doc .

...