Helmut Grohne [Thu, 19 Apr 2012 09:52:27 +0000 (11:52 +0200)]
move lemma-just!=nothing to FinMap and use it there

Helmut Grohne [Tue, 17 Apr 2012 10:10:35 +0000 (12:10 +0200)]
inline bot-elim into lemma-just-nothing

Seems like the more common use case.

Helmut Grohne [Wed, 4 Apr 2012 12:08:46 +0000 (14:08 +0200)]
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.

Helmut Grohne [Fri, 16 Mar 2012 10:41:44 +0000 (11:41 +0100)]
fix wrong function name in lemma-2

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

Helmut Grohne [Thu, 9 Feb 2012 15:14:57 +0000 (16:14 +0100)]
remove useless braces

Helmut Grohne [Thu, 9 Feb 2012 15:04:32 +0000 (16:04 +0100)]
avoid a sym in lemma-union-restrict

Helmut Grohne [Thu, 9 Feb 2012 15:01:38 +0000 (16:01 +0100)]
s/generate/restrict/g

The name was deemed misleading. Nothing else changed.

Helmut Grohne [Thu, 9 Feb 2012 14:56:29 +0000 (15:56 +0100)]
rephrase free-theorem-list-list using pointwise equality

Helmut Grohne [Thu, 9 Feb 2012 14:33:38 +0000 (15:33 +0100)]
formulate theorem-2

Helmut Grohne [Thu, 9 Feb 2012 14:08:36 +0000 (15:08 +0100)]
prove lemma-union-generate

Helmut Grohne [Thu, 9 Feb 2012 13:59:32 +0000 (14:59 +0100)]
prove theorem-1 assuming a lemma-union-generate

Helmut Grohne [Thu, 9 Feb 2012 11:35:10 +0000 (12:35 +0100)]
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.

Helmut Grohne [Thu, 9 Feb 2012 10:58:54 +0000 (11:58 +0100)]
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.

Helmut Grohne [Tue, 31 Jan 2012 17:32:46 +0000 (18:32 +0100)]
replace idrange with enumerate

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

Helmut Grohne [Tue, 31 Jan 2012 17:26:32 +0000 (18:26 +0100)]
postulate free theorem for List a -> List a

Helmut Grohne [Thu, 26 Jan 2012 17:06:42 +0000 (18:06 +0100)]
recursion of lemma-2

Helmut Grohne [Thu, 26 Jan 2012 16:12:44 +0000 (17:12 +0100)]
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

Helmut Grohne [Thu, 26 Jan 2012 15:05:23 +0000 (16:05 +0100)]
reduce imports to speed up agda-mode

Helmut Grohne [Thu, 26 Jan 2012 14:51:15 +0000 (15:51 +0100)]
split Bidir.agda to FinMap.agda

Helmut Grohne [Thu, 26 Jan 2012 14:24:41 +0000 (15:24 +0100)]

Helmut Grohne [Thu, 26 Jan 2012 14:22:09 +0000 (15:22 +0100)]
reduce usage of sym

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

Helmut Grohne [Thu, 26 Jan 2012 14:07:04 +0000 (15:07 +0100)]
open \==-Reasoning at top level

Helmut Grohne [Thu, 26 Jan 2012 13:51:21 +0000 (14:51 +0100)]
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

Helmut Grohne [Thu, 26 Jan 2012 10:45:06 +0000 (11:45 +0100)]
complete the yes part of lemma-checkInsert-generate using inspect

Helmut Grohne [Thu, 26 Jan 2012 10:37:44 +0000 (11:37 +0100)]
change lemma-insert-same to work with \== proofs

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

Helmut Grohne [Mon, 23 Jan 2012 18:51:55 +0000 (19:51 +0100)]
base case of lemma-2

Helmut Grohne [Mon, 23 Jan 2012 10:50:28 +0000 (11:50 +0100)]
rewrite lemma-1 using propositional equality

Helmut Grohne [Sun, 22 Jan 2012 22:11:19 +0000 (23:11 +0100)]
actually fmap is what I meant instead of >>=

Helmut Grohne [Sun, 22 Jan 2012 21:59:17 +0000 (22:59 +0100)]
introduce >>= on Maybe to improve readability

Helmut Grohne [Sun, 22 Jan 2012 21:47:39 +0000 (22:47 +0100)]

Helmut Grohne [Sun, 22 Jan 2012 21:43:32 +0000 (22:43 +0100)]
formulate theorem-1

Helmut Grohne [Sun, 22 Jan 2012 21:36:16 +0000 (22:36 +0100)]
formulate lemma-2

Helmut Grohne [Sun, 22 Jan 2012 15:40:58 +0000 (16:40 +0100)]
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.

Helmut Grohne [Sat, 21 Jan 2012 11:22:34 +0000 (12:22 +0100)]
rewrite generate using zip and fromAscList

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

Helmut Grohne [Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100)]
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.

Helmut Grohne [Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100)]
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.

Helmut Grohne [Thu, 19 Jan 2012 11:11:01 +0000 (12:11 +0100)]
first attempt to define bff (with holes)

Helmut Grohne [Thu, 19 Jan 2012 10:47:16 +0000 (11:47 +0100)]
employ standard library of agda where possible

Helmut Grohne [Thu, 19 Jan 2012 10:33:17 +0000 (11:33 +0100)]
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.

Helmut Grohne [Thu, 19 Jan 2012 10:31:52 +0000 (11:31 +0100)]