~helmut/bidiragda.git - Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)

Age	Commit message (Collapse)	Author
2012-01-22	formulate theorem-1	Helmut Grohne

2012-01-22	formulate lemma-2	Helmut Grohne

2012-01-22	attempt to prove lemma-1	Helmut Grohne
	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.
2012-01-21	rewrite generate using zip and fromAscList	Helmut Grohne
	This way matches the usage in lemma-1 more closely since zip actually is something similar to assoc.
2012-01-21	split FinMap to FinMapMaybe	Helmut Grohne
	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.
2012-01-19	replaced NatMap with FinMap	Helmut Grohne
	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.
2012-01-19	first attempt to define bff (with holes)	Helmut Grohne

2012-01-19	employ standard library of agda where possible	Helmut Grohne

2012-01-19	first attempt to model lemma-1	Helmut Grohne
	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.