summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2012-09-26use _\==n_ and _\notin_ instead of \negHelmut Grohne
Consistent. Shorter.
2012-09-26rename suc-\== to suc-injectiveHelmut Grohne
This way of naming things is more similar to the standard library and to my own \::-injective. Suggested by Andres Loeh.
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-18one more application of lemma-just\==nnothingHelmut Grohne
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-14\::-subst is a special case of subst-congHelmut Grohne
2012-09-14vec-len-via-list and length-toList are the sameHelmut Grohne
2012-09-14complete missing parts of LiftGetHelmut Grohne
Thanks to Joachim Breitner and Wouter Swierstra for their encouragement and hints. Note that the result duplicates work at this point, but the proofs are complete.
2012-09-11show fromList-toList in the subst formHelmut Grohne
Thanks to Joachim Breitner for assisting and pointing to proof-irrelevance.
2012-09-11LiftGet: replace vec-length-same with toList-substHelmut Grohne
The name vec-length-same hides the fact that it eliminates a toList and a fromList. Actually a more generic form without fromList is possible. Thanks to Joachim Breitner for spotting.
2012-09-10LiftGet: vec-length is also known as subst (Vec A)Helmut Grohne
Thanks to Andres Löh for spotting.
2012-09-08give a sufficient precondition for theorem-2Helmut Grohne
If get on Fin results in Vecs whose elements are unique, then theorem-2 can be applied.
2012-09-04rewrite main theorems to using Vec instead of ListHelmut Grohne
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-03 05:01:04 +0000