Problems on data type indices that uses list concatenation

Question

I'm having a nasty problem with a formalisation of a theorem that uses a data type that have some constructors whose indices have list concatenation. When I try to use emacs mode to case split, Agda returns the following error message:

I'm not sure if there should be a case for the constructor
o-success, because I get stuck when trying to solve the following
unification problems (inferred index ≟ expected index):
  e₁ o e'' , x₁ ++ x'' ++ y₁ ≟ e o e' , x ++ x' ++ y
  suc (n₂ + n'') , x₁ ++ x'' ≟ m' , p''
when checking that the expression ? has type
suc (.n₁ + .n') == .m' × .x ++ .x' == p'

Since the code is has more than a small number of lines, I put it on the following gist:

https://gist.github.com/rodrigogribeiro/976b3d5cc82c970314c2

Any tip is appreciated.

Best,

Answer 1

There was a similar question.

However you want to unify xs1 ++ xs2 ++ xs3 with ys1 ++ ys2 ++ ys3, but _++_ is not a constructor — it's a function, and it's not injective. Consider this simplified example:

data Bar {A : Set} : List A -> Set where
  bar : ∀ xs {ys} -> Bar (xs ++ ys)

ex : ∀ {A} {zs : List A} -> Bar zs -> Bar zs -> List A
ex (bar xs) b = {!!}

b is of type Bar (xs ++ .ys), but b is not necessarily equal to bar .xs, so you can't pattern-match like this. Here are two Bars, which have equal types but different values:

ok : ∃₂ λ (b1 b2 : Bar (tt ∷ [])) -> b1 ≢ b2
ok = bar [] , bar (tt ∷ []) , λ ()

This is because xs1 ++ xs2 ≡ ys1 ++ ys2 doesn't imply xs1 ≡ ys1 × xs2 ≡ ys2 in general.

But it's possible to generalize an index. You can use the technique described by Vitus at the link above, or you can use this simple combinator, which forgets the index:

generalize : ∀ {α β} {A : Set α} (B : A -> Set β) {x : A} -> B x -> ∃ B
generalize B y = , y

E.g.

ex : ∀ {A} {zs : List A} -> Bar zs -> Bar zs -> List A
ex {A} (bar xs) b with generalize Bar b
... | ._ , bar ys = xs ++ ys

After all, are you sure your lemma is true?

UPDATE

Some remarks first.

Your empty case states

empty : forall x -> G :: (emp , x) => (1 , x)

that the empty parser parses the whole string. It should be

empty : forall x -> G :: (emp , x) => (1 , [])

as in the paper.

Your definition of o-fail1 contains this part:

(n , fail ∷ o)

but fail fails everything, so it should be (n , fail ∷ []). With this representation you would probably need decidable equality on A to finish the lemma, and proofs would be dirty. Clean and idiomatic way to represent something, that can fail, is to wrap it in the Maybe monad, so here is my definition of _::_=>_:

data _::_=>_ {n} (G : Con n) : Foo n × List A -> Nat × Maybe (List A) -> Set where
  empty       : ∀ {x}     -> G :: emp   ,  x      => 1 , just []
  sym-success : ∀ {a x}   -> G :: sym a , (a ∷ x) => 1 , just (a ∷ [])
  sym-failure : ∀ {a b x} -> ¬ (a == b) -> G :: sym a , b ∷ x => 1 , nothing
  var         : ∀ {x m o} {v : Fin (suc n)}
              -> G :: lookup v G , x => m , o -> G :: var v , x => suc m , o
  o-success : ∀ {e e' x x' y n n'}
            -> G :: e      , x ++ x' ++ y => n            , just x
            -> G :: e'     ,      x' ++ y => n'           , just x'
            -> G :: e o e' , x ++ x' ++ y => suc (n + n') , just (x ++ x')
  o-fail1   : ∀ {e e' x x' y n}
            -> G :: e      , x ++ x' ++ y => n     , nothing
            -> G :: e o e' , x ++ x' ++ y => suc n , nothing
  o-fail2   : ∀ {e e' x x' y n n'}
            -> G :: e      , x ++ x' ++ y => n            , just x
            -> G :: e'     ,      x' ++ y => n'           , nothing
            -> G :: e o e' , x ++ x' ++ y => suc (n + n') , nothing

Here is the lemma:

postulate
  cut : ∀ {α} {A : Set α} -> ∀ xs {ys zs : List A} -> xs ++ ys == xs ++ zs -> ys == zs

mutual
  aux : ∀ {n} {G : Con n} {e e' z x x' y n n' m' p'}
      -> z == x ++ x' ++ y
      -> G :: e      , z       => n  , just x
      -> G :: e'     , x' ++ y => n' , just x'
      -> G :: e o e' , z       => m' , p'
      -> suc (n + n') == m' × just (x ++ x') == p'
  aux {x = x} {x'} {n = n} {n'} r pr1 pr2 (o-success {x = x''} pr3 pr4) with x | n | lemma pr1 pr3
  ... | ._ | ._ | refl , refl rewrite cut x'' r with x' | n' | lemma pr2 pr4
  ... | ._ | ._ | refl , refl = refl , refl
  aux ...

  lemma : ∀ {n m m'} {G : Con n} {f x p p'}
        -> G :: f , x => m , p -> G :: f , x => m' , p' -> m == m' × p == p'
  lemma (o-success pr1 pr2)  pr3            = aux refl pr1 pr2 pr3
  lemma ...

The proof proceeds as follows:

1. We generalize the type of lemma's pr3 in an auxiliary function as in the Vitus' answer. Now it's possible to pattern-match on pr3.
2. We prove, that the first parser in lemma's pr3 (called also pr3 in the aux) produces the same output as pr1.
3. After some rewriting, we prove that the second parser in lemma's pr3 (called pr4 in the aux) produces the same output as pr2.
4. And since pr1 and pr3 produce the same output, and pr2 and pr4 produce the same output, o-success pr1 pr2 and o-success pr3 pr4 produce the same output, so we put refl , refl.

The code. I didn't prove the o-fail1 and o-fail2 cases, but they should be similar.

UPDATE

Amount of boilerplate can be reduced by

1. Fixing the definitions of the fail cases, which contain redundant information.
2. Returning Maybe (List A) instead of Nat × Maybe (List A). You can compute this Nat recursively, if needed.
3. Using the inspect idiom instead of auxiliary functions.

I don't think there is a simpler solution. The code.