summaryrefslogtreecommitdiff
path: root/Precond.agda
AgeCommit message (Collapse)Author
2014-11-26fix compilation against agda stdlib 0.9Helmut Grohne
2014-10-30make more parameters implicitHelmut Grohne
All of these changes were applied to functions of type ... -> (x : ...) -> ... == x -> ... where x could be preceded by just making the x implicit, because it can be uniquely deduced from the equality proof.
2014-10-21move all those toList calls inside _in-domain-of_Helmut Grohne
2014-10-16sym result of lemma-lookupM-{i,checkI}nsert-otherHelmut Grohne
Typically we have the complex term on the LHS and the simplified term on the RHS. These lemmata did it otherwise and by symming them, we save two syms.
2014-03-10also allow Shaped types for the viewHelmut Grohne
Albeit long, this commit is relatively boring.
2014-03-10port precondition to PartialShapeVecHelmut Grohne
2014-03-07use allFin rather than tabulate idHelmut Grohne
2014-02-26weaken assumptions made by theorem-2 and asssoc-enoughHelmut Grohne
2014-02-26remove the sequenceV call from bffHelmut Grohne
This allows bff to be more precise with regard to its failure modes, even though we are not yet making use of that projected precision. It allows inserting a default value for entries that could not be recovered in a shape changing update as described in VoigtlaenderHMW13.
2014-02-24define fromFunc more convenientlyHelmut Grohne
2014-02-24define mapMV via sequenceVHelmut Grohne
This makes a few proofs easier and eliminates the need for sequence-map entirely.
2014-02-17Merge branch feature-partial-getlen into masterHelmut Grohne
It allows defining get functions that are only defined for some vector lengths. It retains backwards compatibility with the previous state via a VecVec compatibility module. The biggest benefit is that now standard library functions such as tail, take and drop can be passed to bff. Conflicts: heavy BFF.agda (imports, bff type clash) Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and lemma-get-mapMV) Generic.agda (imports) Precond.agda (imports, bff type clash in assoc-enough)
2014-02-07allow shape shape updates in bffHelmut Grohne
Unlike the original version in VoigtlaenderHMW13, we do not request an sput : ℕ → ℕ → Maybe ℕ function for determining the updated source shape from the original source and updated view shape. Instead we ask the caller directly to provide the result of sput together with a proof that its getlen matches with the provided, updated view. The precondition assoc-enough is not enriched in this way and still requires a non-changing shape. I.e. it says what it said before.
2014-02-05be more precise about which lookups we useHelmut Grohne
2014-02-05strip even more implementation detail in PrecondHelmut Grohne
2014-02-05strip implementation detail from lemma-union-delete-fromFuncHelmut Grohne
2014-02-04remove unused importsHelmut Grohne
Most of the became unused by using the convenience functions introduced in the parent commit.
2014-02-04add convenience members to PartialVecVec.GetHelmut Grohne
2014-02-04Merge branch feature-get-record into feature-partial-getlenHelmut Grohne
These two features heavily interconnect. As such it makes sense to integrate them properly. This non-trivial merge does that work. Compared to feature-partial-getlen a few definitions moved from FreeTheorems.agda to GetTypes.agda. Many types changed compared to both branches. Conflicts: BFF.agda Bidir.agda FreeTheorems.agda Precond.agda conflict in GetTypes.agda not detected by merge
2014-02-03make things compile with 2.3.0.1Helmut Grohne
* Remove let patter , match = foo usage * Remove Qualified.infix-symbol usage * Add non-obvious absurd patterns * Qualify constructors
2014-01-30fully allow partial get functionsHelmut Grohne
By choosing gl₁ = suc and gl₂ = id, the tail function can now be bidirectionalized.
2014-01-30allow importing of Bidir without any postulatesHelmut Grohne
2014-01-30pass get functions as recordsHelmut Grohne
This allows passing both getlen and get as a single parameter. It also allows to make the free theorem a prerequisite instead of a postulate.
2014-01-27Merge branch feature-deleteHelmut Grohne
Most conflicts stem from varying imports or added functions and a take-both approach merges them. A notable exception is theorem-2, where a new result sequence-cong was required. Apart from that, theorem-2 could be taken almost verbatim from feature-delete albeit its type coming from feature-decsetoid. Conflicts: Bidir.agda FinMap.agda Generic.agda Precond.agda
2014-01-27cleanup unused functions and useless stepsHelmut Grohne
2014-01-27prove assoc-enough in the presence of deleteHelmut Grohne
The old definition of bff had a single failure mode - assoc - and its proof was a single cong. Now we need to show that the other failure mode - mapM (flip lookupM ...) - is eliminated by the success of the former resulting in a larger proof.
2014-01-23generalize BFF and theorem-2 to arbitrary SetoidsHelmut Grohne
Since the generalization of lemma-checkInsert-restrict there is nothing to show for theorem-1. So everything works with Setoids now yielding the same results as the paper proofs.
2014-01-17generalize checkInsert to arbitrary SetoidsHelmut Grohne
This is another step towards permitting arbitrary Setoids in bff.
2013-12-17refactor to get rid of FinMap without Maybe entirelyHelmut Grohne
The union was the only user of this type and now it uses only partial mappings. So drop remaining uses of FinMap and make everything work with FinMapMaybe instead.
2013-12-17update bff implementation to use deleteHelmut Grohne
In the presence of shape-changing updates, bff needs to shrink one of the mappings before unifying them. As long the shape does not change, the union becomes a disjoint union. With this insight we can adapt the proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately theorem-2 requires more work and assoc-enough becomes non-trivial due to the introduction of mapMV.
2013-07-21import _>>=_ and fmap from Data.MaybeHelmut Grohne
Also rename fmap to _<$>_ to match Agda naming conventions. The imported _>>=_ appears to have different binding, so some braces were necessary.
2013-04-19move lemma-\notin-lookupM-assoc to PrecondHelmut Grohne
This removes imports.
2013-04-14simpler formulation of All-differentHelmut Grohne
2013-01-10clean imports of PrecondHelmut Grohne
2013-01-10use different formulation of all-differentHelmut Grohne
Suggested by Joachim Breitner.
2012-12-14un-inline different-dropHelmut 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-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-09-27move definition of get-type to BFF and use it everywhereHelmut Grohne
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-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.