~helmut/bidiragda.git
9 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

9 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

9 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

9 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

9 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

9 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

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

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

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

9 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

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

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

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

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

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

9 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

9 years agoremove lemma-\in-lookupM-assoc
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.

9 years agocomplete lemma-2 using new property _in-domain-of_
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.

9 years agoreduce hole in 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.

9 years agoFinMap: lemma-lookupM-restrict drop useless implicit
Helmut Grohne [Thu, 19 Apr 2012 09:58:40 +0000 (11:58 +0200)]
FinMap: lemma-lookupM-restrict drop useless implicit

9 years agomove lemma-just!=nothing to FinMap and use it there
Helmut Grohne [Thu, 19 Apr 2012 09:52:27 +0000 (11:52 +0200)]
move lemma-just!=nothing to FinMap and use it there

9 years agoinline bot-elim into lemma-just-nothing
Helmut Grohne [Tue, 17 Apr 2012 10:10:35 +0000 (12:10 +0200)]
inline bot-elim into lemma-just-nothing

Seems like the more common use case.

9 years agoabstract proofs over checkInsert
Helmut Grohne [Wed, 4 Apr 2012 12:08:46 +0000 (14:08 +0200)]
abstract proofs over checkInsert

All proofs about expressions containing checkInsert share a common
pattern. There are three cases:
 1) Inserting a key-value-pair that is already present in the map.
 2) Inserting a new key into the map.
 3) Failure to insert a conflicting key-value pair in the map.

The checkInsertProof record enables to write three different cases
reducing the usage of "with" (and thus line length) in
lemma-checkInsert-restrict and lemma-lookupM-assoc.

9 years agofix wrong function name in lemma-2
Helmut Grohne [Fri, 16 Mar 2012 10:41:44 +0000 (11:41 +0100)]
fix wrong function name in lemma-2

lookup and lookupM reference the same function, but serve different
purposes.

9 years agoremove useless braces
Helmut Grohne [Thu, 9 Feb 2012 15:14:57 +0000 (16:14 +0100)]
remove useless braces

9 years agoavoid a sym in lemma-union-restrict
Helmut Grohne [Thu, 9 Feb 2012 15:04:32 +0000 (16:04 +0100)]
avoid a sym in lemma-union-restrict

9 years agos/generate/restrict/g
Helmut Grohne [Thu, 9 Feb 2012 15:01:38 +0000 (16:01 +0100)]
s/generate/restrict/g

The name was deemed misleading. Nothing else changed.

9 years agorephrase free-theorem-list-list using pointwise equality
Helmut Grohne [Thu, 9 Feb 2012 14:56:29 +0000 (15:56 +0100)]
rephrase free-theorem-list-list using pointwise equality

9 years agoformulate theorem-2
Helmut Grohne [Thu, 9 Feb 2012 14:33:38 +0000 (15:33 +0100)]
formulate theorem-2

9 years agoprove lemma-union-generate
Helmut Grohne [Thu, 9 Feb 2012 14:08:36 +0000 (15:08 +0100)]
prove lemma-union-generate

9 years agoprove theorem-1 assuming a lemma-union-generate
Helmut Grohne [Thu, 9 Feb 2012 13:59:32 +0000 (14:59 +0100)]
prove theorem-1 assuming a lemma-union-generate

9 years agostarted proving theorem-1
Helmut Grohne [Thu, 9 Feb 2012 11:35:10 +0000 (12:35 +0100)]
started proving theorem-1

As in the bff paper expand s using lemma-map-denumerate-enumerate
and apply free-theorem-list-list to commute get and map.

9 years agointroduce denumerate
Helmut Grohne [Thu, 9 Feb 2012 10:58:54 +0000 (11:58 +0100)]
introduce denumerate

It is some kind of counter part to enumerate. That is:

map (denumerate s) (enumerate s) \== s

It can be employed in bff and I believe it to simplify reasoning on bff.

9 years agoreplace idrange with enumerate
Helmut Grohne [Tue, 31 Jan 2012 17:32:46 +0000 (18:32 +0100)]
replace idrange with enumerate

Looks like uses of idrange would always be passed a length, so move it
inside the definition.

9 years agopostulate free theorem for List a -> List a
Helmut Grohne [Tue, 31 Jan 2012 17:26:32 +0000 (18:26 +0100)]
postulate free theorem for List a -> List a

9 years agorecursion of lemma-2
Helmut Grohne [Thu, 26 Jan 2012 17:06:42 +0000 (18:06 +0100)]
recursion of lemma-2

9 years agostarted proving lemma-2
Helmut Grohne [Thu, 26 Jan 2012 16:12:44 +0000 (17:12 +0100)]
started proving lemma-2

The step case needs two lemmata. One for the head of the resulting map and one
for the tail. The head case is shown using a

lemma-lookupM-assoc : assoc eq (i :: _) (x :: _) == just h ->
  lookupM i h == just x

9 years agoreduce imports to speed up agda-mode
Helmut Grohne [Thu, 26 Jan 2012 15:05:23 +0000 (16:05 +0100)]
reduce imports to speed up agda-mode

9 years agosplit Bidir.agda to FinMap.agda
Helmut Grohne [Thu, 26 Jan 2012 14:51:15 +0000 (15:51 +0100)]
split Bidir.agda to FinMap.agda

9 years agoimprove readability using spaces
Helmut Grohne [Thu, 26 Jan 2012 14:24:41 +0000 (15:24 +0100)]
improve readability using spaces

9 years agoreduce usage of sym
Helmut Grohne [Thu, 26 Jan 2012 14:22:09 +0000 (15:22 +0100)]
reduce usage of sym

Try to always construct statements of the form
  complex expression \== simple expression.

9 years agoopen \==-Reasoning at top level
Helmut Grohne [Thu, 26 Jan 2012 14:07:04 +0000 (15:07 +0100)]
open \==-Reasoning at top level

9 years agoprove the remaining parts of lemma-checkInsert-generate
Helmut Grohne [Thu, 26 Jan 2012 13:51:21 +0000 (14:51 +0100)]
prove the remaining parts of lemma-checkInsert-generate

Introducing the following lemmata:
 * lemma-lookupM-empty : nothing \== lookupM i empty
 * lemma-from-just : just x \== just y -> x \== y
 * lemma-lookupM-insert : just a \== lookupM i (insert i a m)
 * lemma-lookupM-insert-other : \neg (i \== j) ->
   lookupM i m \== lookupM i (insert j a m)
 * lemma-lookupM-generate : just a = lookupM i (generate f is) -> a \== f i

9 years agocomplete the yes part of lemma-checkInsert-generate using inspect
Helmut Grohne [Thu, 26 Jan 2012 10:45:06 +0000 (11:45 +0100)]
complete the yes part of lemma-checkInsert-generate using inspect

9 years agochange lemma-insert-same to work with \== proofs
Helmut Grohne [Thu, 26 Jan 2012 10:37:44 +0000 (11:37 +0100)]
change lemma-insert-same to work with \== proofs

This way the inserted value is not hidden in the Is-Just proof object.

9 years agobase case of lemma-2
Helmut Grohne [Mon, 23 Jan 2012 18:51:55 +0000 (19:51 +0100)]
base case of lemma-2

9 years agorewrite lemma-1 using propositional equality
Helmut Grohne [Mon, 23 Jan 2012 10:50:28 +0000 (11:50 +0100)]
rewrite lemma-1 using propositional equality

10 years agoactually fmap is what I meant instead of >>=
Helmut Grohne [Sun, 22 Jan 2012 22:11:19 +0000 (23:11 +0100)]
actually fmap is what I meant instead of >>=

10 years agointroduce >>= on Maybe to improve readability
Helmut Grohne [Sun, 22 Jan 2012 21:59:17 +0000 (22:59 +0100)]
introduce >>= on Maybe to improve readability

10 years agoimprove readability by introducing EqInst
Helmut Grohne [Sun, 22 Jan 2012 21:47:39 +0000 (22:47 +0100)]
improve readability by introducing EqInst

10 years agoformulate theorem-1
Helmut Grohne [Sun, 22 Jan 2012 21:43:32 +0000 (22:43 +0100)]
formulate theorem-1

10 years agoformulate lemma-2
Helmut Grohne [Sun, 22 Jan 2012 21:36:16 +0000 (22:36 +0100)]
formulate lemma-2

10 years agoattempt to prove lemma-1
Helmut Grohne [Sun, 22 Jan 2012 15:40:58 +0000 (16:40 +0100)]
attempt to prove lemma-1

In order to prove lemma-1 we first show a lemma-insert-same to show that
inserting the same pair twice does not change the FinMapMaye. lemma-1 still
has two goals. In the first goal agda doesn't accept "is-just (f i)". Why?
The second goal is to be shown as absurd.

10 years agorewrite generate using zip and fromAscList
Helmut Grohne [Sat, 21 Jan 2012 11:22:34 +0000 (12:22 +0100)]
rewrite generate using zip and fromAscList

This way matches the usage in lemma-1 more closely since zip actually is
something similar to assoc.

10 years agosplit FinMap to FinMapMaybe
Helmut Grohne [Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100)]
split FinMap to FinMapMaybe

The FinMapMaybe is what FinMap previously was. The FinMap instead now really
maps its whole domain to something. This property is needed to avoid the
usage of fromJust in the definition of bff. With this split applied the
definition of bff is now complete.

10 years agoreplaced NatMap with FinMap
Helmut Grohne [Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100)]
replaced NatMap with FinMap

The domain of the map is always limited. So using Fin n as the domain is
natural. Additionally FinMaps are now semantically equal iff their normal form
is the same. That means \== can be used.

10 years agofirst attempt to define bff (with holes)
Helmut Grohne [Thu, 19 Jan 2012 11:11:01 +0000 (12:11 +0100)]
first attempt to define bff (with holes)

10 years agoemploy standard library of agda where possible
Helmut Grohne [Thu, 19 Jan 2012 10:47:16 +0000 (11:47 +0100)]
employ standard library of agda where possible

10 years agofirst attempt to model lemma-1
Helmut Grohne [Thu, 19 Jan 2012 10:33:17 +0000 (11:33 +0100)]
first attempt to model lemma-1

Without using the stdlib basic data structures are defined (with the
stdlib names in mind). The IntMap given in the paper is translated to a
NatMap. There are definitions for checkInsert and assoc resulting in a
formalization of lemma-1.

10 years agoadded .gitignore
Helmut Grohne [Thu, 19 Jan 2012 10:31:52 +0000 (11:31 +0100)]
added .gitignore