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

Я пишу основной монадический парсер в Идрисе, чтобы привыкнуть к синтаксису и отличиям от Haskell. У меня есть основы работы, которые работают нормально, но я застрял на попытке создания VerifiedSemigroup и VerifiedMonoid экземпляров для синтаксического анализатора.

Без лишнего внимания, здесь примеры парсера, полугруппы и моноиды, а также начало экземпляра VerifiedSemigroup.

data ParserM a          = Parser (String -> List (a, String))
parse                   : ParserM a -> String -> List (a, String)
parse (Parser p)        = p
instance Semigroup (ParserM a) where
    p <+> q             = Parser (\s => parse p s ++ parse q s)
instance Monoid (ParserM a) where
    neutral             = Parser (const []) 
instance VerifiedSemigroup (ParserM a) where
    semigroupOpIsAssociative (Parser p) (Parser q) (Parser r) = ?whatGoesHere

Я в основном застрял после intros со следующим состоянием проверки:

-Parser.whatGoesHere> intros
----------              Other goals:              ----------
{hole3},{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 a : Type
 p : String -> List (a, String)
 q : String -> List (a, String)
 r : String -> List (a, String)
----------                 Goal:                  ----------
{hole4} : Parser (\s => p s ++ q s ++ r s) =
          Parser (\s => (p s ++ q s) ++ r s)
-Parser.whatGoesHere>

Похоже, я должен как-то использовать rewrite вместе с appendAssociative но я не знаю, как "попасть внутрь" лямбда \s.

Во всяком случае, я застрял на теоретическом доказательстве части упражнения - и я не могу найти много Idris-ориентированной теоремы, подтверждающей документацию. Возможно, мне нужно начать изучать учебники Агды (хотя Идрис - это язык, набираемый в зависимости от языка, я убежден, что хочу учиться!).

Ответ 1

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

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, если дается эта аксиома?)

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

Жесткий вариант - работать с setoids. Сетоид - это в основном тип, снабженный обычным равенством. Идея состоит в том, что вместо наличия Monoid (или VerifiedSemigroup в вашем случае), который работает во встроенном равенстве (= в Idris, ≡ в 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

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