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

Age	Commit message (Collapse)	Author
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-27	cleanup unused functions and useless steps	Helmut Grohne

2014-01-27	prove assoc-enough in the presence of delete	Helmut Grohne
	The old definition of bff had a single failure mode - assoc - and its proof was a single cong. Now we need to show that the other failure mode - mapM (flip lookupM ...) - is eliminated by the success of the former resulting in a larger proof.
2014-01-23	generalize BFF and theorem-2 to arbitrary Setoids	Helmut Grohne
	Since the generalization of lemma-checkInsert-restrict there is nothing to show for theorem-1. So everything works with Setoids now yielding the same results as the paper proofs.
2014-01-17	generalize checkInsert to arbitrary Setoids	Helmut Grohne
	This is another step towards permitting arbitrary Setoids in bff.
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-07-21	import _>>=_ and fmap from Data.Maybe	Helmut Grohne
	Also rename fmap to _<$>_ to match Agda naming conventions. The imported _>>=_ appears to have different binding, so some braces were necessary.
2013-04-19	move lemma-\notin-lookupM-assoc to Precond	Helmut Grohne
	This removes imports.
2013-04-14	simpler formulation of All-different	Helmut Grohne

2013-01-10	clean imports of Precond	Helmut Grohne

2013-01-10	use different formulation of all-different	Helmut Grohne
	Suggested by Joachim Breitner.
2012-12-14	un-inline different-drop	Helmut Grohne

2012-11-19	we can also drop an implicit parameter from assoc-enough	Helmut Grohne

2012-11-19	we can use one more \exists in assoc-enough	Helmut Grohne

2012-11-19	strip prose from assoc-enough	Helmut Grohne

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	also parameterize Precond	Helmut Grohne
	The import of CheckInsert was broken in previous commit.
2012-09-27	move definition of get-type to BFF and use it everywhere	Helmut Grohne

2012-09-26	rename suc-\== to suc-injective	Helmut Grohne
	This way of naming things is more similar to the standard library and to my own \::-injective. Suggested by Andres Loeh.
2012-09-08	give a sufficient precondition for theorem-2	Helmut Grohne
	If get on Fin results in Vecs whose elements are unique, then theorem-2 can be applied.