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

Age	Commit message (Collapse)	Author
2014-01-17	show that Vec is an indexed Setoid	Helmut Grohne
	We get the plain Setoid for free then.
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-16	add a mapM variant on the Maybe monad on Vecs	Helmut Grohne

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-12-16	get rid of the ListBFF implementation	Helmut Grohne
	It is unused, has no proofs and starts to get into the way of refactoring the union function type.
2013-10-02	need to fully qualify Data.List.All._::_	Helmut Grohne
	agda 2.3.0.1 supported the old notation, but 2.3.2.1 needs full qualification.
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-18	trim lemma-union-restrict	Helmut Grohne

2013-04-14	simpler formulation of All-different	Helmut Grohne

2013-04-10	lemma-map-lookupM-assoc is even simpler	Helmut Grohne
	Since we do the induction in the lemma itself now, there is no need to defer the i =? j test to any.
2013-04-09	rewrite lemma-map-lookupM-assoc	Helmut Grohne
	Indeed the usage of is in two different places can be disentangled. What we need is that all lookupM succeed. We already know how to express this: _in-domain-of_. So use a separate list js to map over and require js in-domain-of h'. This is what the original proof actually did. Just now we can drop ph' and therefore is and xs. Also lemma-map-lookupM-insert vanishes, because this generalized form permits direct induction.
2013-02-01	employ insertionresult in lemma-lookupM-checkInsert	Helmut Grohne

2013-01-28	drop the insert- prefix from the insertionresult ctors	Helmut Grohne

2013-01-28	polish lemmata in FinMap	Helmut Grohne

2013-01-17	Merge branch view2 into master	Helmut Grohne
	Get rid of checkInsertProof entirely. Conflicts: Bidir.agda (change of lemma-just\==nnothing vs. checkInsertProof removal)
2013-01-14	shrink lemma-union-not-used by matching on All's ctor	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-12	introduce a proper view on checkInsert	Helmut Grohne
	Thanks to Joachim Breitner for helping me to work out the definition of InsertionResult and to Daniel Seidel for helping me understand what makes a view.
2013-01-10	clean imports of Precond	Helmut Grohne

2013-01-10	use different formulation of all-different	Helmut Grohne
	Suggested by Joachim Breitner.
2013-01-10	Merge branch 'newlemma'	Helmut Grohne
	This branch splits lemma-\notin-lookupM-assoc into an offspring lemma-lookupM-checkInsert-other in the spirit of lemma-lookupM-insert-other.
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-10	add new lemma-checkInsert-lookupM	Helmut Grohne
	Suggested by Joachim Breitner.
2013-01-09	simplify lemma-lookupM-checkInsert using case-split	Helmut Grohne

2013-01-05	shrink lemma-union-not-used using cong\_2	Helmut Grohne

2013-01-05	shrink lemma-tabulate-\circ 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-14	un-inline different-drop	Helmut Grohne

2012-12-10	drop unused import	Helmut Grohne

2012-12-10	get rid of contraposition	Helmut Grohne
	Using function composition in all other places already.
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 length of lemma-lookupM-checkInsert	Helmut Grohne

2012-11-22	shorten line lengths lemma-union-restrict	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-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-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-11-02	rewrite checkInsert using "... \|" notation	Helmut Grohne
	Less characters => more readable.
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	Merge branch 'modparam'	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.