summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-07-21import _>>=_ and fmap from Data.MaybeHelmut Grohne
Also rename fmap to _<$>_ to match Agda naming conventions. The imported _>>=_ appears to have different binding, so some braces were necessary.
2013-04-19move lemma-\notin-lookupM-assoc to PrecondHelmut Grohne
This removes imports.
2013-04-18trim lemma-union-restrictHelmut Grohne
2013-04-14simpler formulation of All-differentHelmut Grohne
2013-04-10lemma-map-lookupM-assoc is even simplerHelmut 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-09rewrite lemma-map-lookupM-assocHelmut 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-01employ insertionresult in lemma-lookupM-checkInsertHelmut Grohne
2013-01-28drop the insert- prefix from the insertionresult ctorsHelmut Grohne
2013-01-28polish lemmata in FinMapHelmut Grohne
2013-01-17Merge branch view2 into masterHelmut Grohne
Get rid of checkInsertProof entirely. Conflicts: Bidir.agda (change of lemma-just\==nnothing vs. checkInsertProof removal)
2013-01-14shrink lemma-union-not-used by matching on All's ctorHelmut Grohne
2013-01-14define a more useful version of lemma-just\==nnothingHelmut 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-12introduce a proper view on checkInsertHelmut 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-10clean imports of PrecondHelmut Grohne
2013-01-10use different formulation of all-differentHelmut Grohne
Suggested by Joachim Breitner.
2013-01-10Merge 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-10reduce a precondition of lemma-checkInsert-lookupMHelmut Grohne
Now it looks a lot more like lemma-lookupM-insert-other, so rename it to lemma-lookupM-checkInsert-other.
2013-01-10rewrite lemma-\notin-lookupM-assocHelmut Grohne
It can be shortened considerably using lemma-checkInsert-lookupM.
2013-01-10add new lemma-checkInsert-lookupMHelmut Grohne
Suggested by Joachim Breitner.
2013-01-09simplify lemma-lookupM-checkInsert using case-splitHelmut Grohne
2013-01-05shrink lemma-union-not-used using cong\_2Helmut Grohne
2013-01-05shrink lemma-tabulate-\circ using cong\_2Helmut Grohne
2013-01-05shrink lemma-map-lookupM-insert using cong\_2Helmut Grohne
2013-01-05shrink base case of lemma-/notin-lookupM-assocHelmut Grohne
2012-12-14un-inline different-dropHelmut Grohne
2012-12-10drop unused importHelmut Grohne
2012-12-10get rid of contrapositionHelmut Grohne
Using function composition in all other places already.
2012-12-10drop unused param from lemma-map-lookupM-insertHelmut Grohne
2012-12-07reduce useless case in lemma-map-lookupM-assocHelmut Grohne
2012-11-22shorten line length of lemma-lookupM-checkInsertHelmut Grohne
2012-11-22shorten line lengths lemma-union-restrictHelmut Grohne
2012-11-22shorten line lengths of theorem-2Helmut Grohne
2012-11-22shorten line length of theorem-1Helmut Grohne
2012-11-19turn lemma-fmap-just parameter into implicitHelmut Grohne
2012-11-19we can also drop an implicit parameter from assoc-enoughHelmut Grohne
2012-11-19we can use one more \exists in assoc-enoughHelmut Grohne
2012-11-19strip prose from assoc-enoughHelmut Grohne
2012-11-17strip prose from lemma-1 and lemma-2Helmut Grohne
The more compact notation excluding refl transformations will also be used in the paper version.
2012-11-02rewrite checkInsert using "... |" notationHelmut Grohne
Less characters => more readable.
2012-10-25similarly rename lemma-from-map-just to map-just-injectiveHelmut Grohne
2012-10-25rename lemma-from-just to just-injectiveHelmut Grohne
We already have suc-injective and \::-injective. Consistency!
2012-10-22Merge branch 'modparam'Helmut Grohne
2012-10-22finally parameterize CheckInsertHelmut Grohne
Also adapt depending modules. Long lines generally become shorter. The misleading name "EqInst" (hiding the decidability) got discarded.
2012-10-22now parameterize BFFHelmut Grohne
And update Bidir and Precond, cause they import BFF.
2012-10-22also parameterize PrecondHelmut Grohne
The import of CheckInsert was broken in previous commit.
2012-10-22parameterize Bidir via Carrier and deqHelmut Grohne
This avoids passing around the decidable equality explicitly.
2012-10-05move all postulates to one moduleHelmut Grohne
This should make it easier to see what is assumed.
2012-10-05remove VecRevBFFHelmut 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-27remove getVec-getlen in favour of plain substHelmut Grohne
2012-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-03 07:01:14 +0000