| Age | Commit message (Collapse) | Author |
|---|
|
These will happen to break with later agda-stdlib releases.
|
|
Later versions of agda will be unable to infer it unambiguously.
|
|
Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.
|
|
Broken in parent commit.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
New type suggested by Janis Voigtländer.
|
|
|
|
|
|
These became duplicates of their non-barred counterparts.
|
|
We never used the equality property. Thus a simple function is
sufficient here. We always fulfilled the property using ≡-to-Π anyway.
|
|
|
|
|
|
The major differences between them are:
* ind-cong treats the first parameter to the function implicit whereas
H.cong₂ makes it explicit.
* ind-cong expects a propositional proof for the first equality whereas
H.cong₂ asks for a heterogeneous one. Lift using H.reflexive.
|
|
|
|
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.
|
|
|
|
While they do work with Lists and there is no inherent need to know the
length, they are most often invoked in a context where a Vec needs to be
converted to a List using toList. By changing them to work with Vec,
quite a few toList calls can be dropped.
|
|
|
|
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.
|
