[Agda] successor / predecessor definition rejected for a tree-based
natural number type
Paul Tarau
paul.tarau at gmail.com
Tue Jul 2 18:43:15 CEST 2013
{-
The following successor / predecessor definition
for a tree-based natural number data type is
rejected by Agda 2.3.2.1 with:
Not in scope:
x at /Users/tarau/Desktop/go/art/lit/coq/vw.agda:24,27-28
when scope checking x
-}
module VW where
open import Data.List
data T : Set where
E : T
V : T -> List T -> T
W : T -> List T -> T
mutual
s : T -> T
s E = V E []
s (V E []) = W E []
s (V E (x::xs)) = W (s x) xs {- agda error here, claims x not in scope -}
s (V z xs) = W E (s' z :: xs)
s (W z []) = V (s z) []
s (W z [E]) = V z [E]
s (W z (E::y::ys)) = V z (s y::ys)
s (W z (x::xs)) = V z (E::s' x::xs)
s' : T -> T
s' (V E []) = E
s' (V z []) = W (s' z) []
s' (V z [E]) = W z [E]
s' (V z (E::x::xs)) = W z (s x::xs)
s' (V z (x::xs)) = W z (E::s' x::xs)
s' (W E []) = V E []
s' (W E (x::xs)) = V (s x) xs
s' (W z xs) = V E (s' z::xs)
{-
Its (attached) Coq equivalent passes termination check,
and while the recursion is mutual, calls are
only made on structurally smaller arguments.
Is this a limitation of Agda's termination checker,
something related to using x inside a list construct
or something else that I am missing?
Thanks in advance for any hints on what's going on,
Paul
P.S. I am just 1-day new to Agda but I am planning to
splash in more deeply, as it is syntactically quite
friendly to my existing Haskell code at
http://logic.cse.unt.edu/tarau/Research/2013/hbin.hs
for which I want to prove equivalence with (the Peano
algebra of) natural numbers. The complete story is
explained in detail at
http://logic.cse.unt.edu/tarau/Research/2013/hbin.pdf
and some of the applications are at
http://logic.cse.unt.edu/tarau/Research/2013/hbs.pdf
-}
{- same in Coq - passes termination check
Require Import List.
Inductive T : Type :=
| E : T
| V : T -> list T -> T
| W : T -> list T -> T.
Fixpoint s (t:T) :=
match t with
| E => V E nil
| V E nil => W E nil
| V E (x::xs) => W (s x) xs
| V z xs => W E (s' z :: xs)
| W z nil => V (s z) nil
| W z (E::nil) => V z (E::nil)
| W z (E::y::ys) => V z (s y::ys)
| W z (x::xs) => V z (E::s' x::xs)
end
with
s' (t:T) : T :=
match t with
| V E nil => E
| V z nil => W (s' z) nil
| V z (E::nil) => W z (E::nil)
| V z (E::x::xs) => W z (s x::xs)
| V z (x::xs) => W z (E::s' x::xs)
| W E nil => V E nil
| W E (x::xs) => V (s x) xs
| W z xs => V E (s' z::xs)
| E => E (* pro forma *)
end.
-}
More information about the Agda
mailing list