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

Age	Commit message (Collapse)	Author
2014-01-28	use the indexed version of the Vec Setoid	Helmut Grohne

2014-01-27	Merge branch feature-delete	Helmut Grohne
	Most conflicts stem from varying imports or added functions and a take-both approach merges them. A notable exception is theorem-2, where a new result sequence-cong was required. Apart from that, theorem-2 could be taken almost verbatim from feature-delete albeit its type coming from feature-decsetoid. Conflicts: Bidir.agda FinMap.agda Generic.agda Precond.agda
2014-01-23	show a stronger lemma-checkInsert-restrict	Helmut Grohne
	We can actually get semantic equality there without requiring anything else. Indeed this was already hinted in the BX for free paper that says, that lemma-1 holds in semantic equality.
2014-01-16	generalize lemma-insert-same to arbitrary Setoids	Helmut Grohne
	The general idea is to enable bff to use arbitrary DecSetoids. * assoc needs to learn about DecSetoid * checkInsert needs to learn about DecSetoid * InsertionResult needs to learn about Setoid * Parameters to InsertionResult.same become weaker * lemma-checkInsert-restrict should work with weaker same * lemma-insert-same needs to learn about Setoid
2013-12-17	refactor to get rid of FinMap without Maybe entirely	Helmut Grohne
	The union was the only user of this type and now it uses only partial mappings. So drop remaining uses of FinMap and make everything work with FinMapMaybe instead.
2013-12-17	update bff implementation to use delete	Helmut Grohne
	In the presence of shape-changing updates, bff needs to shrink one of the mappings before unifying them. As long the shape does not change, the union becomes a disjoint union. With this insight we can adapt the proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately theorem-2 requires more work and assoc-enough becomes non-trivial due to the introduction of mapMV.
2013-12-16	move generic functions to a new Generic module	Helmut Grohne

2013-12-16	add new functions delete, delete-many and partialize	Helmut Grohne
	and accompanying lemmata.
2013-04-18	trim lemma-union-restrict	Helmut Grohne

2013-01-28	polish lemmata in FinMap	Helmut Grohne

2013-01-14	define a more useful version of lemma-just\==nnothing	Helmut Grohne
	If one had a parameter of type just x \== nothing it could be simply refuted by case splitting. So the cases where lemma-just\==nnothing was used always employed trans to combine two results. The new version takes both results instead.
2013-01-05	shrink lemma-tabulate-\circ using cong\_2	Helmut Grohne

2012-12-10	get rid of contraposition	Helmut Grohne
	Using function composition in all other places already.
2012-11-22	shorten line lengths lemma-union-restrict	Helmut Grohne

2012-10-25	rename lemma-from-just to just-injective	Helmut Grohne
	We already have suc-injective and \::-injective. Consistency!
2012-09-26	use _\==n_ and _\notin_ instead of \neg	Helmut Grohne
	Consistent. Shorter.
2012-04-27	use fromFunc to define union	Helmut Grohne
	Semantically this is no change, but reducing to standard interface seems better.
2012-04-19	FinMap: lemma-lookupM-restrict drop useless implicit	Helmut Grohne

2012-04-19	move lemma-just!=nothing to FinMap and use it there	Helmut Grohne

2012-02-09	avoid a sym in lemma-union-restrict	Helmut Grohne

2012-02-09	s/generate/restrict/g	Helmut Grohne
	The name was deemed misleading. Nothing else changed.
2012-02-09	prove lemma-union-generate	Helmut Grohne

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