Merge branch feature-delete
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 27 Jan 2014 12:46:47 +0000 (13:46 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 27 Jan 2014 12:46:47 +0000 (13:46 +0100)
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.

Conflicts:
Bidir.agda
FinMap.agda
Generic.agda
Precond.agda

1  2 
BFF.agda
Bidir.agda
FinMap.agda
Generic.agda
Precond.agda

diff --cc BFF.agda
+++ b/BFF.agda
@@@ -11,9 -11,10 +11,10 @@@ open Category.Functor.RawFunctor {Level
  open import Data.List using (List ; [] ; _∷_ ; map ; length)
  open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
  open import Function using (id ; _∘_ ; flip)
 -open import Relation.Binary.Core using (Decidable ; _≡_)
 +open import Relation.Binary using (DecSetoid ; module DecSetoid)
  
  open import FinMap
+ open import Generic using (mapMV)
  import CheckInsert
  import FreeTheorems
  
diff --cc Bidir.agda
@@@ -8,7 -7,7 +8,7 @@@ open import Data.Fin using (Fin
  import Level
  import Category.Monad
  import Category.Functor
- open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
 -open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
++open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
  open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
  open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
  open import Data.List using (List)
@@@ -25,27 -22,12 +25,27 @@@ import Relation.Binary.EqReasoning as E
  
  import FreeTheorems
  open FreeTheorems.VecVec using (get-type ; free-theorem)
- open import Generic using (just-injective ; map-just-injective ; vecIsSetoid)
 -open import Generic using (just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
++open import Generic using (just-injective ; vecIsSetoid ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
  open import FinMap
  import CheckInsert
 -open CheckInsert Carrier deq
 +open CheckInsert A
  import BFF
 -open BFF.VecBFF Carrier deq using (assoc ; enumerate ; denumerate ; bff)
 +open BFF.VecBFF A using (assoc ; enumerate ; denumerate ; bff)
 +open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
 +
 +module SetoidReasoning where
 + infix 1 begin⟨_⟩_
 + infixr 2 _≈⟨_⟩_ _≡⟨_⟩_
 + infix 2 _∎
 + begin⟨_⟩_ : (X : Setoid ℓ₀ ℓ₀) → {x y : Setoid.Carrier X} → EqR._IsRelatedTo_ X x y → Setoid._≈_ X x y
 + begin⟨_⟩_ X p = EqR.begin_ X p
 + _∎ : {X : Setoid ℓ₀ ℓ₀} → (x : Setoid.Carrier X) → EqR._IsRelatedTo_ X x x
 + _∎ {X} = EqR._∎ X
 + _≈⟨_⟩_ : {X : Setoid ℓ₀ ℓ₀} → (x : Setoid.Carrier X) → {y z : Setoid.Carrier X} → Setoid._≈_ X x y → EqR._IsRelatedTo_ X y z → EqR._IsRelatedTo_ X x z
 + _≈⟨_⟩_ {X} = EqR._≈⟨_⟩_ X
 +
 + _≡⟨_⟩_ : {X : Setoid ℓ₀ ℓ₀} → (x : Setoid.Carrier X) → {y z : Setoid.Carrier X} → x ≡ y → EqR._IsRelatedTo_ X y z → EqR._IsRelatedTo_ X x z
 + _≡⟨_⟩_ {X} = EqR._≡⟨_⟩_ X
  
  lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f (toList is))
  lemma-1 f []        = refl
@@@ -144,54 -126,84 +148,99 @@@ theorem-1 get s = begi
    just (map (denumerate s) (enumerate s))
      ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
    just s ∎
 -    where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
 +    where open ≡-Reasoning
-           h↦h′ = _<$>_ (flip union (fromFunc (denumerate s)))
-           h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupVec)
++          h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
+           h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec)
  
- lemma-<$>-just : {A B : Set} {f : A → B} {b : B} {ma : Maybe A} → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
- lemma-<$>-just {ma = just x}  f<$>ma≡just-b = x , refl
- lemma-<$>-just {ma = nothing} ()
  
- lemma-union-not-used : {m n : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMap n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map just (map (flip lookup (union h h')) is) ≡ map (flip lookupM h) is
+ lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
+ lemma-<$>-just (just x) f<$>ma≡just-b = x , refl
+ lemma-<$>-just nothing  ()
+ lemma-union-not-used : {m n : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMapMaybe n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map (flip lookupM (union h h')) is ≡ map (flip lookupM h) is
  lemma-union-not-used h h' []        p = refl
  lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin
-       just (lookup i (union h h'))
-         ≡⟨ cong just (lookup∘tabulate (λ j → maybe′ id (lookup j h') (lookupM j h)) i) ⟩
-       just (maybe′ id (lookup i h') (lookupM i h))
-         ≡⟨ cong just (cong (maybe′ id (lookup i h')) px) ⟩
-       just (maybe′ id (lookup i h') (just x))
+       lookupM i (union h h')
+         ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h') (lookupM j h)) i ⟩
+       maybe′ just (lookupM i h') (lookupM i h)
+         ≡⟨ cong (maybe′ just (lookupM i h')) px ⟩
+       maybe′ just (lookupM i h') (just x)
          ≡⟨ sym px ⟩
        lookupM i h ∎)
    (lemma-union-not-used h h' is' p')
 +  where open ≡-Reasoning
 +
 +map-just-≈-injective : {n : ℕ} {x y : Vec Carrier n} → Setoid._≈_ (vecIsSetoid (MaybeSetoid A.setoid) n) (map just x) (map just y) → Setoid._≈_ (vecIsSetoid A.setoid n) x y
 +map-just-≈-injective {x = []}    {y = []}    VecEq.[]-cong              = VecEq.[]-cong
 +map-just-≈-injective {x = _ ∷ _} {y = _ ∷ _} (just x≈y VecEq.∷-cong ps) = x≈y VecEq.∷-cong map-just-≈-injective ps
  
 -theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (v : Vec Carrier (getlen m)) → (s u : Vec Carrier m) → bff get s v ≡ just u → get u ≡ v
+ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a
+ lemma->>=-just (just a) p = a , refl
+ lemma->>=-just nothing  ()
+ lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
+ lemma-just-sequence [] = refl
+ lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl
+ lemma-mapM-successful : {A B : Set} {f : A → Maybe B} {n : ℕ} → (v : Vec A n) → {r : Vec B n} → mapMV f v ≡ just r → ∃ λ w → map f v ≡ map just w
+ lemma-mapM-successful         []      p = [] , refl
+ lemma-mapM-successful {f = f} (x ∷ xs) p with f x | mapMV f xs | inspect (mapMV f) xs
+ lemma-mapM-successful         (x ∷ xs) () | nothing | _ | _
+ lemma-mapM-successful         (x ∷ xs) () | just y | nothing | _
+ lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] with lemma-mapM-successful xs p′
+ lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] | w , pw = y ∷ w , cong (_∷_ (just y)) pw
+ lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {n : ℕ} {v : Vec A n} {r : Vec B n} → mapMV f v ≡ just r → {getlen : ℕ → ℕ} (get : get-type getlen) → get <$> mapMV f v ≡ mapMV f (get v)
+ lemma-get-mapMV {f = f} {v = v} p get = let w , pw = lemma-mapM-successful v p in begin
+   get <$> mapMV f v
+     ≡⟨ cong (_<$>_ get) (sym (sequence-map f v)) ⟩
+   get <$> (sequenceV (map f v))
+     ≡⟨ cong (_<$>_ get ∘ sequenceV) pw ⟩
+   get <$> (sequenceV (map just w))
+     ≡⟨ cong (_<$>_ get) (lemma-just-sequence w) ⟩
+   get <$> just w
+     ≡⟨ sym (lemma-just-sequence (get w)) ⟩
+   sequenceV (map just (get w))
+     ≡⟨ cong sequenceV (sym (free-theorem get just w)) ⟩
+   sequenceV (get (map just w))
+     ≡⟨ cong (sequenceV ∘ get) (sym pw) ⟩
+   sequenceV (get (map f v))
+     ≡⟨ cong sequenceV (free-theorem get f v) ⟩
+   sequenceV (map f (get v))
+     ≡⟨ sequence-map f (get v) ⟩
+   mapMV f (get v) ∎
++  where open ≡-Reasoning
++
++sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (vecIsSetoid (MaybeSetoid S) n)} → Setoid._≈_ (vecIsSetoid (MaybeSetoid S) n) m₁ m₂ → Setoid._≈_ (MaybeSetoid (vecIsSetoid S n)) (sequenceV m₁) (sequenceV m₂)
++sequence-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (vecIsSetoid S _))
++sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys
++sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | just sxs | just sys | just p = MaybeEq.just (x≈y VecEq.∷-cong p)
++sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (vecIsSetoid S _))
++sequence-cong {S}                                       (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (vecIsSetoid S _))
- theorem-2 get v s u p with lemma-<$>-just (proj₂ (lemma-<$>-just p))
- theorem-2 get v s u p | h , ph = begin⟨ vecIsSetoid A.setoid _ ⟩
-   get u
-     ≡⟨ just-injective (begin⟨ EqSetoid _ ⟩
-       get <$> (just u)
-         ≡⟨ cong (_<$>_ get) (sym p) ⟩
-       get <$> (bff get s v)
-         ≡⟨ cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
-       get <$> (h′↦r <$> (h↦h′ <$> just h)) ∎) ⟩
-   get (map (flip lookup (h↦h′ h)) s′)
-     ≡⟨ free-theorem get (flip lookup (h↦h′ h)) s′ ⟩
-   map (flip lookup (h↦h′ h)) (get s′)
-      ≈⟨ map-just-≈-injective (begin⟨ vecIsSetoid (MaybeSetoid A.setoid) _ ⟩
-        map just (map (flip lookup (union h g)) (get s′))
-          ≡⟨ lemma-union-not-used h g (get s′) (lemma-assoc-domain (get s′) v h ph) ⟩
-        map (flip lookupM h) (get s′)
-          ≈⟨ lemma-2 (get s′) v h ph ⟩
-        map just v
-          ∎) ⟩
-   v ∎
 +theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (v : Vec Carrier (getlen m)) → (s u : Vec Carrier m) → bff get s v ≡ just u → Setoid._≈_ (vecIsSetoid A.setoid (getlen m)) (get u) v
 -theorem-2 get v s u p | h′ , ph′ | h , ph = just-injective (begin
+ theorem-2 get v s u p with (lemma->>=-just ((flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (get (enumerate s)) v)) p)
+ theorem-2 get v s u p | h′ , ph′ with (lemma-<$>-just (assoc (get (enumerate s)) v) ph′)
 -    ≡⟨ cong sequenceV (lemma-2 (get s′) v h ph) ⟩
++theorem-2 get v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (vecIsSetoid A.setoid _) ⟩
+   get <$> (just u)
+     ≡⟨ cong (_<$>_ get) (sym p) ⟩
+   get <$> (bff get s v)
+     ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
+   get <$> mapMV (flip lookupM (h↦h′ h)) s′
+     ≡⟨ lemma-get-mapMV (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) get ⟩
+   mapMV (flip lookupM (h↦h′ h)) (get s′)
+     ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get s′)) ⟩
+   sequenceV (map (flip lookupM (h↦h′ h)) (get s′))
+     ≡⟨ cong sequenceV (lemma-union-not-used h g′ (get s′) (lemma-assoc-domain (get s′) v h ph)) ⟩
+   sequenceV (map (flip lookupM h) (get s′))
 -    where s′   = enumerate s
++    ≈⟨ sequence-cong (lemma-2 (get s′) v h ph) ⟩
+   sequenceV (map just v)
+     ≡⟨ lemma-just-sequence v ⟩
+   just v ∎)
 +    where open SetoidReasoning
 +          s′   = enumerate s
            g    = fromFunc (denumerate s)
-           h↦h′ = flip union g
-           h′↦r = flip map s′ ∘ flip lookupVec
+           g′   = delete-many (get s′) g
+           h↦h′ = flip union g′
+           h′↦r = flip mapMV s′ ∘ flip lookupM
diff --cc FinMap.agda
@@@ -1,13 -1,10 +1,13 @@@
  module FinMap where
  
 +open import Level using () renaming (zero to ℓ₀)
  open import Data.Nat using (ℕ ; zero ; suc)
 -open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
 +open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) renaming (setoid to MaybeEq)
  open import Data.Fin using (Fin ; zero ; suc)
  open import Data.Fin.Props using (_≟_)
- open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr) renaming (lookup to lookupVec ; map to mapV)
+ open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; toList) renaming (lookup to lookupVec ; map to mapV)
 +open import Data.Vec.Equality using ()
 +open Data.Vec.Equality.Equality using (_∷-cong_)
  open import Data.Vec.Properties using (lookup∘tabulate)
  open import Data.List using (List ; [] ; _∷_ ; map ; zip)
  open import Data.Product using (__ ; _,_)
diff --cc Generic.agda
@@@ -7,13 -7,10 +7,13 @@@ open import Data.Maybe using (Maybe ; j
  open import Data.Nat using (ℕ ; zero ; suc)
  open import Data.Product using (__ ; _,_)
  open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
- open import Function using (_∘_)
 +open import Data.Vec.Equality using () renaming (module Equality to VecEq)
 -import Level
+ open import Function using (_∘_ ; id)
 +open import Level using () renaming (zero to ℓ₀)
 +open import Relation.Binary using (Setoid ; module Setoid)
  open import Relation.Binary.Core using (_≡_ ; refl)
 -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans)
 +open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
 +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) renaming (setoid to PropEq)
  
  open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
  open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)