これはちょっと悲しい子認定されると思う
module Proof1 where data List (A : Set0) : Set0 where [] : List A _::_ : A -> List A -> List A rec1 : {X : Set0} -> List X -> List X rec1 [] = [] rec1 (x :: xs) = rec1 [] -- ここのrec1で
rec1の停止性を証明出来ないらしい。うーん・・・。
rec1 : {X : Set0} -> List X -> List X rec1 [] = [] rec1 (x :: xs) = rec1 xs
これだと普通に大丈夫なので length [] <= length xsとか言えれば良いんだろうかと思って以下
module Proof1 where data Bool : Set0 where true : Bool false : Bool data Nat : Set0 where zero : Nat succ : Nat -> Nat data List (A : Set0) : Set0 where [] : List A _::_ : A -> List A -> List A length : {A : Set0} -> List A -> Nat length [] = zero length (x :: xs) = succ (length xs) _<=_ : Nat -> Nat -> Bool zero <= _ = true (succ _) <= zero = false (succ a) <= (succ b) = a <= b _⊆_ : {A : Set0} -> List A -> List A -> Bool a ⊆ b = (length a) <= (length b) data Val {A : Set0} : A -> Set0 where val : (a : A) -> Val a rec1 : {X : Set0} -> List X -> List X rec1 [] = [] rec1 {X} (x :: xs) = rec1 tmp -- ここで依然として停止性が言えて無いらしい where tmp : List X tmp = [] tmp⊆xs : Val true tmp⊆xs = val (tmp ⊆ xs)
type checkはパスするけど、これまたrec1でダメなので、うーん・・・。
もっと直接的に言わないとダメなのかなぁ。
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.TerminationChecker
残念でしたみたいな・・・。