summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-11-22shorten line length of theorem-1Helmut Grohne
2012-11-19turn lemma-fmap-just parameter into implicitHelmut Grohne
2012-11-19we can also drop an implicit parameter from assoc-enoughHelmut Grohne
2012-11-19we can use one more \exists in assoc-enoughHelmut Grohne
2012-11-19strip prose from assoc-enoughHelmut 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-11-02rewrite checkInsert using "... |" notationHelmut Grohne
Less characters => more readable.
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-22Merge branch 'modparam'Helmut Grohne
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-22also parameterize PrecondHelmut Grohne
The import of CheckInsert was broken in previous commit.
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-10-05remove VecRevBFFHelmut Grohne
The case is not interesting, because it is too restricted. The defined get-type requires a bijection between input length and output length. Since it requires polymorphism we get a reverse get-len via free theorems and both compositions are required to be identities. Thus the case is restricted without providing new insights.
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.
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-01 20:52:06 +0000