summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-01-10use different formulation of all-differentHelmut Grohne
Suggested by Joachim Breitner.
2013-01-10Merge branch 'newlemma'Helmut Grohne
This branch splits lemma-\notin-lookupM-assoc into an offspring lemma-lookupM-checkInsert-other in the spirit of lemma-lookupM-insert-other.
2013-01-10reduce a precondition of lemma-checkInsert-lookupMHelmut Grohne
Now it looks a lot more like lemma-lookupM-insert-other, so rename it to lemma-lookupM-checkInsert-other.
2013-01-10rewrite lemma-\notin-lookupM-assocHelmut Grohne
It can be shortened considerably using lemma-checkInsert-lookupM.
2013-01-10add new lemma-checkInsert-lookupMHelmut Grohne
Suggested by Joachim Breitner.
2013-01-09simplify lemma-lookupM-checkInsert using case-splitHelmut Grohne
2013-01-05shrink lemma-union-not-used using cong\_2Helmut Grohne
2013-01-05shrink lemma-tabulate-\circ using cong\_2Helmut Grohne
2013-01-05shrink lemma-map-lookupM-insert using cong\_2Helmut Grohne
2013-01-05shrink base case of lemma-/notin-lookupM-assocHelmut Grohne
2012-12-14un-inline different-dropHelmut Grohne
2012-12-10drop unused importHelmut Grohne
2012-12-10get rid of contrapositionHelmut Grohne
Using function composition in all other places already.
2012-12-10drop unused param from lemma-map-lookupM-insertHelmut Grohne
2012-12-07reduce useless case in lemma-map-lookupM-assocHelmut Grohne
2012-11-22shorten line length of lemma-lookupM-checkInsertHelmut Grohne
2012-11-22shorten line lengths lemma-union-restrictHelmut Grohne
2012-11-22shorten line lengths of theorem-2Helmut Grohne
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.
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-03 05:46:33 +0000