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

Age	Commit message (Collapse)	Author
2012-02-09	s/generate/restrict/g	Helmut Grohne
	The name was deemed misleading. Nothing else changed.
2012-02-09	rephrase free-theorem-list-list using pointwise equality	Helmut Grohne

2012-02-09	formulate theorem-2	Helmut Grohne

2012-02-09	prove lemma-union-generate	Helmut Grohne

2012-02-09	prove theorem-1 assuming a lemma-union-generate	Helmut Grohne

2012-02-09	started proving theorem-1	Helmut Grohne
	As in the bff paper expand s using lemma-map-denumerate-enumerate and apply free-theorem-list-list to commute get and map.
2012-02-09	introduce denumerate	Helmut Grohne
	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.
2012-01-31	replace idrange with enumerate	Helmut Grohne
	Looks like uses of idrange would always be passed a length, so move it inside the definition.
2012-01-31	postulate free theorem for List a -> List a	Helmut Grohne

2012-01-26	recursion of lemma-2	Helmut Grohne

2012-01-26	started proving lemma-2	Helmut Grohne
	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
2012-01-26	reduce imports to speed up agda-mode	Helmut Grohne

2012-01-26	split Bidir.agda to FinMap.agda	Helmut Grohne

2012-01-26	improve readability using spaces	Helmut Grohne

2012-01-26	reduce usage of sym	Helmut Grohne
	Try to always construct statements of the form complex expression \== simple expression.
2012-01-26	open \==-Reasoning at top level	Helmut Grohne

2012-01-26	prove the remaining parts of lemma-checkInsert-generate	Helmut Grohne
	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
2012-01-26	complete the yes part of lemma-checkInsert-generate using inspect	Helmut Grohne

2012-01-26	change lemma-insert-same to work with \== proofs	Helmut Grohne
	This way the inserted value is not hidden in the Is-Just proof object.
2012-01-23	base case of lemma-2	Helmut Grohne

2012-01-23	rewrite lemma-1 using propositional equality	Helmut Grohne

2012-01-22	actually fmap is what I meant instead of >>=	Helmut Grohne

2012-01-22	introduce >>= on Maybe to improve readability	Helmut Grohne

2012-01-22	improve readability by introducing EqInst	Helmut Grohne

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.