Как мне доказать, казалось бы, очевидный факт, когда соответствующие типы абстрагируются лямбдой в Идрисе?

Ответ прост: вы не можете. Рассуждения о функциях довольно неудобны в теориях интенсионального типа. Например, теория типов Мартина-Лёфа не может доказать:

S x + y = S (x + y)
0   + y = y

x +′ S y = S (x + y)
x +′ 0   = x

_+_ ≡ _+′_  -- ???

(насколько мне известно, это реальная теорема, а не просто «доказательство отсутствия воображения»; однако я не смог найти источник, где я ее прочитал). Это также означает, что нет никаких доказательств для более общего:

ext : ∀ {A : Set} {B : A → Set}
        {f g : (x : A) → B x} →
        (∀ x → f x ≡ g x) → f ≡ g

Это называется расширяемостью функции: если вы можете доказать, что результаты равны для всех аргументов (то есть функции равны экстенсивно), то функции также равны.

Это отлично подойдет для вашей проблемы:

<+>-assoc : {A : Set} (p q r : ParserM A) →
  (p <+> q) <+> r ≡ p <+> (q <+> r)
<+>-assoc (Parser p) (Parser q) (Parser r) =
  cong Parser (ext λ s → ++-assoc (p s) (q s) (r s))

где ++-assoc - ваше доказательство ассоциативности свойства _++_. Я не уверен, как это будет выглядеть с точки зрения тактики, но это будет довольно похоже: примените сравнение для Parser, и цель должна быть такой:

(\s => p s ++ q s ++ r s) = (\s => (p s ++ q s) ++ r s)

Затем вы можете применить расширяемость, чтобы получить предположение s : String и цель:

p s ++ q s ++ r s = (p s ++ q s) ++ r s

Однако, как я сказал ранее, у нас нет расширяемости функций (обратите внимание, что это неверно для теорий типов в целом: теории экстенсиональных типов, теории гомотопических типов и другие могут доказать это утверждение). Самый простой вариант - принять это как аксиому. Как и в случае с любой другой аксиомой, вы рискуете:

• Потеря согласованности (т. Е. Возможность доказать ложность; хотя я думаю, что расширяемость функции в порядке)

• Прерывание редукции (что делает функция, которая выполняет анализ случаев только для refl, при данной аксиоме?)

Я не уверен, как Идрис трактует аксиомы, поэтому не буду вдаваться в подробности. Только помните, что аксиомы могут кое-что испортить, если вы не будете осторожны.

Сложный вариант - работать с сетоидами. Сетоид - это, по сути, тип, снабженный настраиваемым равенством. Идея состоит в том, что вместо Monoid (или VerifiedSemigroup в вашем случае), который работает со встроенным равенством (= в Идрисе, ≡ в Agda), у вас есть специальный моноид (или полугруппа) с другим базовым равенством. Обычно это делается путем упаковки операций моноида (полугруппы) вместе с равенством и кучей доказательств, а именно (в псевдокоде):

=   : A → A → Set  -- equality
_*_ : A → A → A    -- associative binary operation
1   : A            -- neutral element

=-refl  : x = x
=-trans : x = y → y = z → x = z
=-sym   : x = y → y = x

*-cong : x = y → u = v → x * u = y * v  -- the operation respects
                                        -- our equality

*-assoc : x * (y * z) = (x * y) * z
1-left  : 1 * x = x
1-right : x * 1 = x

Выбор равенства для парсеров очевиден: два парсера равны, если их выходы совпадают для всех возможных входов.

-- Parser equality
_≡p_ : {A : Set} (p q : ParserM A) → Set
Parser p ≡p Parser q = ∀ x → p x ≡ q x

Это решение имеет разные компромиссы, а именно то, что новое равенство не может полностью заменить встроенное (это обычно проявляется, когда вам нужно переписать некоторые термины). Но это здорово, если вы просто хотите показать, что ваш код делает то, что должен делать (с точностью до некоторого пользовательского равенства).