Простейший пример проблемы (но не единственный, который я могу продемонстрировать): предположим, что мне дана функция более высокого порядка f : (a -> b) -> c. Я хотел бы доказать, что f = (\g => f (\x => g x)).
По моим собственным соображениям, это должно быть довольно просто: просто примените eta-эквивалентность дважды (один раз внутри, а затем снаружи).
ЕслиЯ хотел доказать f = (\x => f x), простого Refl было бы достаточно: это привело меня к мысли, что «Идрис знает об этой-эквивалентности». Но с другой стороны, то же решение не сработало для f = (\g => f (\x => g x)).
. В тот момент я попытался использовать rewrite, но не смог найти ссылку на g в (\g => f (\x => g x)):
lemma : {g : a -> b} -> g = (\x => g x)
lemma = Refl
theorem : {f : (a -> b) -> c} ->
f = (\g => f (\x => g x))
theorem = rewrite (lemma {g = _}) in Refl
Но, конечно, Идрис не может понять, каким должен быть _, и я тоже.
Это может быть дополнительно сведено к проблеме доказывания (\g => f g) = (\g => f (\x => g x)), конечно, потому что Идрис знает, что равенство транзитивно и знает об eta-эквивалентности (по крайней мере, когда она не «скрыта» в лямбда-абстракциях).
Я начинаю верить, что то, что я испытываючто-то происходит, потому что Идрис не знает о расширении: есть ли другой способ доказать это (без изменения понятия равенства, которое я использую, например, с помощью сетоидов)?
Я использую Идрис 1.3.2 из мерзавца.