Agda: соответствие шаблону равным переменным?

Question

Как опыт обучения, я пытаюсь реализовать проверенный регулярный выражетель, используя стиль продолжения прохождения в Agda, на основе предложенного в this paper.

У меня есть тип регулярных выражений определены следующим образом:

data RE : Set where 
    ε : RE 
    ∅ : RE 
    Lit : Char -> RE 
    _+_ : RE -> RE -> RE 
    _·_ : RE -> RE -> RE 
    _* : RE -> RE 

и типа для доказательства того, что строка соответствует УЭ так:

data REMatch : List Char -> RE -> Set where 
    EmptyMatch : REMatch [] ε 
    LitMatch : (c : Char) -> REMatch (c ∷ []) (Lit c) 
    ... 
    ConcatMatch : 
    (s1 : List Char) (s2 : List Char) (r1 : RE) (r2 : RE) 
    -> REMatch s1 r1 
    -> REMatch s2 r2 
    -> REMatch (s1 ++ s2) (r1 · r2) 

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

accCorrect : 
    (r : RE) (s : List Char) (s1 : List Char) (s2 : List Char) (k : (List Char -> Bool)) 
    -> ((s1 ++ s2) ≡ s) 
    -> (REMatch s1 r) 
    -> (k s2 ≡ true) 
    -> (acc r s k ≡ true) 
accCorrect ε [] [] [] k _ EmptyMatch kproof = kproof 
accCorrect (r1 · r2) s s1 s2 k splitProof (ConcatMatch s1' s1'' r1' r2' subMatch1 subMatch2) kproof = ? 

Однако, это дает следующее сообщение об ошибке:

r2' != r2 of type RE 
when checking that the pattern 
ConcatMatch s1' s1'' r1' r2' subMatch1 subMatch2 has type 
REMatch s1 (r1 · r2) 

Однако, если я заменю подчеркивание r2' с r2, я получаю ошибку «повторяющиеся переменные».

Невозможно построить соответствие для (r1 · r2), за исключением конструктора ConcatMatch.

Мой вопрос:

Как убедить типа Проверку что r2 и r2' равны, в рамках матча картины? Любой аргумент типа REMatch s1 (r1 · r2) должен быть сконструирован с помощью конструктора ConcatMatch с использованием аргументов r1 и r2, но я не знаю, как доказать, что это так из-за соответствия шаблону.

Answer 1

Вот почему Agda имеет точечные узоры:

accCorrect : 
    (r : RE) (s : List Char) (s1 : List Char) (s2 : List Char) (k : (List Char -> Bool)) 
    -> ((s1 ++ s2) ≡ s) 
    -> (REMatch s1 r) 
    -> (k s2 ≡ true) 
    -> (acc r s k ≡ true) 
accCorrect (.r1 · .r2) s ._ s2 k splitProof (ConcatMatch s1' s1'' r1 r2 subMatch1 subMatch2) kproof = {!!} 
accCorrect _ _ _ = {!!} 

И.Э. просто поставьте . перед выражением, которое должно быть выведено. Или вы можете (и должны) использовать неявные аргументы:

accCorrect' : 
    {r : RE} (s : List Char) {s1 : List Char} (s2 : List Char) (k : (List Char -> Bool)) 
    -> ((s1 ++ s2) ≡ s) 
    -> (REMatch s1 r) 
    -> (k s2 ≡ true) 
    -> (acc r s k ≡ true) 
accCorrect' s s2 k splitProof (ConcatMatch s1' s1'' r1 r2 subMatch1 subMatch2) kproof = {!!} 
accCorrect' _ _ _ _ _ = {!!} 

Однако вы, вероятно, сталкиваются с более сложными проблемами, потому что вы коснулись зеленой слизью (терминология связана с Конор МакБрайд):

The presence of ‘green slime’ — defined functions in the return types of constructors — is a danger sign.

Пример аналогичный и иллюстративный question.