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

Age	Commit message (Collapse)	Author
2013-01-10	reduce a precondition of lemma-checkInsert-lookupM	Helmut Grohne
	Now it looks a lot more like lemma-lookupM-insert-other, so rename it to lemma-lookupM-checkInsert-other.
2013-01-10	rewrite lemma-\notin-lookupM-assoc	Helmut Grohne
	It can be shortened considerably using lemma-checkInsert-lookupM.
2013-01-05	shrink lemma-union-not-used using cong\_2	Helmut Grohne

2013-01-05	shrink lemma-map-lookupM-insert using cong\_2	Helmut Grohne

2013-01-05	shrink base case of lemma-/notin-lookupM-assoc	Helmut Grohne

2012-12-10	drop unused import	Helmut Grohne

2012-12-10	drop unused param from lemma-map-lookupM-insert	Helmut Grohne

2012-12-07	reduce useless case in lemma-map-lookupM-assoc	Helmut Grohne

2012-11-22	shorten line lengths of theorem-2	Helmut Grohne

2012-11-22	shorten line length of theorem-1	Helmut Grohne

2012-11-19	turn lemma-fmap-just parameter into implicit	Helmut Grohne

2012-11-17	strip prose from lemma-1 and lemma-2	Helmut Grohne
	The more compact notation excluding refl transformations will also be used in the paper version.
2012-10-25	similarly rename lemma-from-map-just to map-just-injective	Helmut Grohne

2012-10-25	rename lemma-from-just to just-injective	Helmut Grohne
	We already have suc-injective and \::-injective. Consistency!
2012-10-22	finally parameterize CheckInsert	Helmut Grohne
	Also adapt depending modules. Long lines generally become shorter. The misleading name "EqInst" (hiding the decidability) got discarded.
2012-10-22	now parameterize BFF	Helmut Grohne
	And update Bidir and Precond, cause they import BFF.
2012-10-22	parameterize Bidir via Carrier and deq	Helmut Grohne
	This avoids passing around the decidable equality explicitly.
2012-10-05	move all postulates to one module	Helmut Grohne
	This should make it easier to see what is assumed.
2012-09-27	move definition of get-type to BFF and use it everywhere	Helmut Grohne

2012-09-26	use _\==n_ and _\notin_ instead of \neg	Helmut Grohne
	Consistent. Shorter.
2012-09-26	import [_] instead of Reveal_is_	Helmut Grohne
	This makes things a little shorter and more readable.
2012-09-18	Merge branch 'using-vec'	Helmut Grohne
	Conflict in Bidir.agda: master removed a with i \=? j and using-vec reduced cases that became absurd during Vec transformation.
2012-09-17	save a with in lemma-\inn-lookupM-assoc	Helmut Grohne
	Since \negp can be written as i\innis \circ here.
2012-09-14	employ rewrite in lemma-map-lookupM-assoc	Helmut Grohne
	Thanks to Wouter Swierstra for pointing to the keyword.
2012-09-04	rewrite main theorems to using Vec instead of List	Helmut Grohne

2012-06-05	move bff and friends to submodule ListBFF	Helmut Grohne

2012-06-05	move checkInsert and related properties to CheckInsert.agda	Helmut Grohne

2012-04-27	lemma-2: do not confuse lookup with lookupM	Helmut Grohne
	Even though they are the same.
2012-04-27	prove the theorem-2	Helmut Grohne

2012-04-20	remove lemma-\in-lookupM-assoc	Helmut Grohne
	It is a special case of lemma-assoc-domain.
2012-04-20	complete lemma-2 using new property _in-domain-of_	Helmut Grohne
	Reasoning about assoc ... = just ... has turned out to be difficult for inductive arguments. This is why I defined a new property between a List (Fin n) and a FinMapMaybe n A. Thanks to Janis Voigtlaender for suggesting this. lemma-assoc-domain transforms a property about assoc into a domain property which can be used to complete the missing pieces of lemma-2.
2012-04-19	reduce hole in lemma-2	Helmut Grohne
	Introduce lemma-map-lookupM-assoc. It branches on whether the newly inserted element is already present. To employ the results of this branch two new lemmata lemma-\in-lookupM-assoc and lemma-\notin-lookupM-assoc are used and they need lemma-lookupM-checkInsert. The remaining hole in lemma-map-lookupM-assoc targets the case where the checkInsert actually is an insert of a new element. It probably needs more thinking to get this case right.
2012-04-19	move lemma-just!=nothing to FinMap and use it there	Helmut Grohne

2012-04-17	inline bot-elim into lemma-just-nothing	Helmut Grohne
	Seems like the more common use case.
2012-04-04	abstract proofs over checkInsert	Helmut Grohne
	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.
2012-03-16	fix wrong function name in lemma-2	Helmut Grohne
	lookup and lookupM reference the same function, but serve different purposes.
2012-02-09	remove useless braces	Helmut Grohne

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