Agda, type of evidence and article
In AgdaIntro, the view section explains:
.. that s does not remember the relationship between terms and templates.
This means that when determining
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
And you want to prove
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 = {!!}
Hole type ({!!}) isTrue (px), although we already matched px and found out that this is true.
The compiler does not know that we have matched the pattern on px and is asking us to prove that px is true!
This motivates the introduction of a new type,
.. the type of elements of type A together with proofs that they are equal to some given x in A.
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
With this type, the find function can be written:
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, If I want to prove the following property:
predicate : ∀ {A : Set} {p : A -> Bool } {xs : List A } ->
All (satisfies' p) (filter p xs)
I will have the same problem when searching, so I need to match a pattern to validate to get a witness, but I ALSO have to have a compiler to step through the filter in casep x == true
If I do parallel pattern matching, the compiler treats them as independent expressions
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 = {!!}
How can I tell the compiler that the two branches are linked in some way? Should I add proof of this?
source to share
Just don't match the pattern on p x
:
predicate {A} {p} {xs = []} = all[]
predicate {A} {p} {x :: xs} with inspect (p x)
predicate {A} {p} {x :: xs} | it true pf rewrite pf = {!!}
predicate {A} {p} {x :: xs} | it false pf rewrite pf = {!!}
Note that the idiom is inspect
deprecated. Use test steroids . You can find it in the standard library here .
Your code will become
predicate : ∀ {A : Set} {p : A -> Bool } {xs : List A } ->
All (satisfies p) (filter p xs)
predicate {A} {p} {xs = []} = all[]
predicate {A} {p} {xs = x :: xs} with p x | inspect p x
predicate {A} {p} {x :: xs} | true | [ pf ] = {!!}
predicate {A} {p} {x :: xs} | false | [ pf ] = {!!}
c pf
is in the first hole
.Data.Unit.Core.reveal (.Data.Unit.Core.hide p x) == true
which beta boils down to p x == true
. That is, if you have
test : ∀ {A : Set} {p : A -> Bool} {x} -> p x == true -> True
test _ = _
then placing test {p = p} pf
in the first hole and typing Cc Cd you get True
.
source to share