| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
|
|
This is an improved version of getVec-to-getList in that it also
transports the corresponding free theorem.
|
|
By choosing gl₁ = suc and gl₂ = id, the tail function can now be
bidirectionalized.
|
|
There is no way for Agda to infer these functions or even the intended
index Setoid, so making these explicit is rather required.
|
|
|
|
|
|
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.
|
|
|
|
The representation chosen is to give both an injection gl₁ and a
function gl₂ (formerly getlen), such that by choosing a non-identity for
gl₁ partiality of getlen can be expressed. An alternative would have
been to allow getlen to return a Maybe ℕ and have get return
maybe (Vec A) ⊤ (getlen n)
thus sending all inputs for which getlen yields nothing to tt. It seems
that while there is no way to obtain a such a getlen predicate from an
arbitrary index Setoid I, it should be possible to manufacture a Setoid
from a predicate. Thanks to Stefan Mehner for the insightful discussion.
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
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.
|
|
The biggest piece of this puzzle was establishing
get <$> mapMV f v == mapMV f (get v)
provided that the result of mapMV is just something.
lemma-union-not-used lost a "map just", but could be retained in
structure.
|
|
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.
|
|
We can actually get semantic equality there without requiring anything
else. Indeed this was already hinted in the BX for free paper that says,
that lemma-1 holds in semantic equality.
|
|
This is another step towards permitting arbitrary Setoids in bff.
|
|
We get the plain Setoid for free then.
|
|
The general idea is to enable bff to use arbitrary DecSetoids.
* assoc needs to learn about DecSetoid
* checkInsert needs to learn about DecSetoid
* InsertionResult needs to learn about Setoid
* Parameters to InsertionResult.same become weaker
* lemma-checkInsert-restrict should work with weaker same
* lemma-insert-same needs to learn about Setoid
|
|
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.
|
|
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.
|
|
|
|
|
|
and accompanying lemmata.
|
|
It is unused, has no proofs and starts to get into the way of
refactoring the union function type.
|
|
agda 2.3.0.1 supported the old notation, but 2.3.2.1 needs full
qualification.
|
|
Also rename fmap to _<$>_ to match Agda naming conventions. The imported
_>>=_ appears to have different binding, so some braces were necessary.
|
|
This removes imports.
|
|
|
|
|
|
Since we do the induction in the lemma itself now, there is no need to
defer the i =? j test to any.
|
|
Indeed the usage of is in two different places can be disentangled. What
we need is that all lookupM succeed. We already know how to express
this: _in-domain-of_. So use a separate list js to map over and require
js in-domain-of h'. This is what the original proof actually did. Just
now we can drop ph' and therefore is and xs. Also
lemma-map-lookupM-insert vanishes, because this generalized form permits
direct induction.
|
|
|
|
|
|
|
|
Get rid of checkInsertProof entirely.
Conflicts:
Bidir.agda (change of lemma-just\==nnothing
vs. checkInsertProof removal)
|
|
|
|
If one had a parameter of type just x \== nothing it could be simply
refuted by case splitting. So the cases where lemma-just\==nnothing was
used always employed trans to combine two results. The new version takes
both results instead.
|
|
Thanks to Joachim Breitner for helping me to work out the definition of
InsertionResult and to Daniel Seidel for helping me understand what
makes a view.
|
|
|
|
Suggested by Joachim Breitner.
|
|
This branch splits lemma-\notin-lookupM-assoc into an offspring
lemma-lookupM-checkInsert-other in the spirit of lemma-lookupM-insert-other.
|
|
Now it looks a lot more like lemma-lookupM-insert-other, so rename it to
lemma-lookupM-checkInsert-other.
|
|
It can be shortened considerably using lemma-checkInsert-lookupM.
|
|
Suggested by Joachim Breitner.
|
