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

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

9 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

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

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

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

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

9 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