8 years agodrop the injection requirement for gl₁
Helmut Grohne [Tue, 14 Oct 2014 07:52:00 +0000 (09:52 +0200)]
drop the injection requirement for gl₁

Turns out, we never use this requirement. The only place where it may
come in relevant is the free theorems. But here non-injectivity turns
out to be reasoning about multiple get functions that are selected by
the additional index each individually satisfying the free theorem and
thus commonly satisfying it as well.

8 years agoresolve ambiguity in BFFPlug
Helmut Grohne [Fri, 26 Sep 2014 11:02:25 +0000 (13:02 +0200)]
resolve ambiguity in BFFPlug

Fixes compilation with Agda 2.4.2.

8 years agodrop-suc is cong pred
Helmut Grohne [Fri, 6 Jun 2014 07:23:00 +0000 (09:23 +0200)]
drop-suc is cong pred

8 years agofix compilation for Agda again
Helmut Grohne [Thu, 3 Apr 2014 13:33:06 +0000 (15:33 +0200)]
fix compilation for Agda again

It fails to infer the type of MaybeFunctor._<$>_, so give it explicitly.

8 years agoMerge branch feature-shaped into master
Helmut Grohne [Thu, 3 Apr 2014 06:57:34 +0000 (08:57 +0200)]
Merge branch feature-shaped into master

Generalizing both Vecs in the type of get to instances of Shaped. Thus allowing
trees and other data structures to be used.

8 years agodrop PartialShapeVec
Helmut Grohne [Thu, 3 Apr 2014 06:45:19 +0000 (08:45 +0200)]
drop PartialShapeVec

One can use PartialShapeShape instead, so there is limited utility for
this type. It is not used directly and there also is no PartialVecShape.

8 years agoalso allow Shaped types for the view
Helmut Grohne [Mon, 10 Mar 2014 15:11:15 +0000 (16:11 +0100)]
also allow Shaped types for the view

Albeit long, this commit is relatively boring.

8 years agogeneralize lemma-{just-sequence,sequence-successful}
Helmut Grohne [Mon, 10 Mar 2014 15:00:57 +0000 (16:00 +0100)]
generalize lemma-{just-sequence,sequence-successful}

8 years agoExample: show that PairVec is Shaped
Helmut Grohne [Mon, 10 Mar 2014 12:32:11 +0000 (13:32 +0100)]
Example: show that PairVec is Shaped

Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s)
is not Shaped in this way since its real index is only a number.

8 years agoport precondition to PartialShapeVec
Helmut Grohne [Mon, 10 Mar 2014 08:39:16 +0000 (09:39 +0100)]
port precondition to PartialShapeVec

8 years agoport theorem-{1,2} to PartialShapeVec
Helmut Grohne [Mon, 10 Mar 2014 08:31:57 +0000 (09:31 +0100)]
port theorem-{1,2} to PartialShapeVec

8 years agoimplement a bff on a shaped source type
Helmut Grohne [Mon, 10 Mar 2014 07:17:41 +0000 (08:17 +0100)]
implement a bff on a shaped source type

Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.

8 years agoadd a Functor structure
Helmut Grohne [Fri, 7 Mar 2014 14:18:24 +0000 (15:18 +0100)]
add a Functor structure

The intent is to replace some uses of Vec with a structure that also
happens to be a functor. RawFunctors from the standard library provide
no laws though, so we define a Functor structure that adds the laws. As
an additional law congruence is added, because

 * Other standard library structures in Algebra.Structures also require
 * Otherwise the identity law would have to reason about different

8 years agoimprove notation of theorem-1 using local bindings
Helmut Grohne [Fri, 7 Mar 2014 09:10:20 +0000 (10:10 +0100)]
improve notation of theorem-1 using local bindings

8 years agouse allFin rather than tabulate id
Helmut Grohne [Fri, 7 Mar 2014 08:16:45 +0000 (09:16 +0100)]
use allFin rather than tabulate id

8 years agoMerge branch feature-omit-sequence into master
Helmut Grohne [Wed, 5 Mar 2014 07:46:28 +0000 (08:46 +0100)]
Merge branch feature-omit-sequence into master

Beyond allowing default values during shape updates, this branch simplifies
working with shapes other than Vec.

8 years agomake lemma-sequenceV-successful more precise
Helmut Grohne [Tue, 4 Mar 2014 17:58:25 +0000 (18:58 +0100)]
make lemma-sequenceV-successful more precise

8 years agoweaken assumptions made by theorem-2 and asssoc-enough
Helmut Grohne [Wed, 26 Feb 2014 12:57:23 +0000 (13:57 +0100)]
weaken assumptions made by theorem-2 and asssoc-enough

8 years agoremove the sequenceV call from bff
Helmut Grohne [Wed, 26 Feb 2014 11:49:45 +0000 (12:49 +0100)]
remove the sequenceV call from bff

This allows bff to be more precise with regard to its failure modes,
even though we are not yet making use of that projected precision. It
allows inserting a default value for entries that could not be recovered
in a shape changing update as described in VoigtlaenderHMW13.

8 years agofix compilation on Agda
Helmut Grohne [Wed, 26 Feb 2014 09:12:50 +0000 (10:12 +0100)]
fix compilation on Agda

8 years agoconvert LiftGet module to using heterogeneous equality
Helmut Grohne [Wed, 26 Feb 2014 08:16:19 +0000 (09:16 +0100)]
convert LiftGet module to using heterogeneous equality

The reduction in proof length is impressive.

8 years agoadd intersperse as another example
Helmut Grohne [Mon, 24 Feb 2014 15:44:17 +0000 (16:44 +0100)]
add intersperse as another example

8 years agotheorem-2 works with EqR rather than SetoidReasoning again
Helmut Grohne [Mon, 24 Feb 2014 13:58:01 +0000 (14:58 +0100)]
theorem-2 works with EqR rather than SetoidReasoning again

8 years agodefine fromFunc more conveniently
Helmut Grohne [Mon, 24 Feb 2014 13:52:33 +0000 (14:52 +0100)]
define fromFunc more conveniently

8 years agogeneralize/weaken lemma-get-mapMV
Helmut Grohne [Mon, 24 Feb 2014 10:37:42 +0000 (11:37 +0100)]
generalize/weaken lemma-get-mapMV

It is now lemma-get-sequenceV and thus no longer applies the free
theorem for the function. Apart making the proof shorter, it also makes
the main use of the free theorem more visible in theorem-2.

8 years agodefine mapMV via sequenceV
Helmut Grohne [Mon, 24 Feb 2014 10:28:31 +0000 (11:28 +0100)]
define mapMV via sequenceV

This makes a few proofs easier and eliminates the need for sequence-map

8 years agogeneralize lemma-lookupM-assoc
Helmut Grohne [Mon, 24 Feb 2014 09:38:28 +0000 (10:38 +0100)]
generalize lemma-lookupM-assoc

8 years agominor simplifications
Helmut Grohne [Fri, 21 Feb 2014 10:04:44 +0000 (11:04 +0100)]
minor simplifications

8 years agouse map-Σ to simplify lemma-mapM-successful
Helmut Grohne [Fri, 21 Feb 2014 10:04:23 +0000 (11:04 +0100)]
use map-Σ to simplify lemma-mapM-successful

8 years agofix compilation on Agda
Helmut Grohne [Mon, 17 Feb 2014 12:32:12 +0000 (13:32 +0100)]
fix compilation on Agda

8 years agouse drop, tail and take from Data.Vec in examples
Helmut Grohne [Mon, 17 Feb 2014 10:32:35 +0000 (11:32 +0100)]
use drop, tail and take from Data.Vec in examples

This is possible using the PartialVecVec implementation.

8 years agoswitch examples to PartialVecVec
Helmut Grohne [Mon, 17 Feb 2014 10:26:02 +0000 (11:26 +0100)]
switch examples to PartialVecVec

8 years agoMerge branch feature-partial-getlen into master
Helmut Grohne [Mon, 17 Feb 2014 10:04:51 +0000 (11:04 +0100)]
Merge branch feature-partial-getlen into master

It allows defining get functions that are only defined for some vector
lengths. It retains backwards compatibility with the previous state via
a VecVec compatibility module. The biggest benefit is that now standard
library functions such as tail, take and drop can be passed to bff.

Conflicts: heavy
BFF.agda (imports, bff type clash)
Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and
Generic.agda (imports)
Precond.agda (imports, bff type clash in assoc-enough)

8 years agoavoid useless repetition
Helmut Grohne [Mon, 17 Feb 2014 09:30:43 +0000 (10:30 +0100)]
avoid useless repetition

8 years agoMerge branch feature-shape-update into master
Helmut Grohne [Fri, 14 Feb 2014 15:35:25 +0000 (16:35 +0100)]
Merge branch feature-shape-update into master

The branch enables shape updates in variety of flavours:
 * explicitly passing the desired target shape
 * providing a plugin sput : ℕ → ℕ → Maybe ℕ
 * providing a right-inverse to getlen
It also provides a backwards compatibility function to facilitate
shape-retaining updates.

8 years agoadd back original bff function before shape updates
Helmut Grohne [Fri, 14 Feb 2014 15:32:20 +0000 (16:32 +0100)]
add back original bff function before shape updates

8 years agoadd bffplug and bffinv functions and examples
Helmut Grohne [Mon, 10 Feb 2014 15:27:41 +0000 (16:27 +0100)]
add bffplug and bffinv functions and examples

We can now exploit getlen being rightinvertible and it works for drop
and sieve.

8 years agoMerge branch master into feature-shape-update
Helmut Grohne [Mon, 10 Feb 2014 14:50:27 +0000 (15:50 +0100)]
Merge branch master into feature-shape-update

For building on the sieve example.

8 years agoadd sieve to examples
Helmut Grohne [Mon, 10 Feb 2014 14:49:35 +0000 (15:49 +0100)]
add sieve to examples

8 years agoeliminate useless withs
Helmut Grohne [Fri, 7 Feb 2014 17:55:23 +0000 (18:55 +0100)]
eliminate useless withs

8 years agoreplace rewrite with cong where feasible
Helmut Grohne [Fri, 7 Feb 2014 17:32:54 +0000 (18:32 +0100)]
replace rewrite with cong where feasible

8 years agoallow shape shape updates in bff
Helmut Grohne [Fri, 7 Feb 2014 15:15:03 +0000 (16:15 +0100)]
allow shape shape updates in bff

Unlike the original version in VoigtlaenderHMW13, we do not request an
  sput : ℕ → ℕ → Maybe ℕ
function for determining the updated source shape from the original
source and updated view shape. Instead we ask the caller directly to
provide the result of sput together with a proof that its getlen matches
with the provided, updated view.

The precondition assoc-enough is not enriched in this way and still
requires a non-changing shape. I.e. it says what it said before.

8 years agobe more precise about which lookups we use
Helmut Grohne [Wed, 5 Feb 2014 14:59:06 +0000 (15:59 +0100)]
be more precise about which lookups we use

8 years agostrip even more implementation detail in Precond
Helmut Grohne [Wed, 5 Feb 2014 14:54:54 +0000 (15:54 +0100)]
strip even more implementation detail in Precond

8 years agostrip implementation detail from lemma-union-delete-fromFunc
Helmut Grohne [Wed, 5 Feb 2014 14:47:05 +0000 (15:47 +0100)]
strip implementation detail from lemma-union-delete-fromFunc

8 years agoadd lemma-lookupM-fromFunc
Helmut Grohne [Wed, 5 Feb 2014 14:21:57 +0000 (15:21 +0100)]
add lemma-lookupM-fromFunc

The new lemma replaces two uses of lemma-fromFunc-tabulate, because the
latter exposes the implementation of FinMapMaybe, whereas the former
argues about the behaviour of FinMapMaybe. The aim of not exposing the
implementation (apart from brevity) is to enable refactoring.

8 years agoadd examples
Helmut Grohne [Wed, 5 Feb 2014 10:05:29 +0000 (11:05 +0100)]
add examples

8 years agoremove unused imports
Helmut Grohne [Tue, 4 Feb 2014 10:12:42 +0000 (11:12 +0100)]
remove unused imports

Most of the became unused by using the convenience functions introduced
in the parent commit.

8 years agoadd convenience members to PartialVecVec.Get
Helmut Grohne [Tue, 4 Feb 2014 09:52:49 +0000 (10:52 +0100)]
add convenience members to PartialVecVec.Get

8 years agoMerge branch feature-get-record into feature-partial-getlen
Helmut Grohne [Tue, 4 Feb 2014 09:32:34 +0000 (10:32 +0100)]
Merge branch feature-get-record into feature-partial-getlen

These two features heavily interconnect. As such it makes sense to
integrate them properly. This non-trivial merge does that work. Compared
to feature-partial-getlen a few definitions moved from FreeTheorems.agda
to GetTypes.agda. Many types changed compared to both branches.

        conflict in GetTypes.agda not detected by merge

8 years agomake things compile with
Helmut Grohne [Mon, 3 Feb 2014 15:36:11 +0000 (16:36 +0100)]
make things compile with

 * Remove let patter , match = foo usage
 * Remove Qualified.infix-symbol usage
 * Add non-obvious absurd patterns
 * Qualify constructors

8 years agoMerge branch feature-get-record into master
Helmut Grohne [Mon, 3 Feb 2014 13:51:06 +0000 (14:51 +0100)]
Merge branch feature-get-record into master

This branch brings three main benefits:
 * Only one explicit parameter is needed to ask for a get function.
 * The postulated free theorems are mostly turned into preconditions,
   i.e. the only use of the postulates is in LiftGet.
 * We can now convert list based get functions to vec based ones and back
   including the (now) accompanying free theorem.

8 years agoalso show the other direction GetL-to-GetV
Helmut Grohne [Mon, 3 Feb 2014 13:41:19 +0000 (14:41 +0100)]
also show the other direction GetL-to-GetV

8 years agoadd a GetV-to-GetL transformer
Helmut Grohne [Mon, 3 Feb 2014 10:41:14 +0000 (11:41 +0100)]
add a GetV-to-GetL transformer

This is an improved version of getVec-to-getList in that it also
transports the corresponding free theorem.

8 years agofully allow partial get functions
Helmut Grohne [Thu, 30 Jan 2014 13:23:10 +0000 (14:23 +0100)]
fully allow partial get functions

By choosing gl₁ = suc and gl₂ = id, the tail function can now be

8 years agomake the getlen functions explicit in PartialVecBFF
Helmut Grohne [Thu, 30 Jan 2014 13:04:29 +0000 (14:04 +0100)]
make the getlen functions explicit in PartialVecBFF

There is no way for Agda to infer these functions or even the intended
index Setoid, so making these explicit is rather required.

8 years agoexpress VecBFF via PartialVecBFF
Helmut Grohne [Thu, 30 Jan 2014 13:01:10 +0000 (14:01 +0100)]
express VecBFF via PartialVecBFF

8 years agoallow importing of Bidir without any postulates
Helmut Grohne [Thu, 30 Jan 2014 08:13:11 +0000 (09:13 +0100)]
allow importing of Bidir without any postulates

8 years agopass get functions as records
Helmut Grohne [Thu, 30 Jan 2014 08:02:06 +0000 (09:02 +0100)]
pass get functions as records

This allows passing both getlen and get as a single parameter. It also
allows to make the free theorem a prerequisite instead of a postulate.

8 years agosimplify compilation of the whole source
Helmut Grohne [Thu, 30 Jan 2014 07:07:29 +0000 (08:07 +0100)]
simplify compilation of the whole source

8 years agodefine bff on a partial getlen
Helmut Grohne [Tue, 28 Jan 2014 14:15:12 +0000 (15:15 +0100)]
define bff on a partial getlen

The representation chosen is to give both an injection gl₁ and a
function gl₂ (formerly getlen), such that by choosing a non-identity for
gl₁ partiality of getlen can be expressed. An alternative would have
been to allow getlen to return a Maybe ℕ and have get return
  maybe (Vec A) ⊤ (getlen n)
thus sending all inputs for which getlen yields nothing to tt. It seems
that while there is no way to obtain a such a getlen predicate from an
arbitrary index Setoid I, it should be possible to manufacture a Setoid
from a predicate. Thanks to Stefan Mehner for the insightful discussion.

8 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._≈_

8 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

8 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

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

8 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.


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

8 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

8 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.

8 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

8 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.

8 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.

8 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.

8 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.

8 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

8 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.

8 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.

8 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

8 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

8 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.

8 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.

9 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 supported the old notation, but needs full

9 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.

9 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.

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

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

9 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.

9 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.

9 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

9 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

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

9 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.

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

9 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

9 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.

9 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.

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

9 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.

9 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.

9 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

9 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.