Description
Probably WellFounded does not hold for <-lex on lists.
Right?
But for each n, it holds for the vectors of length ≤ n.
So far I have implemented it for vectors of length ≡ n.
But
a) my library uses a different representation for Vector (shown below),
b) I expect, the Agda team can implement this itself.
c) I can send the code as a sample, it is clear enough. One can rewrite it to the standard Vector representation.
The approach is as follows.
The vector representation:
module Vector.Base {α} (A : Set α)
where
data Vector (n : ℕ) : Set α
where
vec : (xs : List A) → length xs ≡ n → Vector n
_<_ : Rel A α
A general simple lemma suggested in another issue and used here:
subrelation-WellFounded : ∀ {r} {~ ~' : Rel A r} → (~' ⇒ ~) → WellFounded ~ → WellFounded ~'
Lexicographic ordering on lists:
_<llex_ = Lex-< _≡_ _<_
Lexicographic ordering on Vector n:
<lex : ∀ n → Rel (Vector n) _
<lex n = _<llex_ on toList
Theorem:
wellFounded-<lex : WellFounded _<_ → (n : ℕ) → WellFounded (<lex n)
The proof is by induction on n and by using <lex-1+n ⇒ (×-lex _<_ <lexₙ) on f,
where f : Vector 1+n → A × Vector n is a certain evident map.
This is using that a) <lex-1+n on Vector 1+n equals to a certain composition ×-lex on Product with
<lexₙ on Vector n,
b) WellFounded for ×-lex for Product is in lib-1.7.