#idris #typechecking #theorem-proving
#idris #проверка типов #доказательство теоремы
Вопрос:
Тестирование «простого» примера типов идентификаторов, равенства мод, но доказательство транзитивности не будет проверять тип даже из шаблона. Больше, чем исправление, я хочу знать, почему?
Вот фрагмент минимальной проблемы
data ModEq : (n:Nat) -> (x:Nat) -> (y:Nat) -> Type where
{- 3 constructors
reflexive: x == x (mod n),
left-induct: x == y (mod n) => (x n) == y (mod n)
right-induct: x == y (mod n) => x == (y n) (mod n)
-}
Reflex : (x:Nat) -> ModEq n x x --- Needs syntatic sugar, for now prefix
LInd : (ModEq n x y) -> ModEq n (x n) y
RInd : (ModEq n x y) -> ModEq n x (y n)
{----- Proof of transitive property. -----}
total
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
{- x=x amp; x=y => x=y -}
isTrans (Reflex x) v = v
isTrans u (Reflex y) = u
{- ((x=y=>(x n)=y) amp; y=z) => x=y amp; y=z => x=z (induct) => (x n)=z -}
isTrans (LInd u) v = LInd (isTrans u v)
isTrans u (RInd v) = RInd (isTrans u v)
{- (x=y=>x=(y n)) amp; (y=z=>(y n)=z) => x=y amp; y=z => x=z (induct) -}
isTrans (RInd u) (LInd v) = isTrans u v
Несоответствие типов находится в последней строке, хотя из строки комментария я действительно не могу сказать, почему логически это неправильно. Вот ошибка:
48 | isTrans (RInd u) (LInd v) = isTrans u v
| ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
Type mismatch between
ModEq n (x n) z (Type of LInd v)
and
ModEq n (y n) z (Expected type)
Specifically:
Type mismatch between
plus x n
and
plus y n
Я не только смущен тем, как LInd v
был назначен (неправильный кажущийся) тип ModEq n (x n) z, но я указываю, что когда я просто пытаюсь использовать подход «тип-определение-уточнение» со встроенным шаблоном, я получаю:
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
И даже это не будет проверять тип, оно жалуется:
40 | isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
| ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
Type mismatch between
ModEq n (x n) z (Type of LInd _)
and
ModEq n (y n) z (Expected type)
Specifically:
Type mismatch between
plus x n
and
plus y n
Ответ №1:
Проблема в том, что компилятор не может вывести в вашем последнем случае это y = {x n}
. Однако вы можете дать ему этот намек:
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (Reflex _) v = v
isTrans u (Reflex _) = u
isTrans (LInd u) v = LInd $ isTrans u v
isTrans u (RInd v) = RInd $ isTrans u v
isTrans (RInd u) (LInd v) {n} {x} {y = x n} = ?isTrans_rhs
Что дает вам следующую цель для isTrans_rhs
:
x : Nat
n : Nat
u : ModEq n x x
z : Nat
v : ModEq n x z
--------------------------------------
isTrans_rhs : ModEq n x z
и, таким образом, вы можете заключить isTrans (RInd u) (LInd v) {n} {x} {y = x n} = v
Комментарии:
1. Ах! Так что это потому, что моя ошибка была с неявными аргументами, а имплициты не являются частью автоматически сгенерированного шаблона. Так что даже это приведет к сбою. Теперь это имеет смысл. Спасибо!