これはちょっと悲しい子認定されると思う

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
残念でしたみたいな・・・。