summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-04-19FinMap: lemma-lookupM-restrict drop useless implicitHelmut Grohne
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-09avoid a sym in lemma-union-restrictHelmut Grohne
2012-02-09s/generate/restrict/gHelmut Grohne
The name was deemed misleading. Nothing else changed.
2012-02-09rephrase free-theorem-list-list using pointwise equalityHelmut Grohne
2012-02-09formulate theorem-2Helmut Grohne
2012-02-09prove lemma-union-generateHelmut Grohne
2012-02-09prove theorem-1 assuming a lemma-union-generateHelmut Grohne
2012-02-09started proving theorem-1Helmut Grohne
As in the bff paper expand s using lemma-map-denumerate-enumerate and apply free-theorem-list-list to commute get and map.
2012-02-09introduce denumerateHelmut Grohne
It is some kind of counter part to enumerate. That is: map (denumerate s) (enumerate s) \== s It can be employed in bff and I believe it to simplify reasoning on bff.
2012-01-31replace idrange with enumerateHelmut Grohne
Looks like uses of idrange would always be passed a length, so move it inside the definition.
2012-01-31postulate free theorem for List a -> List aHelmut Grohne
2012-01-26recursion of lemma-2Helmut Grohne
2012-01-26started proving lemma-2Helmut Grohne
The step case needs two lemmata. One for the head of the resulting map and one for the tail. The head case is shown using a lemma-lookupM-assoc : assoc eq (i :: _) (x :: _) == just h -> lookupM i h == just x
2012-01-26reduce imports to speed up agda-modeHelmut Grohne
2012-01-26split Bidir.agda to FinMap.agdaHelmut Grohne
2012-01-26improve readability using spacesHelmut Grohne
2012-01-26reduce usage of symHelmut Grohne
Try to always construct statements of the form complex expression \== simple expression.
2012-01-26open \==-Reasoning at top levelHelmut Grohne
2012-01-26prove the remaining parts of lemma-checkInsert-generateHelmut Grohne
Introducing the following lemmata: * lemma-lookupM-empty : nothing \== lookupM i empty * lemma-from-just : just x \== just y -> x \== y * lemma-lookupM-insert : just a \== lookupM i (insert i a m) * lemma-lookupM-insert-other : \neg (i \== j) -> lookupM i m \== lookupM i (insert j a m) * lemma-lookupM-generate : just a = lookupM i (generate f is) -> a \== f i
2012-01-26complete the yes part of lemma-checkInsert-generate using inspectHelmut Grohne
2012-01-26change lemma-insert-same to work with \== proofsHelmut Grohne
This way the inserted value is not hidden in the Is-Just proof object.
2012-01-23base case of lemma-2Helmut Grohne
2012-01-23rewrite lemma-1 using propositional equalityHelmut Grohne
2012-01-22actually fmap is what I meant instead of >>=Helmut Grohne
2012-01-22introduce >>= on Maybe to improve readabilityHelmut Grohne
2012-01-22improve readability by introducing EqInstHelmut Grohne
2012-01-22formulate theorem-1Helmut Grohne
2012-01-22formulate lemma-2Helmut Grohne
2012-01-22attempt to prove lemma-1Helmut Grohne
In order to prove lemma-1 we first show a lemma-insert-same to show that inserting the same pair twice does not change the FinMapMaye. lemma-1 still has two goals. In the first goal agda doesn't accept "is-just (f i)". Why? The second goal is to be shown as absurd.
2012-01-21rewrite generate using zip and fromAscListHelmut Grohne
This way matches the usage in lemma-1 more closely since zip actually is something similar to assoc.
2012-01-21split FinMap to FinMapMaybeHelmut Grohne
The FinMapMaybe is what FinMap previously was. The FinMap instead now really maps its whole domain to something. This property is needed to avoid the usage of fromJust in the definition of bff. With this split applied the definition of bff is now complete.
2012-01-19replaced NatMap with FinMapHelmut Grohne
The domain of the map is always limited. So using Fin n as the domain is natural. Additionally FinMaps are now semantically equal iff their normal form is the same. That means \== can be used.
2012-01-19first attempt to define bff (with holes)Helmut Grohne
2012-01-19employ standard library of agda where possibleHelmut Grohne
2012-01-19first attempt to model lemma-1Helmut Grohne
Without using the stdlib basic data structures are defined (with the stdlib names in mind). The IntMap given in the paper is translated to a NatMap. There are definitions for checkInsert and assoc resulting in a formalization of lemma-1.
2012-01-19added .gitignoreHelmut Grohne
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-02 03:26:48 +0000