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

Age	Commit message (Collapse)	Author
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.
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-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-10-05	remove VecRevBFF	Helmut Grohne
	The case is not interesting, because it is too restricted. The defined get-type requires a bijection between input length and output length. Since it requires polymorphism we get a reverse get-len via free theorems and both compositions are required to be identities. Thus the case is restricted without providing new insights.
2012-09-27	remove getVec-getlen in favour of plain subst	Helmut Grohne

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	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-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.