I'm trying to define binary numbers in agda but agda cant see that ⟦_⇑⟧ is terminating. I really dont want to have to break out accessibility relations. How can I show agda that n gets smaller?
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 ⇑⟧
Error:
Termination checking failed for the following functions:
⟦_⇑⟧
Problematic calls:
⟦ k ⇑⟧
Termination checking fails for good reasons, since the following function is not structurally recursive over its input:
⟦_⇑⟧ : ℕ → 𝔹 ⟦ zero ⇑⟧ = 𝕫 ⟦ suc n ⇑⟧ with parity n ⟦ suc .(k + k) ⇑⟧ | 𝕖 k = 𝕠 ⟦ k ⇑⟧ ⟦ suc .(suc (k + k)) ⇑⟧ | 𝕠 k = 𝕖 ⟦ k ⇑⟧
Agda even tells you what is the problematic call : ⟦ k ⇑⟧. (in this case, there are two of these ill-formed calls).
While I agree it might look that the function is called on a structurally smaller argument it's not the case. To understand why, you have to see that k is used as input for a function call, _+_, and that only the result of this function is structurally smaller than n, not k itself. And agda has no way of knowing the following property about _+_ :
∀ {n} → n < suc (n + n)
Should you provide a proof of such lemma, you could use the fact that _<_ is well founded to make your function structurally recursive over Acc, but it seems you are reluctant to do so.
An easy way to understand why Agda cannot know that this terminates is the following: imagine you replace suc .(k + k) by suc .(a ∸ b) and recursively call your function over a. From agda's point of view, both are the same cases, and in this case, it does not usually terminate unless b happens to be 0.
Here is the module corrected in terms of termination :
module Binary where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Induction.Nat
open import Induction.WellFounded
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 ⇓⟧
decr : ∀ {n} → n < suc (n + n)
decr {n} = s≤s (m≤m+n n n)
helper : (n : ℕ) → Acc _<_ n → 𝔹
helper zero a = 𝕫
helper (suc n) a with parity n
helper (suc .(k + k)) (acc rs) | 𝕖 k = 𝕠 (helper k (rs _ decr))
helper (suc .(suc (k + k))) (acc rs) | 𝕠 k = 𝕖 (helper k (rs _ (s≤s (<⇒≤ decr))))
⟦_⇑⟧ : ℕ → 𝔹
⟦ n ⇑⟧ = helper n (<-wellFounded n)
I was also skeptical about the correctness of your definitions and it turns out I was right, for instance, considering the following definition:
test : ℕ
test = ⟦ ⟦ 124 ⇑⟧ ⇓⟧
Agda returns 2 when evaluating test.
Considering the definition:
test₁ : ℕ
test₁ = ⟦ ⟦ 16 ⇑⟧ ⇓⟧
Agda returns 14 when evaluating test₁
In order to correct your definitions, you can take inspiration from what is done in the standard library, either in the module Data.Bin (deprecated) or in the module Data.Nat.Binary depending on which version of the stdlib you have.