С пунктами, скрывающими прекращение - PullRequest
Новая
       17

С пунктами, скрывающими прекращение

0 голосов
/ 11 ноября 2019

Я пытаюсь определить двоичные числа в агде, но агда не видит, что ⟦_⇑⟧ заканчивается. Я действительно не хочу разрывать отношения доступности. Как я могу показать agda, что n становится меньше? 

module Binary where

open import Data.Nat using (ℕ; _+_; +-suc)
open ℕ

2* : ℕ → ℕ
2* n = n + n

data Parity : ℕ → Set where
  ? : ∀ k → Parity (2* k)
  ? : ∀ k → Parity (1 + 2* k)

parity : ∀ n → Parity n
parity zero = ? 0
parity (suc n) with parity n
parity (suc .(k + k)) | ? k = ? k
parity (suc .(suc (k + k))) | ? k rewrite sym (+-suc k k) = ? (suc k)

data ? : Set where
  ? : ?
  ? : ? → ?
  ? : ? → ?

⟦_⇓⟧ : ? → ℕ
⟦ ? ⇓⟧ = 0
⟦ ? b ⇓⟧ = 2* ⟦ b ⇓⟧
⟦ ? b ⇓⟧ = 1 + 2* ⟦ b ⇓⟧

⟦_⇑⟧ : ℕ → ?
⟦ zero ⇑⟧ = ?
⟦ suc n ⇑⟧ with parity n
⟦ suc .(k + k) ⇑⟧ | ? k = ? ⟦ k ⇑⟧
⟦ suc .(suc (k + k)) ⇑⟧ | ? k = ? ⟦ k ⇑⟧

Ошибка: 

Termination checking failed for the following functions:
  ⟦_⇑⟧
Problematic calls:
  ⟦ k ⇑⟧
...