在AgdaIntro中,视图部分解释:
使用这种类型,find函数可以这样编写:
现在,如果我想要证明以下属性:
..使用with时不会记住with-term和模式之间的连接。
这意味着当你定义时,
data False : Set where
record True : Set where
isTrue : Bool -> Set
isTrue true = True
isTrue false = False
infixr 30 _:all:_
data All {A : Set}(P : A -> Set) : List A -> Set where
all[] : All P []
_:all:_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)
satisfies : {A : Set} -> (A -> Bool) -> A -> Set
satisfies p x = isTrue (p x)
data Find {A : Set}(p : A -> Bool) : List A -> Set where
found : (xs : List A)(y : A) -> satisfies p y -> (ys : List A) ->
Find p (xs ++ y :: ys)
not-found : forall {xs} -> All (satisfies (not � p)) xs ->
Find p xs
你想证明
find1 :{A:Set}(p:A->Bool)(xs:ListA)->Find p xs
find1 p [] = not-found all []
find1 p(x::xs) with p x
...| true = found [] x {!!} xs
...| false = {!!}
尽管我们已经匹配并发现p x为真,但孔洞({!!})的类型是isTrue(p x)。
编译器不知道我们已经在p x上进行了模式匹配,并要求我们提供一个证明,证明p x为真!
这促使引入一个新类型,即
..一个类型A的元素类型与它们相等的证明,证明它们等于A中的某个给定x。
data Inspect {A : Set}(x : A) : Set where
it : (y : A) -> x == y -> Inspect x
inspect : {A : Set}(x : A) -> Inspect x
inspect x = it x refl
使用这种类型,find函数可以这样编写:
trueIsTrue : {x : Bool} -> x == true -> isTrue x
trueIsTrue refl = _
falseIsFalse : {x : Bool} -> x == false -> isFalse x
falseIsFalse refl = _
find : {A : Set}(p : A -> Bool)(xs : List A) -> Find p xs
find p [] = not-found all[]
find p (x :: xs) with inspect (p x)
... | it true prf = found [] x (trueIsTrue prf) xs
... | it false prf with find p xs
find p (x :: ._) | it false _ | found xs y py ys =
found (x :: xs) y py ys
find p (x :: xs) | it false prf | not-found npxs =
not-found (falseIsFalse prf :all: npxs)
现在,如果我想要证明以下属性:
NOW,如果我想证明以下属性:
predicate : ∀ {A : Set} {p : A -> Bool } {xs : List A } ->
All (satisfies' p) (filter p xs)
我将会遇到与find相同的问题,因此我需要在inspect上进行模式匹配以获取证明,但是我还需要编译器在过滤器中进展,例如p x == true
!
如果我进行一些并行模式匹配,编译器会将它们视为独立表达式。
predicate {A} {p} {xs = []} = all[]
predicate {A} {p} {xs = x :: xs} with p x
predicate {A} {p} {x :: xs} | px with inspect (p x)
predicate {A} {p} {x :: xs} | true | it true pf = {!!}
predicate {A} {p} {x :: xs} | true | it false pf = {!!}
predicate {A} {p} {x :: xs} | false | it true pf = {!!}
predicate {A} {p} {x :: xs} | false | it false pf = {!!}
我应该如何告诉编译器这两个分支有某种联系?我需要添加证明吗?
rewrite
关键字只出现在Agda 2.2.6中。 “您是否广泛使用Agda?” ——不太,我只是在家里学习东西。 - effectfully