| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
It is a special case of lemma-assoc-domain.
|
|
Reasoning about assoc ... = just ... has turned out to be difficult for
inductive arguments. This is why I defined a new property between a List
(Fin n) and a FinMapMaybe n A. Thanks to Janis Voigtlaender for
suggesting this. lemma-assoc-domain transforms a property about assoc
into a domain property which can be used to complete the missing pieces
of lemma-2.
|
|
Introduce lemma-map-lookupM-assoc. It branches on whether the newly
inserted element is already present. To employ the results of this
branch two new lemmata lemma-\in-lookupM-assoc and
lemma-\notin-lookupM-assoc are used and they need
lemma-lookupM-checkInsert. The remaining hole in lemma-map-lookupM-assoc
targets the case where the checkInsert actually is an insert of a new
element. It probably needs more thinking to get this case right.
|
|
|
