[Agda] Termination-check doesn't know which case it should check?
Andrés Sicard-Ramírez
andres.sicard.ramirez at gmail.com
Wed Jul 3 14:43:42 CEST 2013
On 3 July 2013 03:34, Darryl McAdams <psygnisfive at yahoo.com> wrote:
> The following code gives a termination error on <+>-lemma even tho the
> recursion is guarded.
>
> _+>_ : ℕ → ℕ → ℕ
> zero +> n = n
> suc m +> n = m +> suc n
>
> _<+_ : ℕ → ℕ → ℕ
> m <+ zero = m
> m <+ suc n = suc m <+ n
>
> +>-suc-lemma : (m n : ℕ) → m +> suc n ≡ suc (m +> n)
> +>-suc-lemma m n = {!!}
>
> <+-suc-lemma : (m n : ℕ) → suc m <+ n ≡ suc (m <+ n)
> <+-suc-lemma m n = {!!}
>
> <+>-lemma : (m n : ℕ) → m +> n ≡ m <+ n
> <+>-lemma 0 0 = refl
> <+>-lemma 0 (suc n) rewrite <+-suc-lemma 0 n | cong suc (<+>-lemma 0
> n) = refl
> <+>-lemma (suc m) 0 rewrite +>-suc-lemma m 0 | cong suc (<+>-lemma m
> 0) = refl
> <+>-lemma (suc m) (suc n) rewrite <+-suc-lemma (suc m) n | <+-suc-lemma m n
> | +>-suc-lemma m (suc n) | +>-suc-lemma m n
> | cong (suc ∘ suc) (<+>-lemma m n) = refl
>
I couldn't reproduce the issue with Agda-2.3.2.1.
--
Andrés
More information about the Agda
mailing list