Post by Sergei MeshvelianiCan anybody demonstrate it on the following example?
Here you go:
--------------------------------------------------------------
open import Function using (_∘_; _on_)
open import Data.List using (List; []; _∷_)
open import Data.Bin using (Bin; toBits; pred; _<_; less; toℕ)
open import Data.Digit using (Bit)
import Data.Nat as Nat
import Induction.Nat as NatInd
open import Induction.WellFounded
open Bin
predBin : Bin → Bin
predBin = pred ∘ toBits
postulate
predBin-< : (bs : List Bit) -> predBin (bs 1#) < (bs 1#)
-- The strict order on binary naturals implies the strict order on the
-- corresponding unary naturals.
<⇒<ℕ : ∀ {b₁ b₂} → b₁ < b₂ → (Nat._<_ on toℕ) b₁ b₂
<⇒<ℕ (less lt) = lt
-- We can derive well-foundedness of _<_ on binary naturals from
-- well-foundedness of _<_ on unary naturals.
<-wellFounded : WellFounded _<_
<-wellFounded =
Subrelation.wellFounded <⇒<ℕ (Inverse-image.wellFounded toℕ
NatInd.<-wellFounded)
open All <-wellFounded using () renaming (wfRec to <-rec)
downFrom : Bin → List Bin -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []
downFrom = <-rec _ _ df
where
df : (b : Bin) → (∀ b′ → b′ < b → List Bin) → List Bin
df 0# dfRec = 0# ∷ []
df (bs 1#) dfRec = (bs 1#) ∷ (dfRec (predBin (bs 1#)) (predBin-< bs))
--------------------------------------------------------------
In order to use well-founded induction, we first have to prove that
the strict order < is indeed well-founded. Thankfully, the standard
library already contains such a proof for the strict order on (unary)
naturals as well as a collection of combinators for deriving
well-foundedness of relations from others (in this case the strict
order on unary naturals).
The core of the implementation of `downFrom' via well-founded
recursion is the function `df', which has the same signature as
`downFrom' except for the additional argument `dfRec', which serves as
the 'induction hypothesis'. The argument `dfRec' is itself a function
with (almost) the same signature as `downFrom' allowing us to make
recursive calls (i.e. take a recursive step), provided we can prove
that the first argument of the recursive call (i.e. the argument to
the induction hypothesis) is smaller than the first argument of the
enclosing call to `df'. The proof that this is indeed the case is
passed to `dfRec' as an additional argument of type b′ < b.
The following answer on Stackoverflow contains a nice explanation on
how all of this is implemented in Agda under the hood:
https://stackoverflow.com/a/19667260
Cheers
/Sandro
Post by Sergei MeshvelianiPost by Sergei MeshvelianiDear all,
I am trying to understand how to use WellFounded of Standard library.
Can anybody demonstrate it on the following example?
--------------------------------------------------------------
open import Function using (_∘_)
open import Data.List using (List; []; _∷_)
open import Data.Bin using (Bin; toBits; pred)
open Bin
predBin : Bin → Bin
predBin = pred ∘ toBits
downFrom : Bin → List Bin -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []
downFrom 0# = 0# ∷ []
downFrom (bs 1#) = (bs 1#) ∷ (downFrom (predBin (bs 1#)))
--------------------------------------------------------------
downFrom is not recognized as terminating.
How to reorganize it with using items from
Induction/*, WellFounded.agda ?
I presumed also that it is already given the property
postulate
predBin-< : (bs : List Bit) -> predBin (bs 1#) < (bs 1#)
(I do not mean to deal here with its proof).
--
SM
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda