Writing proofs for a 'find index' function

[Kevin Mahoney]

Hi,

I'm writing a small article that touches on what dependent types are capable of. The problem is that although I have some background in Haskell, I'm quite new at this. I'm slowly making my way through some books on Coq and Agda, but right now I'm in over my head. :)

Here's what I'm working with: https://gist.github.com/KMahoney/b2a7856d179999daa2de

Now, in order to publish my article I don't actually need to provide the proofs (although that would be nice for me to understand), but I would like to fact check that

1) My types look plausible for what I'm trying to prove and

2) It is in fact possible to prove these properties.

Any advice or recommendations on reading material would be appreciated. I think I at least need a sigma in my 'justProof', because the 'r' has to come from somewhere, right?

[David Christiansen]

Hi Kevin

> I'm writing a small article that touches on what dependent types are
> capable of. The problem is that although I have some background in Haskell,
> I'm quite new at this. I'm slowly making my way through some books on Coq
> and Agda, but right now I'm in over my head. :)

It's still a bit rough to get going with these things, unfortunately.

> Here's what I'm working
> with: https://gist.github.com/KMahoney/b2a7856d179999daa2de
>
> Now, in order to publish my article I don't actually need to provide the
> proofs (although that would be nice for me to understand), but I would like
> to fact check that
>
> 1) My types look plausible for what I'm trying to prove and
> 2) It is in fact possible to prove these properties.

I think that your types are close, but not correct for what you want.
This is because they are mixing two different notions of equality: the
built-in notion of equality in the type system, and the Boolean check
that a user implements as part of implementing Eq. Elem uses the
built-in notion of equality, while Eq can do basically anything.

Here's a counterexample for your nothingProof - a similar one could be
built for the other proof:

module Main

import Data.Vect
import Data.Fin

%default total

find : Eq x => List x -> x -> Maybe Int
find [] elem = Nothing
find (y :: xs) elem = if y == elem then (Just 0) else (map (\ n => n +
1) (find xs elem))

find2 : Eq x => {n : Nat} -> Vect n x -> x -> Maybe (Fin n)
find2 [] elem = Nothing
find2 (y :: xs) elem = if y == elem then (Just FZ) else (map FS (find2
xs elem))

ex : find2 [1, 2, 3] 2 = Just 1
ex = Refl

nothingProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> Not
(Elem e v) -> (find2 v e) = Nothing
nothingProof n v elem notIn = ?noIdea1

justProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> (find2 v e
= Just r) -> (index r v == e) = True
justProof n v elem findProof = ?noIdea2

data Counterexample : Type where
One : Counterexample
Two : Counterexample

implementation Eq Counterexample where
_ == _ = True

implementation Uninhabited (Just x = Nothing) where
uninhabited Refl impossible

nothingCounterexample : Void
nothingCounterexample =
absurd $ nothingProof _ [One] Two notIn

where notIn : Elem Two [One] -> Void
notIn Here impossible
notIn (There Here) impossible


What you probably should do, based on your stated goal, is to use the
DecEq interface instead of the Eq interface. This one is set up such
that its notion of equality _must_ correspond with the type theory's
notion of equality. Additionally, instead of returning Fin elements, try
returning an Elem proof directly - that has just as much information
about the position of the element in the Vect, because each Here or
There constructor corresponds to either an FS or an FZ constructor, but
it also guarantees the placement.

Here's an example of how it could work to find the Elem directly. I also
wrote a Maybe (Fin n) version that uses DecEq, and then proved the
lemmas that you wanted for your version. I put them in one proof instead
of two to save time and space - the type does a case analysis to figure
out which version it's working on.

I didn't use anything not in the Idris tutorial as far as I can see,
with the possible exception of the Uninhabited interface. The way that
works is this: a proof that something is impossible can go in an
Uninhabited implementation, and then "absurd" resolves that
implementation at a use site so we don't have to remember custom names
for all those lemmas.

Here's how I might do what you're going for, with a few explanatory
comments:

module Main

import Data.Vect
import Data.Fin

%default total

||| If a value is neither at the head of a Vect nor in the tail of
||| that Vect, then it is not in the Vect.
notHeadNotTail : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
notHeadNotTail notHead notTail Here = notHead Refl
notHeadNotTail notHead notTail (There tl) = notTail tl

||| Determine the first location of an element in a Vect. The types
||| guarantee that we find a valid index, but not that it's the first
||| occurrence.
find : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
find x [] = No absurd
find x (y :: xs) with (decEq x y)
find x (x :: xs) | Yes Refl = Yes Here
find x (y :: xs) | No notHead with (find x xs)
find x (y :: xs) | No notHead | Yes prf = Yes (There prf)
find x (y :: xs) | No notHead | No notTail =
No $ notHeadNotTail notHead notTail

||| Find a Fin giving a position in a Vect, instead of an Elem
findIndex : DecEq a => (x : a) -> (xs : Vect n a) -> Maybe (Fin n)
findIndex x [] = Nothing
findIndex x (y :: xs) =
case decEq x y of
Yes _ => pure FZ
-- the following could be written as:
-- No _ => do tailIdx <- findIndex x xs
-- pure (FS tailIdx)
-- but idiom brackets are a bit cleaner:
No _ => [| FS (findIndex x xs) |]
-- (that was like the Haskell FS <$> findIndex x xs)


-- Prove that the Fin version corresponds to the Elem
-- version. Correspondence here means that if a Fin is found, we can
-- construct an Elem proof, and if a Fin is not found, then it is
-- provably impossible to construct an Elem proof.
findIndexOk : DecEq a => (x : a) -> (xs : Vect n a) ->
case findIndex x xs of
Just i => Elem x xs
Nothing => Not (Elem x xs)
findIndexOk x [] = absurd -- this is proved in the library already! :-)
findIndexOk x (y :: xs) with (decEq x y)
findIndexOk x (x :: xs) | Yes Refl = Here
findIndexOk x (y :: xs) | No notHead with (findIndexOk x xs) -- get an
induction hypothesis
findIndexOk x (y :: xs) | No notHead | ih with (findIndex x xs) --
split on the result of
--
the recursive call, to
--
reduce case expression
--
in the IH type
-- in this case, the induction hypothesis takes the second
-- branch in the case expression in the type, which tells us
-- that Not (Elem x xs)
findIndexOk x (y :: xs) | No notHead | ih | Nothing =
notHeadNotTail notHead ih
-- in this case, the IH tells us that it was indeed in the tail,
-- so we wrap in There to make it valid for y :: xs instead of
-- just xs
findIndexOk x (y :: xs) | No notHead | ih | Just z = There ih


(in case my mail client is being silly with line wraps, here's a gist
link: https://gist.github.com/david-christiansen/3b02d054b52405fecc70)

If that code doesn't make sense, I'd recommend working through the Idris
tutorial. If that doesn't clear things up, please ask further questions!

/David

[Kevin Mahoney]

Thank you David, that's really helpful!

At first I was confused why 'Eq' is not good enough, but I think I have it. Am I right in thinking that another way around that would be to keep the 'Eq' typeclass, but instead of 'Elem' for the proof, using something like 'Any (/x => x == elem)' ?

I think I understand the approach to the proof, if not the details, and in fact I'd noticed the relationship between Fin and the Elem constructors myself. I just didn't know how to use it!

In any case, your type signature for findIndexOk is enough for me to complete my article. I will link to your post for readers curious enough for a full explanation.

[Cliff L. Biffle]

On Sat, Feb 13, 2016 at 12:36 PM, Kevin Mahoney <ke...@kevinmahoney.co.uk> wrote:

At first I was confused why 'Eq' is not good enough, but I think I have it.

In short: 'Eq' is not specific enough.  You can implement 'Eq' to do anything at all, including returning true for any combination of inputs.  That means it (1) isn't guaranteed to match the type system's notion of equality as used by Elem, and (2) is often less useful for proofs in general, because it's less strict.

As David said, DecEq is designed in a way where you can't implement it in a ridiculous way.  (Well, without some serious gymnastics.)  In addition to the "equality" result, an implementation of 'decEq' hands back a proof of type system equality that the type checker (and thus proofs) will accept.

Having both concepts in the language tends to confuse noobs, and can lead to impedance mismatches in real programs (where one module is using Eq and the other needs DecEq).  But it's not clear that we could, say, discard Eq, in part because implementations may be more efficient than DecEq, and in part because you can't currently use a decEq result in an if statement. :-)

-Cliff

[David Christiansen]

On 13/02/16 15:36, Kevin Mahoney wrote:
> Thank you David, that's really helpful!

Glad to hear it!

> At first I was confused why 'Eq' is not good enough, but I think I have it.
> Am I right in thinking that another way around that would be to keep the
> 'Eq' typeclass, but instead of 'Elem' for the proof, using something like
> 'Any (/x => x == elem)' ?

Yes, something like this should work.

> I think I understand the approach to the proof, if not the details, and in
> fact I'd noticed the relationship between Fin and the Elem constructors
> myself. I just didn't know how to use it!

These proofs are pretty dense, and don't look much like proper
mathematical proofs unless you really squint. Hopefully the comments
bridged the gap a bit.

> In any case, your type signature for findIndexOk is enough for me to
> complete my article. I will link to your post for readers curious enough
> for a full explanation.

Well, I hope that's good enough for them. I did mention the tutorial a
few times, so hopefully it's not just nonsense in their ears.

/David

[David Christiansen]

On 13/02/16 15:46, Cliff L. Biffle wrote:
> Having both concepts in the language tends to confuse noobs, and can lead
> to impedance mismatches in real programs (where one module is using Eq and
> the other needs DecEq). But it's not clear that we could, say, discard Eq,
> in part because implementations may be more efficient than DecEq, and in
> part because you can't currently use a decEq result in an if statement. :-)

Even worse: DecEq may be too specific for some uses, and ensuring
consistency between Eq and DecEq may make programs slower.

For many types, we want an equality that is coarser than the built-in
one. For instance, we might want it to be alpha-equivalence for lambda
terms, or set equality for a tree type. DecEq forces us to keep these
separate, or even worse, to make our data representation be dictated by
the needs of type checking, which might come in conflict with other
considerations, such as performance or ease of error reporting. Quotient
types or setoids would fix this, at the cost of massive tedium.

Also, in Idris, constructor fields not used at runtime are erased.
However, the type system doesn't really know about this. If we use
DecEq, then it may have to inspect all the fields of the constructor.
This means that they are suddenly _all_ runtime-relevant, which can
potentially make them much slower.

/David

[Markus Klink]

David, 

does your gist compile for you?

For (reduced by me)

find : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

find x [] = No absurd

find x (y :: xs) = ?hole

I get the compiler error

When checking argument contra to constructor Prelude.Basics.No:

        Can't find implementation for Uninhabited (Elem x [])

Regards

Markus

[bo...@pik-potsdam.de]

Kevin,

your |justProof| looks quite similar to our

> lookupIndexLemma : (k : Fin n) ->
> (xs : Vect n t) ->
> (p : Injective2 xs) ->
> (q : Elem (index k xs) xs) ->
> lookup (index k xs) xs q = k

If you take a look at

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/VectOperations.lidr
https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/VectProperties.lidr

you will find an implementation of |lookupIndexLemma| and some more
properties of vectors.

Best,
Nicola

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>