summaryrefslogtreecommitdiff
path: root/Bidir.agda
AgeCommit message (Collapse)Author
2013-12-17update bff implementation to use deleteHelmut 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-16move generic functions to a new Generic moduleHelmut Grohne
2013-10-02need 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-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-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-01-28drop the insert- prefix from the insertionresult ctorsHelmut 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-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-05shrink lemma-union-not-used 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-10drop unused importHelmut Grohne
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 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-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-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-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-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-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
2012-09-26use _\==n_ and _\notin_ instead of \negHelmut Grohne
Consistent. Shorter.
2012-09-26import [_] instead of Reveal_is_Helmut Grohne
This makes things a little shorter and more readable.
2012-09-18Merge 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.
2012-09-17save a with in lemma-\inn-lookupM-assocHelmut Grohne
Since \negp can be written as i\innis \circ here.
2012-09-14employ rewrite in lemma-map-lookupM-assocHelmut Grohne
Thanks to Wouter Swierstra for pointing to the keyword.
2012-09-04rewrite main theorems to using Vec instead of ListHelmut Grohne
2012-06-05move bff and friends to submodule ListBFFHelmut Grohne
2012-06-05move checkInsert and related properties to CheckInsert.agdaHelmut Grohne
2012-04-27lemma-2: do not confuse lookup with lookupMHelmut Grohne
Even though they are the same.
2012-04-27prove the theorem-2Helmut Grohne
2012-04-20remove lemma-\in-lookupM-assocHelmut Grohne
It is a special case of lemma-assoc-domain.
2012-04-20complete lemma-2 using new property _in-domain-of_Helmut Grohne
Reasoning about assoc ... = just ... has turned out to be difficult for inductive arguments. This is why I defined a new property between a List (Fin n) and a FinMapMaybe n A. Thanks to Janis Voigtlaender for suggesting this. lemma-assoc-domain transforms a property about assoc into a domain property which can be used to complete the missing pieces of lemma-2.
2012-04-19reduce hole in lemma-2Helmut Grohne
Introduce lemma-map-lookupM-assoc. It branches on whether the newly inserted element is already present. To employ the results of this branch two new lemmata lemma-\in-lookupM-assoc and lemma-\notin-lookupM-assoc are used and they need lemma-lookupM-checkInsert. The remaining hole in lemma-map-lookupM-assoc targets the case where the checkInsert actually is an insert of a new element. It probably needs more thinking to get this case right.
2012-04-19move lemma-just!=nothing to FinMap and use it thereHelmut Grohne
2012-04-17inline bot-elim into lemma-just-nothingHelmut Grohne
Seems like the more common use case.
2012-04-04abstract proofs over checkInsertHelmut Grohne
All proofs about expressions containing checkInsert share a common pattern. There are three cases: 1) Inserting a key-value-pair that is already present in the map. 2) Inserting a new key into the map. 3) Failure to insert a conflicting key-value pair in the map. The checkInsertProof record enables to write three different cases reducing the usage of "with" (and thus line length) in lemma-checkInsert-restrict and lemma-lookupM-assoc.
2012-03-16fix wrong function name in lemma-2Helmut Grohne
lookup and lookupM reference the same function, but serve different purposes.
2012-02-09remove useless bracesHelmut Grohne
2012-02-09s/generate/restrict/gHelmut Grohne
The name was deemed misleading. Nothing else changed.
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-02 04:30:18 +0000