summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-08-30prove LiftGet.get-trafo-2-getlenHelmut Grohne
2012-08-30phrase other half of bijection in LiftGetHelmut Grohne
2012-08-30prove half of the bijection in LiftGetHelmut Grohne
2012-08-30give the type of different gets a nameHelmut Grohne
2012-08-06attempt isomorphism between get on List and on VecHelmut Grohne
Thus far we have found maps in both directions but lack statements about the composition of them.
2012-06-19third definition of bffHelmut Grohne
It is a definition based on Vec but with less assumptions. The VecBFF has therefore been renamed to VecRevBFF. VecBFF uses get : \forall n \exists m -> Vec A n -> Vec a m VecRevBFF uses get : \forall m \exists n -> Vec A n -> Vec a m
2012-06-05make the Vec bff more similar to the List versionHelmut Grohne
2012-06-05define a bff over VecHelmut 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-27use fromFunc to define unionHelmut Grohne
Semantically this is no change, but reducing to standard interface seems better.
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-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.
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-03 05:26:42 +0000