Agda: pattern matching equal variables?

Question

As a learning experience, I'm trying to implement a verified regular-expression matcher using continuation-passing style in Agda, based on the one proposed in this paper.

I've got a type for regular expressions defined like this:

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

And a type for a proof that a string matches an RE like this:

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)

I'm trying to write a correctness proof for my matcher, but I'm getting type errors on my pattern matches, before I even try to have a proof:

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 = ?

However, this gives the following error:

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

However, if I replace the underscores r2' with r2, I get a "repeated variables" error.

There is no way to construct a match for (r1 · r2) except the ConcatMatch constructor.

My question:

How do I convince the type-checker that r2 and r2' are equal, from within a pattern match? Any argument of type REMatch s1 (r1 · r2) must be constructed with the ConcatMatch constructor using arguments r1 and r2, but I don't know how to prove that this is the case from within a pattern match.

user3237465 user3237465 · Accepted Answer · 2015-05-06T00:58:46

That's why Agda has dot patterns:

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 _ _ _ = {!!}

I.e. just place . before the expression that supposed to be inferred. Or you can (and should) use implicit arguments:

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' _ _ _ _ _ = {!!}

However you'll probably encounter more complex problems, because you have touched the green slime (the terminology is due to Conor McBride):

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

Here is a similar and illustrative question.

Agda: pattern matching equal variables?

1 Answers