どっちがいいんだろう?

何かを定義する時に、

∃n > 0.n + n > 0

のように、0より大きなある自然数nを加算した結果は0よりも大きいという意味が無い命題を書きたい時に

∃n > 0

といった、ある種自然数のsubtypeを作って定義を進めたい、というような時、Agda2ではどう書くのが良いんだろうなーというのが在ります。

例えば

module Hatena where

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

three : Nat
three = succ (succ (succ zero))

data Bool : Set0 where
  true : Bool
  false : Bool

not : Bool -> Bool
not true = false
not false = true

data Id {A : Set0} : A -> A -> Set0 where
  refl : (a : A) -> Id a a

record pair (A : Set0) (B : Set0) : Set0 where
  field
    fst : A
    snd : B

record ∃ {A : Set}(P : A -> Set) : Set where
  field
    witness : A
    proof   : P witness

_<_ : Nat -> Nat -> Bool
zero < zero = false
zero < (succ _) = true
(succ a) < zero = false
(succ a) < (succ b) = a < b

isEven : Nat -> Bool
isEven zero = true
isEven (succ zero) = false
isEven (succ (succ a)) = isEven a

isOdd : Nat -> Bool
isOdd a = not (isEven a)

-- p1 : ∃n < 3.isEven(n)
-- どっちが良いだろう?
-- 他にもあるかなー
postulate pr1-1 : ∃ (\n -> Id (n < three) true -> Id (isEven n) true)
postulate pr1-2 : ∃ (\n -> pair (Id (n < three) true) (Id (isEven n) true))

-- pr2-aux : ∀n.isEven(n) -> isOdd(succ n)
postulate pr2-aux : {n : Nat} -> Id (isEven n) true -> Id (isOdd (succ n)) true

-- pr2 : ∃n.isOdd(succ n)
pr2 : ∃ \n -> Id (isOdd (succ n)) true
pr2 = pr2-aux tmp
  where
    w : Nat
    w = ∃.witness pr1-1

    proof : Id (w < three) true -> Id (isEven w) true
    proof = ∃.proof pr1-1

    tmp : Id (isEven w) true
    tmp = proof (refl true) -- ここで失敗

pr2' : ∃ \n -> Id (isOdd (succ n)) true
pr2' = pr2-aux tmp
  where
    w : Nat
    w = ∃.witness pr1-2

    proof : pair (Id (w < three) true) (Id (isEven w) true)
    proof = ∃.proof pr1-2

    tmp : Id (isEven w) true
    tmp = pair.snd proof

pr2は明ですが、まぁそれを何故か

pr2-aux : ∀n.isEven(n) -> isOdd(succ n)
と
p1 : ∃n < 3.isEven(n)

を使って証明します。

でその時に、∃のAgda2での表現はまぁどうするのが適当なんだろうなーという事です。

ちなみに、上記定義であればpr2だと型チェックで失敗。pr2'だと成功です。

(敢えてpostulateを使っているのでpr2だとこの場合は失敗するのですが(というのは、witnessなconcreteな値を取れないのでtmpで失敗))

関係するぽいもの

http://www.gilith.com/research/talks/cambridge2000-subtypes.pdf

http://mattam.org/research/publications/Subset_Coercions_in_Coq.pdf

追記

ATS(Applied Type System)では割と上手く振る舞ってくれるというのを噂で聞いたのですが、ATSはようわからん...

こっちの方が良いかも

module Filter where

data _==_ {A : Set0} : A -> A -> Set0 where
  refl : (a : A) -> a == a

symm-I : {A : Set0}{a b : A} -> a == b -> b == a
symm-I (refl a) = refl a

trans-I : {A : Set0}{a b c : A} -> a == b -> b == c -> a == c
trans-I (refl a) bc = bc

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

data Array (A : Set0) : Nat -> Set0 where
  [] : Array A zero
  _::_ : {n : Nat} -> A -> Array A n -> Array A (succ n)

data Bool : Set0 where
  true : Bool
  false : Bool

_<_ : Nat -> Nat -> Bool
zero < zero = false
zero < (succ _) = true
(succ _) < zero = false
(succ a) < (succ b) = a < b

_<=_ : Nat -> Nat -> Bool
zero <= _ = true
(succ _) <= zero = false
(succ a) <= (succ b) = a <= b

<=-lem : {n1 : Nat}{n2 : Nat} -> (n1 <= n2) == true -> (n1 <= (succ n2)) == true
<=-lem {zero}{_} _ = refl true
<=-lem {succ a}{zero} ()
<=-lem {succ a}{succ b} pr = proof
  where
    pr' : (a <= b) == true
    pr' = pr

    hypo1 : (a <= (succ b)) == true
    hypo1 = <=-lem pr'

    hypo2 : (succ a <= (succ (succ b))) == (a <= (succ b))
    hypo2 = refl (a <= (succ b))

    proof : (succ a <= (succ (succ b))) == true
    proof = trans-I hypo2 hypo1

record ∃ {A : Set0} (P : A -> Set0) : Set0 where
  field
    witness : A
    proof   : P witness

record pair (A B : Set0) : Set0 where
  field
    fst : A
    snd : B

-- filter : ∀n.∀A.(pred : A -> Bool) -> Array A n -> ∃n'<=n.Array A n'
{-
filter : {n : Nat} {A : Set0} -> (p : A -> Bool) -> Array A n -> (∃ \n' -> (n' <= n) == true -> Array A n')
filter {zero} {A} p [] = proof
  where
    w : Nat
    w = zero

    pr : (w <= zero) == true -> Array A w
    pr = (\pr -> [])

    proof : ∃ \n' -> (n' <= zero) == true -> Array A n'
    proof = record { witness = w; proof = pr}
filter {succ n} {A} p (x :: xs) with p x
... | true = _
  where
    hypo : ∃ \n' -> (n' <= n) == true -> Array A n'
    hypo = filter p xs
-}

filter' : {n : Nat} {A : Set0} -> (p : A -> Bool) -> Array A n -> (∃ \n' -> pair ((n' <= n) == true) (Array A n'))
filter' {zero} {A} p [] = proof
  where
    w : Nat
    w = zero

    proof : ∃(\n' -> pair ((n' <= zero) == true) (Array A n'))
    proof = record { witness = w; proof = record { fst = refl true ; snd = [] }}
filter' {succ n} {A} p (x :: xs) with p x
... | true = proof
  where
    hypo : ∃(\n' -> pair ((n' <= n) == true) (Array A n'))
    hypo = filter' p xs

    w : Nat
    w = ∃.witness hypo

    l : (w <= n) == true
    l = pair.fst (∃.proof hypo)

    r : Array A w
    r = pair.snd (∃.proof hypo)

    succ_w : Nat
    succ_w = succ w

    aux : (succ w <= succ n) == (w <= n)
    aux = refl (w <= n)

    l' : (succ_w <= (succ n)) == true
    l' = trans-I aux l

    r' : Array A succ_w
    r' = x :: r

    proof : (∃ (\n' -> pair ((n' <= (succ n)) == true) (Array A n')))
    proof = record {witness = succ_w ; proof = record {fst = l' ; snd = r'}}
... | false = proof
  where
    hypo : (∃ (\n' -> pair ((n' <= n) == true) (Array A n')))
    hypo = filter' p xs

    w : Nat
    w = ∃.witness hypo

    l : (w <= n) == true
    l = pair.fst (∃.proof hypo)

    r : Array A w
    r = pair.snd (∃.proof hypo)

    l' : (w <= (succ n)) == true
    l' = <=-lem l

    proof : (∃ (\n' -> pair ((n' <= (succ n)) == true) (Array A n')))
    proof = record {witness = w ; proof = record {fst = l' ; snd = r}}

長さ情報を持つ配列に関するfilterでやってみました。

証明してるのは単に、filter関数は引数で取った配列は、長さだけに注目すると、同じか、それよりも短い配列を返しますよね?ということです。
(配列の内容に関する証明は行ってません。