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.

diff --git a/Bidir.agda b/Bidir.agda
new file mode 100644 (file)
index 0000000..e2706a0
--- /dev/null
+++ b/Bidir.agda
@@ -0,0 +1,108 @@
+module Bidir where
+
+data Bool : Set where
+  true : Bool
+  false : Bool
+
+not : Bool → Bool
+not true = false
+not false = true
+
+data â„• : Set where
+  zero : â„•
+  suc : ℕ → ℕ
+
+equal? : â„• -> â„• -> Bool
+equal? zero    zero    = true
+equal? (suc n) (suc m) = equal? n m
+equal? _       _       = false
+
+data Maybe (A : Set) : Set where
+  nothing : Maybe A
+  just : A → Maybe A
+
+maybeToBool : {A : Set} → Maybe A → Bool
+maybeToBool nothing  = false
+maybeToBool (just _) = true
+
+maybe′ : {A B : Set} → (A → Maybe B) → Maybe B → Maybe A → Maybe B
+maybe′ y _ (just a) = y a
+maybe′ _ n nothing  = n
+
+data _×_ (A B : Set) : Set where
+  _,_ : A → B → A × B
+
+data List (A : Set) : Set where
+  [] : List A
+  _∷_ : A → List A → List A
+
+_++_ : {A : Set} → List A → List A → List A
+_++_ []        ys = ys
+_++_ (x ∷ xs) ys = x ∷ (xs ++ ys)
+
+map : {A B : Set} → (A → B) → List A → List B
+map f []        = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+zip : {A B : Set} → List A → List B → List (A × B)
+zip (a ∷ as) (b ∷ bs) = (a , b) ∷ zip as bs
+zip _         _         = []
+
+data _==_ {A : Set}(x : A) : A → Set where
+  refl : x == x
+
+module NatMap where
+
+  NatMap : Set → Set
+  NatMap A = List (ℕ × A)
+
+  lookup : {A : Set} → ℕ → NatMap A → Maybe A
+  lookup n []       = nothing
+  lookup n ((m , a) ∷ xs) with equal? n m
+  lookup n ((m , a) ∷ xs) | true = just a
+  lookup n ((m , a) ∷ xs) | false        = lookup n xs
+
+  notMember : {A : Set} → ℕ → NatMap A → Bool
+  notMember n m = not (maybeToBool (lookup n m))
+
+  -- For now we simply prepend the element. This may lead to duplicates.
+  insert : {A : Set} → ℕ → A → NatMap A → NatMap A
+  insert n a m = (n , a) ∷ m
+
+  fromAscList : {A : Set} → List (ℕ × A) → NatMap A
+  fromAscList []       = []
+  fromAscList ((n , a) ∷ xs) = insert n a (fromAscList xs)
+
+  empty : {A : Set} → NatMap A
+  empty = []
+
+  union : {A : Set} → NatMap A → NatMap A → NatMap A
+  union []       m = m
+  union ((n , a) ∷ xs) m = insert n a (union xs m)
+
+open NatMap
+
+checkInsert : {A : Set} → (A → A → Bool) → ℕ → A → NatMap A → Maybe (NatMap A)
+checkInsert eq i b m with lookup i m
+checkInsert eq i b m | just c with eq b c
+checkInsert eq i b m | just c | true = just m
+checkInsert eq i b m | just c | false = nothing
+checkInsert eq i b m | nothing = just (insert i b m)
+
+assoc : {A : Set} → (A → A → Bool) → List ℕ → List A → Maybe (NatMap A)
+assoc _  []       []       = just empty
+assoc eq (i ∷ is) (b ∷ bs) = maybe′ (checkInsert eq i b) nothing (assoc eq is bs)
+assoc _  _        _        = nothing
+
+--data Equal? where
+--  same ...
+--  different ...
+
+generate : {A : Set} → (ℕ → A) → List ℕ → NatMap A
+generate f []       = empty
+generate f (n ∷ ns) = insert n (f n) (generate f ns)
+
+-- this lemma is probably wrong, because two different NatMaps may represent the same semantic value.
+lemma-1 : {τ : Set} → (eq : τ → τ → Bool) → (f : ℕ → τ) → (is : List ℕ) → assoc eq is (map f is) == just (generate f is)
+lemma-1 eq f []        = refl
+lemma-1 eq f (i ∷ is′) = {!!}