[Agda] Re: induction recursion - normalisation

[Ondrej Rypacek]

I already know a part of the answer:


> Strangely, the symmetrical case below, in the definition of tgt, i.e.
>
> tgt fzero (alpha x y z yz xy) = comp fzero x (comp fzero y z yz) xy
>
> works fine. Why? What's the difference ?

The difference is the order of their definition: when I swap them,
it's again the first one in the file which fails. I find it odd, but I
know nothing about the way mutual recursion is implemented.

Is there any way around this behaviour of mutual recursion ? Cause
otherwise the recursion is imho well defined.


Cheers, Ondrej


> Any ideas what's wrong and how to fix it ?
>
>
> Cheers,
> Ondrej
>
> -------
>
> {-# OPTIONS --no-termination-check #-}
>
> module globSetCat where
>
> open import Data.Nat
> open import Data.Fin hiding (#_;_<_) renaming (suc to fsuc;zero to fzero)
> open import Data.Product
> open import Data.Empty
> open import Data.Unit hiding (tt ; _≤_ )
> open import Relation.Binary.PropositionalEquality
>
>
> -- a category structure on a set
> record GlobularSet : Set₁ where
>  field
>    #_ : ℕ → Set
>    src : ∀ {n} → # (suc n) → # n
>    tgt : ∀ {n} → # (suc n) → # n
>
>    ss-st : ∀ {n x} → src {suc (suc n)} (src x) ≡ src (tgt x)
>    ts-tt : ∀ {n x} → tgt {suc (suc n)} (src x) ≡ tgt (tgt x)
>
>
> module Freeω (G : GlobularSet) where
>  open GlobularSet G renaming (src to |src|;tgt to |tgt|)
>
>  mutual
>    data Freeω : ℕ → Set where
>      emb : ∀ {n} → # n → Freeω n
>      comp : ∀ {n} → (m : Fin (suc n)) → (α β : Freeω (suc n)) → src m
> β ≡ tgt m α → Freeω (suc n)
>      id : ∀ {n} → Freeω n → Freeω (suc n)
>      alpha : ∀ {n} → (x y z : Freeω (suc n)) → src fzero z ≡ tgt
> fzero y → src fzero y ≡ tgt fzero x → Freeω (suc (suc n))
>
>    src : ∀ {n} → (m : Fin (suc n)) → Freeω (suc n) → Freeω (n ℕ-ℕ m)
>    src fzero (emb y) = emb (|src| y)
>    src fzero (comp _ f g _) = src fzero f
>    src fzero (id y) = y
>    src fzero (alpha x y z yz xy) = comp fzero (comp fzero x y xy) z {!!}
>    src {zero} (fsuc ()) x
>    src {suc n} (fsuc i) x = src i (src fzero x)
>
>    tgt : ∀ {n} → (m : Fin (suc n)) → Freeω (suc n) → Freeω (n ℕ-ℕ m)
>    tgt fzero (emb y) = emb (|tgt| y)
>    tgt fzero (comp _ f g _) = tgt fzero g
>    tgt fzero (id y) = y
>    tgt fzero (alpha x y z yz xy) = comp fzero x (comp fzero y z yz) xy
>    tgt {zero} (fsuc ()) x
>    tgt {suc n} (fsuc i) x = tgt i (tgt fzero x)
>