Helmut Grohne [Tue, 28 Jan 2014 08:16:26 +0000 (09:16 +0100)]
cleanup unused function and import

Helmut Grohne [Mon, 27 Jan 2014 12:46:47 +0000 (13:46 +0100)]
Merge branch feature-delete

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

Helmut Grohne [Mon, 27 Jan 2014 09:50:15 +0000 (10:50 +0100)]
Merge branch feature-decsetoid

Helmut Grohne [Mon, 27 Jan 2014 08:31:56 +0000 (09:31 +0100)]
cleanup unused functions and useless steps

Helmut Grohne [Mon, 27 Jan 2014 08:02:45 +0000 (09:02 +0100)]
prove assoc-enough in the presence of delete

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.

Helmut Grohne [Fri, 24 Jan 2014 12:30:39 +0000 (13:30 +0100)]
prove theorem-2 in the presence of delete

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. Helmut Grohne [Thu, 23 Jan 2014 12:19:02 +0000 (13:19 +0100)] generalize BFF and theorem-2 to arbitrary Setoids 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. Helmut Grohne [Thu, 23 Jan 2014 10:48:54 +0000 (11:48 +0100)] show a stronger lemma-checkInsert-restrict 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. Helmut Grohne [Fri, 17 Jan 2014 08:24:47 +0000 (09:24 +0100)] generalize checkInsert to arbitrary Setoids This is another step towards permitting arbitrary Setoids in bff. Helmut Grohne [Fri, 17 Jan 2014 05:29:48 +0000 (06:29 +0100)] show that Vec is an indexed Setoid We get the plain Setoid for free then. Helmut Grohne [Thu, 16 Jan 2014 10:32:12 +0000 (11:32 +0100)] generalize lemma-insert-same to arbitrary Setoids 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 Helmut Grohne [Tue, 17 Dec 2013 07:49:24 +0000 (08:49 +0100)] refactor to get rid of FinMap without Maybe entirely 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. Helmut Grohne [Tue, 17 Dec 2013 07:22:12 +0000 (08:22 +0100)] update bff implementation to use delete 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. Helmut Grohne [Mon, 16 Dec 2013 17:10:17 +0000 (18:10 +0100)] add a mapM variant on the Maybe monad on Vecs Helmut Grohne [Mon, 16 Dec 2013 16:34:59 +0000 (17:34 +0100)] move generic functions to a new Generic module Helmut Grohne [Mon, 16 Dec 2013 15:02:21 +0000 (16:02 +0100)] add new functions delete, delete-many and partialize and accompanying lemmata. Helmut Grohne [Mon, 16 Dec 2013 14:47:53 +0000 (15:47 +0100)] get rid of the ListBFF implementation It is unused, has no proofs and starts to get into the way of refactoring the union function type. Helmut Grohne [Wed, 2 Oct 2013 08:59:57 +0000 (10:59 +0200)] need to fully qualify Data.List.All._::_ agda 2.3.0.1 supported the old notation, but 2.3.2.1 needs full qualification. Helmut Grohne [Sun, 21 Jul 2013 18:46:18 +0000 (20:46 +0200)] import _>>=_ and fmap from Data.Maybe Also rename fmap to _<$>_ to match Agda naming conventions. The imported
_>>=_ appears to have different binding, so some braces were necessary.

Helmut Grohne [Fri, 19 Apr 2013 10:08:55 +0000 (12:08 +0200)]
move lemma-\notin-lookupM-assoc to Precond

This removes imports.

Helmut Grohne [Thu, 18 Apr 2013 14:32:37 +0000 (16:32 +0200)]
trim lemma-union-restrict

Helmut Grohne [Sun, 14 Apr 2013 15:50:16 +0000 (17:50 +0200)]
simpler formulation of All-different

Helmut Grohne [Wed, 10 Apr 2013 06:26:29 +0000 (08:26 +0200)]
lemma-map-lookupM-assoc is even simpler

Since we do the induction in the lemma itself now, there is no need to
defer the i =? j test to any.

Helmut Grohne [Tue, 9 Apr 2013 19:00:14 +0000 (21:00 +0200)]
rewrite lemma-map-lookupM-assoc

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.

Helmut Grohne [Fri, 1 Feb 2013 12:13:01 +0000 (13:13 +0100)]
employ insertionresult in lemma-lookupM-checkInsert

Helmut Grohne [Mon, 28 Jan 2013 12:58:30 +0000 (13:58 +0100)]
drop the insert- prefix from the insertionresult ctors

Helmut Grohne [Mon, 28 Jan 2013 11:28:08 +0000 (12:28 +0100)]
polish lemmata in FinMap

Helmut Grohne [Thu, 17 Jan 2013 14:09:00 +0000 (15:09 +0100)]
Merge branch view2 into master

Get rid of checkInsertProof entirely.

Conflicts:
Bidir.agda (change of lemma-just\==nnothing
vs. checkInsertProof removal)

Helmut Grohne [Mon, 14 Jan 2013 13:14:30 +0000 (14:14 +0100)]
shrink lemma-union-not-used by matching on All's ctor

Helmut Grohne [Mon, 14 Jan 2013 12:13:00 +0000 (13:13 +0100)]
define a more useful version of lemma-just\==nnothing

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

Helmut Grohne [Sat, 12 Jan 2013 16:05:39 +0000 (17:05 +0100)]
introduce a proper view on checkInsert

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.

Helmut Grohne [Thu, 10 Jan 2013 12:16:42 +0000 (13:16 +0100)]
clean imports of Precond

Helmut Grohne [Thu, 10 Jan 2013 12:11:41 +0000 (13:11 +0100)]
use different formulation of all-different

Suggested by Joachim Breitner.

Helmut Grohne [Thu, 10 Jan 2013 10:18:12 +0000 (11:18 +0100)]
Merge branch 'newlemma'

This branch splits lemma-\notin-lookupM-assoc into an offspring
lemma-lookupM-checkInsert-other in the spirit of lemma-lookupM-insert-other.

Helmut Grohne [Thu, 10 Jan 2013 10:09:38 +0000 (11:09 +0100)]
reduce a precondition of lemma-checkInsert-lookupM

Now it looks a lot more like lemma-lookupM-insert-other, so rename it to
lemma-lookupM-checkInsert-other.

Helmut Grohne [Wed, 9 Jan 2013 22:46:10 +0000 (23:46 +0100)]
rewrite lemma-\notin-lookupM-assoc

It can be shortened considerably using lemma-checkInsert-lookupM.

Helmut Grohne [Wed, 9 Jan 2013 22:26:46 +0000 (23:26 +0100)]

Suggested by Joachim Breitner.

Helmut Grohne [Wed, 9 Jan 2013 22:24:58 +0000 (23:24 +0100)]
simplify lemma-lookupM-checkInsert using case-split

Helmut Grohne [Sat, 5 Jan 2013 11:03:57 +0000 (12:03 +0100)]
shrink lemma-union-not-used using cong\_2

Helmut Grohne [Sat, 5 Jan 2013 10:59:31 +0000 (11:59 +0100)]
shrink lemma-tabulate-\circ using cong\_2

Helmut Grohne [Sat, 5 Jan 2013 10:53:42 +0000 (11:53 +0100)]
shrink lemma-map-lookupM-insert using cong\_2

Helmut Grohne [Sat, 5 Jan 2013 09:41:37 +0000 (10:41 +0100)]
shrink base case of lemma-/notin-lookupM-assoc

Helmut Grohne [Fri, 14 Dec 2012 11:03:04 +0000 (12:03 +0100)]
un-inline different-drop

Helmut Grohne [Mon, 10 Dec 2012 11:48:25 +0000 (12:48 +0100)]
drop unused import

Helmut Grohne [Mon, 10 Dec 2012 10:48:15 +0000 (11:48 +0100)]
get rid of contraposition

Using function composition in all other places already.

Helmut Grohne [Mon, 10 Dec 2012 09:57:50 +0000 (10:57 +0100)]
drop unused param from lemma-map-lookupM-insert

Helmut Grohne [Thu, 6 Dec 2012 23:08:07 +0000 (00:08 +0100)]
reduce useless case in lemma-map-lookupM-assoc

Helmut Grohne [Thu, 22 Nov 2012 14:23:03 +0000 (15:23 +0100)]
shorten line length of lemma-lookupM-checkInsert

Helmut Grohne [Thu, 22 Nov 2012 14:20:29 +0000 (15:20 +0100)]
shorten line lengths lemma-union-restrict

Helmut Grohne [Thu, 22 Nov 2012 14:06:21 +0000 (15:06 +0100)]
shorten line lengths of theorem-2

Helmut Grohne [Thu, 22 Nov 2012 13:42:16 +0000 (14:42 +0100)]
shorten line length of theorem-1

Helmut Grohne [Mon, 19 Nov 2012 15:34:33 +0000 (16:34 +0100)]
turn lemma-fmap-just parameter into implicit

Helmut Grohne [Mon, 19 Nov 2012 13:56:28 +0000 (14:56 +0100)]
we can also drop an implicit parameter from assoc-enough

Helmut Grohne [Mon, 19 Nov 2012 13:48:24 +0000 (14:48 +0100)]
we can use one more \exists in assoc-enough

Helmut Grohne [Mon, 19 Nov 2012 12:33:40 +0000 (13:33 +0100)]
strip prose from assoc-enough

Helmut Grohne [Sat, 17 Nov 2012 18:24:11 +0000 (19:24 +0100)]
strip prose from lemma-1 and lemma-2

The more compact notation excluding refl transformations will also be
used in the paper version.

Helmut Grohne [Fri, 2 Nov 2012 14:19:40 +0000 (15:19 +0100)]
rewrite checkInsert using "... |" notation

Helmut Grohne [Thu, 25 Oct 2012 11:37:31 +0000 (13:37 +0200)]
similarly rename lemma-from-map-just to map-just-injective

Helmut Grohne [Thu, 25 Oct 2012 10:53:19 +0000 (12:53 +0200)]
rename lemma-from-just to just-injective

We already have suc-injective and \::-injective. Consistency!

Helmut Grohne [Mon, 22 Oct 2012 09:30:52 +0000 (11:30 +0200)]
Merge branch 'modparam'

Helmut Grohne [Mon, 22 Oct 2012 09:21:10 +0000 (11:21 +0200)]
finally parameterize CheckInsert

Also adapt depending modules. Long lines generally become shorter. The

Helmut Grohne [Mon, 22 Oct 2012 09:05:34 +0000 (11:05 +0200)]
now parameterize BFF

And update Bidir and Precond, cause they import BFF.

Helmut Grohne [Mon, 22 Oct 2012 08:50:51 +0000 (10:50 +0200)]
also parameterize Precond

The import of CheckInsert was broken in previous commit.

Helmut Grohne [Mon, 22 Oct 2012 08:42:21 +0000 (10:42 +0200)]
parameterize Bidir via Carrier and deq

This avoids passing around the decidable equality explicitly.

Helmut Grohne [Fri, 5 Oct 2012 10:47:09 +0000 (12:47 +0200)]
move all postulates to one module

This should make it easier to see what is assumed.

Helmut Grohne [Fri, 5 Oct 2012 08:58:15 +0000 (10:58 +0200)]
remove VecRevBFF

The case is not interesting, because it is too restricted. The defined
get-type requires a bijection between input length and output length.
Since it requires polymorphism we get a reverse get-len via free
theorems and both compositions are required to be identities. Thus the
case is restricted without providing new insights.

Helmut Grohne [Thu, 27 Sep 2012 11:55:29 +0000 (13:55 +0200)]
remove getVec-getlen in favour of plain subst

Helmut Grohne [Thu, 27 Sep 2012 11:11:53 +0000 (13:11 +0200)]
move definition of get-type to BFF and use it everywhere

Helmut Grohne [Wed, 26 Sep 2012 20:02:48 +0000 (22:02 +0200)]
use _\==n_ and _\notin_ instead of \neg

Consistent. Shorter.

Helmut Grohne [Wed, 26 Sep 2012 14:14:52 +0000 (16:14 +0200)]
rename suc-\== to suc-injective

This way of naming things is more similar to the standard library and to
my own \::-injective. Suggested by Andres Loeh.

Helmut Grohne [Wed, 26 Sep 2012 13:35:32 +0000 (15:35 +0200)]

This makes things a little shorter and more readable.

Helmut Grohne [Tue, 18 Sep 2012 07:28:00 +0000 (09:28 +0200)]
Merge branch 'using-vec'

Conflict in Bidir.agda:
master removed a with i \=? j and using-vec reduced cases that became
absurd during Vec transformation.

Helmut Grohne [Tue, 18 Sep 2012 06:28:08 +0000 (08:28 +0200)]
one more application of lemma-just\==nnothing

Helmut Grohne [Mon, 17 Sep 2012 20:17:02 +0000 (22:17 +0200)]
save a with in lemma-\inn-lookupM-assoc

Since \negp can be written as i\innis \circ here.

Helmut Grohne [Fri, 14 Sep 2012 18:41:26 +0000 (20:41 +0200)]
employ rewrite in lemma-map-lookupM-assoc

Thanks to Wouter Swierstra for pointing to the keyword.

Helmut Grohne [Fri, 14 Sep 2012 17:42:30 +0000 (19:42 +0200)]
\::-subst is a special case of subst-cong

Helmut Grohne [Fri, 14 Sep 2012 15:23:58 +0000 (17:23 +0200)]
vec-len-via-list and length-toList are the same

Helmut Grohne [Fri, 14 Sep 2012 12:00:57 +0000 (14:00 +0200)]
complete missing parts of LiftGet

Thanks to Joachim Breitner and Wouter Swierstra for their encouragement
and hints. Note that the result duplicates work at this point, but the
proofs are complete.

Helmut Grohne [Tue, 11 Sep 2012 21:36:41 +0000 (23:36 +0200)]
show fromList-toList in the subst form

Thanks to Joachim Breitner for assisting and pointing to
proof-irrelevance.

Helmut Grohne [Tue, 11 Sep 2012 21:33:29 +0000 (23:33 +0200)]
LiftGet: replace vec-length-same with toList-subst

The name vec-length-same hides the fact that it eliminates a toList and
a fromList. Actually a more generic form without fromList is possible.
Thanks to Joachim Breitner for spotting.

Helmut Grohne [Mon, 10 Sep 2012 20:34:16 +0000 (22:34 +0200)]
LiftGet: vec-length is also known as subst (Vec A)

Thanks to Andres Löh for spotting.

Helmut Grohne [Sat, 8 Sep 2012 07:01:57 +0000 (09:01 +0200)]
give a sufficient precondition for theorem-2

If get on Fin results in Vecs whose elements are unique, then theorem-2
can be applied.

Helmut Grohne [Tue, 4 Sep 2012 07:32:52 +0000 (09:32 +0200)]
rewrite main theorems to using Vec instead of List

Helmut Grohne [Tue, 4 Sep 2012 06:42:38 +0000 (08:42 +0200)]
formulate List <-> Vec isomorphism problems

There are now like four open holes in LiftGet.agda that all boil down to
the same problem. For proving equalities on Vec we first need to show
that those Vecs actually have the same type. Proofs on two different
levels are needed and somehow need to be merged.

Helmut Grohne [Thu, 30 Aug 2012 14:50:21 +0000 (16:50 +0200)]
prove LiftGet.get-trafo-2-getlen

Helmut Grohne [Thu, 30 Aug 2012 13:59:56 +0000 (15:59 +0200)]
phrase other half of bijection in LiftGet

Helmut Grohne [Thu, 30 Aug 2012 13:33:46 +0000 (15:33 +0200)]
prove half of the bijection in LiftGet

Helmut Grohne [Thu, 30 Aug 2012 12:18:54 +0000 (14:18 +0200)]
give the type of different gets a name

Helmut Grohne [Mon, 6 Aug 2012 17:18:41 +0000 (19:18 +0200)]
attempt isomorphism between get on List and on Vec

Thus far we have found maps in both directions but lack statements about
the composition of them.

Helmut Grohne [Tue, 19 Jun 2012 14:28:03 +0000 (16:28 +0200)]
third definition of bff

It is a definition based on Vec but with less assumptions. The VecBFF
has therefore been renamed to VecRevBFF.

VecBFF uses get : \forall n \exists m -> Vec A n -> Vec a m
VecRevBFF uses get : \forall m \exists n -> Vec A n -> Vec a m

Helmut Grohne [Tue, 5 Jun 2012 16:03:51 +0000 (18:03 +0200)]
make the Vec bff more similar to the List version

Helmut Grohne [Tue, 5 Jun 2012 13:37:18 +0000 (15:37 +0200)]
define a bff over Vec

Helmut Grohne [Tue, 5 Jun 2012 13:35:09 +0000 (15:35 +0200)]
move bff and friends to submodule ListBFF

Helmut Grohne [Tue, 5 Jun 2012 12:12:10 +0000 (14:12 +0200)]
move checkInsert and related properties to CheckInsert.agda

Helmut Grohne [Fri, 27 Apr 2012 18:53:05 +0000 (20:53 +0200)]
lemma-2: do not confuse lookup with lookupM

Even though they are the same.

Helmut Grohne [Fri, 27 Apr 2012 18:51:06 +0000 (20:51 +0200)]
use fromFunc to define union

Semantically this is no change, but reducing to standard interface seems
better.

Helmut Grohne [Fri, 27 Apr 2012 16:05:47 +0000 (18:05 +0200)]
prove the theorem-2

Helmut Grohne [Fri, 20 Apr 2012 10:15:33 +0000 (12:15 +0200)]
remove lemma-\in-lookupM-assoc

It is a special case of lemma-assoc-domain.

Helmut Grohne [Fri, 20 Apr 2012 09:55:52 +0000 (11:55 +0200)]
complete lemma-2 using new property _in-domain-of_

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.

Helmut Grohne [Thu, 19 Apr 2012 10:27:00 +0000 (12:27 +0200)]
reduce hole in 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.