Recently I'm using agda to prove some properties of de Bruijn indices, where the comparison of natural numbers is used ubiquitously.
When I do the reasoning, I'm always annoyed by the agda's unexpected unfolding of library function definition in "conditionals" (I'm not sure about this name, it appears right after the bar).
I put a minimal workable code here:
module _ where
open import Data.Nat using (ℕ; zero; suc; pred; _+_; _*_; _^_; _∸_; _≤?_; _≤_; s≤s)
open import Relation.Nullary using (yes; no; Dec)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
↑-var : ℕ → ℕ → ℕ
↑-var n x with n ≤? x
... | yes n≤x = suc x
... | no n>x = x
↑-↑-var : ∀ m n x
→ m ≤ n
→ ↑-var (suc n) (↑-var m x) ≡ ↑-var m (↑-var n x)
↑-↑-var m n x m≤n with m ≤? x
... | yes p = {!!}
... | no ¬p = {!!}
When you put the cursor in the first hole and show goals, the goal will be like:
Goal: (↑-var (suc n) (suc x)
| Relation.Nullary.Decidable.Core.map′
(Data.Nat.Properties.<ᵇ⇒< n (suc x)) Data.Nat.Properties.≤⇒≤ᵇ
(Data.Bool.Properties.T? (n Data.Nat.<ᵇ suc x)))
≡
(↑-var m
(↑-var n x
| Relation.Nullary.Decidable.Core.map′
(Data.Nat.Properties.≤ᵇ⇒≤ n x) Data.Nat.Properties.≤⇒≤ᵇ
(Data.Bool.Properties.T? (n Data.Nat.≤ᵇ x)))
| Relation.Nullary.Decidable.Core.map′
(Data.Nat.Properties.≤ᵇ⇒≤ m
(↑-var n x
| Relation.Nullary.Decidable.Core.map′
(Data.Nat.Properties.≤ᵇ⇒≤ n x) Data.Nat.Properties.≤⇒≤ᵇ
(Data.Bool.Properties.T? (n Data.Nat.≤ᵇ x))))
Data.Nat.Properties.≤⇒≤ᵇ
(Data.Bool.Properties.T?
(m Data.Nat.≤ᵇ
(↑-var n x
| Relation.Nullary.Decidable.Core.map′
(Data.Nat.Properties.≤ᵇ⇒≤ n x) Data.Nat.Properties.≤⇒≤ᵇ
(Data.Bool.Properties.T? (n Data.Nat.≤ᵇ x))))))
————————————————————————————————————————————————————————————
m≤n : m ≤ n
n : ℕ
p : m ≤ x
x : ℕ
m : ℕ
Such definition unfolding disturbs a lot especially when it appears in a more complicated lemma. Can someone tell me where I did wrongly or is there a better practice to reason about natural numbers or how to ease the pain?
It will be appreciated if you elaborate on meaning of the "bar (|)" in the second line. (I sort of know that it may belong to some conditionals).
Agda always unfolds definitions to weak-head normal form (whnf) during conversion checking. This is necessary to guarantee that all implicit arguments inferred by Agda are unique up to definitional equality (other proof assistants such as Coq or Lean do not provide this guarantee).
One way to avoid excessive unfolding is to use abstract (https://agda.readthedocs.io/en/v2.6.3/language/abstract-definitions.html), which will mark a definition as not unfolding except in other abstract definitions from the same module.
If you require the ability to unfold a definition at a later point, another technique is to define a new module that is parametrized over the values for which you want to avoid unfolding, and then apply the module to the concrete definitions at the point you want them to be unfolded.
The next release of Agda (2.6.4) will also provide a more granular version of abstract - dubbed opaque - that can be unfolded on demand in other modules as well (https://agda.readthedocs.io/en/latest/language/opaque-definitions.html).