| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
Special case of contradiction.
|
|
Turns out, we never use this requirement. The only place where it may
come in relevant is the free theorems. But here non-injectivity turns
out to be reasoning about multiple get functions that are selected by
the additional index each individually satisfying the free theorem and
thus commonly satisfying it as well.
|
|
Fixes compilation with Agda 2.4.2.
|
|
|
|
It fails to infer the type of MaybeFunctor._<$>_, so give it explicitly.
|
|
Generalizing both Vecs in the type of get to instances of Shaped. Thus allowing
trees and other data structures to be used.
|
|
One can use PartialShapeShape instead, so there is limited utility for
this type. It is not used directly and there also is no PartialVecShape.
|
|
Albeit long, this commit is relatively boring.
|
|
|
|
Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s)
is not Shaped in this way since its real index is only a number.
|
|
|
|
|
|
Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.
|
|
The intent is to replace some uses of Vec with a structure that also
happens to be a functor. RawFunctors from the standard library provide
no laws though, so we define a Functor structure that adds the laws. As
an additional law congruence is added, because
* Other standard library structures in Algebra.Structures also require
congruence.
* Otherwise the identity law would have to reason about different
identities.
|
|
|
|
|
|
Beyond allowing default values during shape updates, this branch simplifies
working with shapes other than Vec.
|
|
|
|
|
|
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.
|
|
|
|
The reduction in proof length is impressive.
|
|
|
|
|
|
|
|
It is now lemma-get-sequenceV and thus no longer applies the free
theorem for the function. Apart making the proof shorter, it also makes
the main use of the free theorem more visible in theorem-2.
|
|
This makes a few proofs easier and eliminates the need for sequence-map
entirely.
|
|
|
|
|
|
|
|
|
|
This is possible using the PartialVecVec implementation.
|
|
|
|
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)
|
|
|
|
The branch enables shape updates in variety of flavours:
* explicitly passing the desired target shape
* providing a plugin sput : ℕ → ℕ → Maybe ℕ
* providing a right-inverse to getlen
It also provides a backwards compatibility function to facilitate
shape-retaining updates.
|
|
|
|
We can now exploit getlen being rightinvertible and it works for drop
and sieve.
|
|
For building on the sieve example.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
The new lemma replaces two uses of lemma-fromFunc-tabulate, because the
latter exposes the implementation of FinMapMaybe, whereas the former
argues about the behaviour of FinMapMaybe. The aim of not exposing the
implementation (apart from brevity) is to enable refactoring.
|
|
|
