While studying well-foundedness, I wanted to see how different designs behave. For example, for a type:
data _<_ (x : Nat) : Nat -> Set where
<-b : x < (suc x)
<-s : (y : Nat) -> x < y -> x < (suc y)
well-foundedness is easy to demonstrate. But if a similar type is defined differently:
data _<_ : Nat -> Nat -> Set where
z-< : (m : Nat) -> zero < (suc m)
s<s : (m n : Nat) -> m < n -> (suc m) < (suc n)
It is obvious that in both cases the descending chain is not infinite, but in the second case well-foundedness is not easy to demonstrate: it is not easy to show (y -> y < x -> Acc y) exists for a given x.
Are there some principles that help choose the designs like the first in preference to the designs like the second?
It's not impossibly hard to prove well-foundedness of the second definition, it just requires extra theorems. Here, relying on decidability of _==_ for Nat, we can construct new _<_ for the case (suc y) != x, and can rewrite the target types to use the solution to the problem known to decrease in size as the solution for suc y.
-- trying to express well-foundedness is tricky, because of how x < y is defined:
-- since both x and y decrease in the inductive step case, need special effort to
-- prove when the induction stops - when no more constructors are available
<-Well-founded : Well-founded Nat _<_
<-Well-founded x = acc (aux x) where
aux : (x y : Nat) -> y < x -> Acc _<_ y
aux zero y ()
aux x zero z-< = acc \_ ()
aux (suc x) (suc y) (s<s y<x) with is-eq? (suc y) x
... | no sy!=x = aux x (suc y) (neq y<x sy!=x)
... | yes sy==x rewrite sy==x = <-Well-founded x
The first definition is "canonical" in a sense, while the second one is not. In Agda, every inductive type has a subterm relation which is well-founded and transitive, although not necessarily total, decidable or proof-irrelevant. For W-types, it's the following:
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality
data W (S : Set)(P : S → Set) : Set where
lim : ∀ s → (P s → W S P) → W S P
_<_ : ∀ {S P} → W S P → W S P → Set
a < lim s f = ∃ λ p → a ≡ f p ⊎ a < f p
If we define Nat as a W-type, then the generic _<_ is the same as the first definition. The first definition establishes a subterm relation even if we have no idea about the constructors of Nat. The second definition is only a subterm relation because we know that zero is reachable from every suc n. If we added an extra zero' : Nat constructor, then this would not be the case anymore.