move lemma-just!=nothing to FinMap and use it there

inline bot-elim into lemma-just-nothing

Seems like the more common use case.

abstract proofs over checkInsert

All proofs about expressions containing checkInsert share a common
pattern. There are three cases:
 1) Inserting a key-value-pair that is already present in the map.
 2) Inserting a new key into the map.
 3) Failure to insert a conflicting key-value pair in the map.

The checkInsertProof record enables to write three different cases
reducing the usage of "with" (and thus line length) in
lemma-checkInsert-restrict and lemma-lookupM-assoc.

fix wrong function name in lemma-2

lookup and lookupM reference the same function, but serve different
purposes.

remove useless braces

avoid a sym in lemma-union-restrict

s/generate/restrict/g

The name was deemed misleading. Nothing else changed.

rephrase free-theorem-list-list using pointwise equality

formulate theorem-2

prove lemma-union-generate

prove theorem-1 assuming a lemma-union-generate

started proving theorem-1

As in the bff paper expand s using lemma-map-denumerate-enumerate
and apply free-theorem-list-list to commute get and map.

introduce denumerate

It is some kind of counter part to enumerate. That is:

map (denumerate s) (enumerate s) \== s

It can be employed in bff and I believe it to simplify reasoning on bff.

replace idrange with enumerate

Looks like uses of idrange would always be passed a length, so move it
inside the definition.

postulate free theorem for List a -> List a

recursion of lemma-2

started proving lemma-2

The step case needs two lemmata. One for the head of the resulting map and one
for the tail. The head case is shown using a

lemma-lookupM-assoc : assoc eq (i :: _) (x :: _) == just h ->
  lookupM i h == just x

reduce imports to speed up agda-mode

split Bidir.agda to FinMap.agda

improve readability using spaces

reduce usage of sym

Try to always construct statements of the form
  complex expression \== simple expression.

open \==-Reasoning at top level

prove the remaining parts of lemma-checkInsert-generate

Introducing the following lemmata:
 * lemma-lookupM-empty : nothing \== lookupM i empty
 * lemma-from-just : just x \== just y -> x \== y
 * lemma-lookupM-insert : just a \== lookupM i (insert i a m)
 * lemma-lookupM-insert-other : \neg (i \== j) ->
   lookupM i m \== lookupM i (insert j a m)
 * lemma-lookupM-generate : just a = lookupM i (generate f is) -> a \== f i

complete the yes part of lemma-checkInsert-generate using inspect

change lemma-insert-same to work with \== proofs

This way the inserted value is not hidden in the Is-Just proof object.

base case of lemma-2

rewrite lemma-1 using propositional equality

actually fmap is what I meant instead of >>=

introduce >>= on Maybe to improve readability

improve readability by introducing EqInst

formulate theorem-1

formulate lemma-2

attempt to prove lemma-1

In order to prove lemma-1 we first show a lemma-insert-same to show that
inserting the same pair twice does not change the FinMapMaye. lemma-1 still
has two goals. In the first goal agda doesn't accept "is-just (f i)". Why?
The second goal is to be shown as absurd.

rewrite generate using zip and fromAscList

This way matches the usage in lemma-1 more closely since zip actually is
something similar to assoc.

split FinMap to FinMapMaybe

The FinMapMaybe is what FinMap previously was. The FinMap instead now really
maps its whole domain to something. This property is needed to avoid the
usage of fromJust in the definition of bff. With this split applied the
definition of bff is now complete.

replaced NatMap with FinMap

The domain of the map is always limited. So using Fin n as the domain is
natural. Additionally FinMaps are now semantically equal iff their normal form
is the same. That means \== can be used.

first attempt to define bff (with holes)

employ standard library of agda where possible

first attempt to model lemma-1

Without using the stdlib basic data structures are defined (with the
stdlib names in mind). The IntMap given in the paper is translated to a
NatMap. There are definitions for checkInsert and assoc resulting in a
formalization of lemma-1.

added .gitignore