| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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 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.
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The more compact notation excluding refl transformations will also be
used in the paper version.
|
|
|
|
We already have suc-injective and \::-injective. Consistency!
|
|
Also adapt depending modules. Long lines generally become shorter. The
misleading name "EqInst" (hiding the decidability) got discarded.
|
|
And update Bidir and Precond, cause they import BFF.
|
|
This avoids passing around the decidable equality explicitly.
|
|
This should make it easier to see what is assumed.
|
|
|
|
Consistent. Shorter.
|
|
This makes things a little shorter and more readable.
|
|
Conflict in Bidir.agda:
master removed a with i \=? j and using-vec reduced cases that became
absurd during Vec transformation.
|
|
Since \negp can be written as i\innis \circ here.
|
|
Thanks to Wouter Swierstra for pointing to the keyword.
|
|
|
|
|
|
|
|
Even though they are the same.
|
|
|
