~helmut/bidiragda.git
10 years agoimprove readability using spaces
Helmut Grohne [Thu, 26 Jan 2012 14:24:41 +0000 (15:24 +0100)]
improve readability using spaces

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

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

10 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

10 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

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

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

10 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