[Agda] Panic: CanSplit

[jp.beaumont at student.qut.edu.au]

I don't think this is any better, however, it does avoid defining multiple versions 
of <= so maybe it's of some use to you. To avoid the issues with pattern matching 
on the inequality proof you can introduce a new variable which is constrained to 
equal "fs i". This new variable will then be able to unify with the "inj i" 
resulting from pattern matching on the inequality proof. The rest of the proof 
pretty much follows the expected pattern then.

fsLeftLt : forall {n : Nat} (i : Fin n) (j : Fin (Succ n)) {k : Fin (Succ n)} 
               -> k <= j -> k ≡ fs i → inj i <= j
fsLeftLt i        .(fs i) Base               refl = Step _ _ Base
fsLeftLt i        .(fs j) (Step fz     j lt) ()
fsLeftLt .(inj i) .(fs j) (Step (fs i) j lt) refl = Step _ _ (fsLeftLt i j lt refl) 

fsLtLemma : forall {n : Nat} (i j : Fin n) {k : Fin (Succ n)} 
                -> k <= fs j -> k ≡ fs i -> i <= j
fsLtLemma i        .i Base                refl = Base
fsLtLemma i        j  (Step fz .j y)      ()
fsLtLemma .(inj i) j  (Step (fs i) .j lt) refl = fsLeftLt i j lt refl

fsLt : forall {n : Nat} (i j : Fin n) -> fs i <= fs j -> i <= j
fsLt i j lt = fsLtLemma i j lt refl

> From: Wouter Swierstra < wouter at chalmers.se>
> Subject: Re: [Agda] Panic: CanSplit
> To: Ulf Norell <ulf.norell at gmail.com>
> Cc: Agda List <agda at lists.chalmers.se>
>
> >
> >  Panic: CantSplit Tmp.Step
> >
> > Is this with a recent version of Agda? I thought I had fixed these
> > error messages to make more sense.
>
> Updating Agda resulted in a much better error message - thanks Ulf!
>
> I managed to solve my original problem this morning by defining the
> following alternative version of less-than-or-equal-to:
>
> > data _<=_ : {n : Nat} -> Fin n -> Fin n -> Set where
> >  Base : forall {n : Nat} {i : Fin n} -> fz <= i
> >  Step : forall {n : Nat} (i j : Fin n) -> i <= j -> fs i <= fs j
>
> and showing that the two definitions are equivalent. I can't help but
> wonder if there is some clever trick I'm missing.
>
>   Wouter
>
> ------------------------------