~helmut/bidiragda.git
7 years agoimprove readability using _∋_≈_ instead of Setoid._≈_
Helmut Grohne [Tue, 28 Jan 2014 09:53:45 +0000 (10:53 +0100)]
improve readability using _∋_≈_ instead of Setoid._≈_

7 years agothere is no need to work with IsPreorder
Helmut Grohne [Tue, 28 Jan 2014 08:36:54 +0000 (09:36 +0100)]
there is no need to work with IsPreorder

7 years agouse the indexed version of the Vec Setoid
Helmut Grohne [Tue, 28 Jan 2014 08:30:45 +0000 (09:30 +0100)]
use the indexed version of the Vec Setoid

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

7 years agoMerge branch feature-delete
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

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

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

7 years agoprove assoc-enough in the presence of delete
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.

7 years agoprove theorem-2 in the presence of delete
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.

7 years agogeneralize BFF and theorem-2 to arbitrary Setoids
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.

7 years agoshow a stronger lemma-checkInsert-restrict
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.

7 years agogeneralize checkInsert to arbitrary Setoids
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.

7 years agoshow that Vec is an indexed Setoid
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.

7 years agogeneralize lemma-insert-same to arbitrary Setoids
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

7 years agorefactor to get rid of FinMap without Maybe entirely
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.

7 years agoupdate bff implementation to use delete
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.

7 years agoadd a mapM variant on the Maybe monad on Vecs
Helmut Grohne [Mon, 16 Dec 2013 17:10:17 +0000 (18:10 +0100)]
add a mapM variant on the Maybe monad on Vecs

7 years agomove generic functions to a new Generic module
Helmut Grohne [Mon, 16 Dec 2013 16:34:59 +0000 (17:34 +0100)]
move generic functions to a new Generic module

7 years agoadd new functions delete, delete-many and partialize
Helmut Grohne [Mon, 16 Dec 2013 15:02:21 +0000 (16:02 +0100)]
add new functions delete, delete-many and partialize

and accompanying lemmata.

7 years agoget rid of the ListBFF implementation
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.

8 years agoneed to fully qualify Data.List.All._::_
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.

8 years agoimport _>>=_ and fmap from Data.Maybe
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.

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

This removes imports.

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

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

8 years agolemma-map-lookupM-assoc is even simpler
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.

8 years agorewrite lemma-map-lookupM-assoc
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.

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

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

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

8 years agoMerge branch view2 into master
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)

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

8 years agodefine a more useful version of lemma-just\==nnothing
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
both results instead.

8 years agointroduce a proper view on checkInsert
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.

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

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

Suggested by Joachim Breitner.

8 years agoMerge branch 'newlemma'
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.

8 years agoreduce a precondition of lemma-checkInsert-lookupM
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.

8 years agorewrite lemma-\notin-lookupM-assoc
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.

8 years agoadd new lemma-checkInsert-lookupM
Helmut Grohne [Wed, 9 Jan 2013 22:26:46 +0000 (23:26 +0100)]
add new lemma-checkInsert-lookupM

Suggested by Joachim Breitner.

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

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

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

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

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

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

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

8 years agoget rid of contraposition
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.

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

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

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

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

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

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

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

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

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

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

8 years agostrip prose from lemma-1 and lemma-2
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.

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

Less characters => more readable.

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

8 years agorename lemma-from-just to 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!

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

8 years agofinally parameterize CheckInsert
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
misleading name "EqInst" (hiding the decidability) got discarded.

8 years agonow parameterize BFF
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.

8 years agoalso parameterize Precond
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.

8 years agoparameterize Bidir via Carrier and deq
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.

9 years agomove all postulates to one module
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.

9 years agoremove VecRevBFF
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.

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

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

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

Consistent. Shorter.

9 years agorename suc-\== to suc-injective
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.

9 years agoimport [_] instead of Reveal_is_
Helmut Grohne [Wed, 26 Sep 2012 13:35:32 +0000 (15:35 +0200)]
import [_] instead of Reveal_is_

This makes things a little shorter and more readable.

9 years agoMerge branch 'using-vec'
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.

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

9 years agosave a with in lemma-\inn-lookupM-assoc
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.

9 years agoemploy rewrite in lemma-map-lookupM-assoc
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.

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

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

9 years agocomplete missing parts of LiftGet
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.

9 years agoshow fromList-toList in the subst form
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.

9 years agoLiftGet: replace vec-length-same with toList-subst
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.

9 years agoLiftGet: vec-length is also known as subst (Vec A)
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.

9 years agogive a sufficient precondition for theorem-2
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.

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

9 years agoformulate List <-> Vec isomorphism problems
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.

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

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

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

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

9 years agoattempt isomorphism between get on List and on Vec
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.

9 years agothird definition of bff
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

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

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

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

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

9 years agolemma-2: do not confuse lookup with lookupM
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.

9 years agouse fromFunc to define union
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.

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