summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-09-10LiftGet: vec-length is also known as subst (Vec A)Helmut Grohne
Thanks to Andres Löh for spotting.
2012-09-04formulate List <-> Vec isomorphism problemsHelmut Grohne
There are now like four open holes in LiftGet.agda that all boil down to the same problem. For proving equalities on Vec we first need to show that those Vecs actually have the same type. Proofs on two different levels are needed and somehow need to be merged.
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-03 05:01:46 +0000