| 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 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Using function composition in all other places already.
|
|
|
|
|
|
|
|
|
|
|
