make things compile with 2.3.0.1
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 3 Feb 2014 15:36:11 +0000 (16:36 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Mon, 3 Feb 2014 15:36:11 +0000 (16:36 +0100)
 * Remove let patter , match = foo usage
 * Remove Qualified.infix-symbol usage
 * Add non-obvious absurd patterns
 * Qualify constructors

Bidir.agda
FinMap.agda
Generic.agda
Precond.agda

index e792b3a..e024aac 100644 (file)
@@ -101,11 +101,11 @@ lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs
 lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _
 lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
   lookupM i h ∷ map (flip lookupM h) is
-    ≈⟨ lemma-lookupM-assoc i is x xs h (trans (cong (flip _>>=_ (checkInsert i x)) ir) p) VecEq.∷-cong ISetoid.refl (VecISetoid (MaybeSetoid A.setoid)) ⟩
+    ≈⟨ VecEq._∷-cong_ (lemma-lookupM-assoc i is x xs h (trans (cong (flip _>>=_ (checkInsert i x)) ir) p)) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩
   just x ∷ map (flip lookupM h) is
     ≡⟨  cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h h' p is (lemma-assoc-domain is xs h' ir)) ⟩
   just x ∷ map (flip lookupM h') is
-    ≈⟨ Setoid.refl (MaybeSetoid A.setoid) VecEq.∷-cong (lemma-2 is xs h' ir) ⟩
+    ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩
   just x ∷ map just xs ∎
   where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
 
@@ -191,19 +191,19 @@ lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] | w ,
 
 
 lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {n : ℕ} {v : Vec A n} {r : Vec B n} → mapMV f v ≡ just r → (get : Get) → Get.get get <$> mapMV f v ≡ mapMV f (Get.get get v)
-lemma-get-mapMV {f = f} {v = v} p G = let w , pw = lemma-mapM-successful v p in begin
+lemma-get-mapMV {f = f} {v = v} p G = 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 just w)) ⟩
-  sequenceV (get (map just w))
-    ≡⟨ cong (sequenceV ∘ get) (sym pw) ⟩
+    ≡⟨ cong (_<$>_ get ∘ sequenceV) (proj₂ wp) ⟩
+  get <$> (sequenceV (map just (proj₁ wp)))
+    ≡⟨ cong (_<$>_ get) (lemma-just-sequence (proj₁ wp)) ⟩
+  get <$> just (proj₁ wp)
+    ≡⟨ sym (lemma-just-sequence (get (proj₁ wp))) ⟩
+  sequenceV (map just (get (proj₁ wp)))
+    ≡⟨ cong sequenceV (sym (free-theorem just (proj₁ wp))) ⟩
+  sequenceV (get (map just (proj₁ wp)))
+    ≡⟨ cong (sequenceV ∘ get) (sym (proj₂ wp)) ⟩
   sequenceV (get (map f v))
     ≡⟨ cong sequenceV (free-theorem f v) ⟩
   sequenceV (map f (get v))
@@ -211,13 +211,16 @@ lemma-get-mapMV {f = f} {v = v} p G = let w , pw = lemma-mapM-successful v p in
   mapMV f (get v) ∎
   where open ≡-Reasoning
         open Get G
+        wp = lemma-mapM-successful v p
 
 sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
 sequence-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _))
-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 (VecISetoid S at _))
-sequence-cong {S}                                       (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p)
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | ()
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | ()
+sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
+sequence-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
 theorem-2 : (G : Get) → {m : ℕ} → (v : Vec Carrier (Get.getlen G m)) → (s u : Vec Carrier m) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
 theorem-2 G v s u p with (lemma->>=-just ((flip union (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (Get.get G (enumerate s)) v)) p)
index ea4f49b..052ed6f 100644 (file)
@@ -94,7 +94,7 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g →
 lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
 lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))
 
-lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f)
+lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (Maybe.just ∘ f)
 lemma-fromFunc-tabulate {zero}  f = refl
 lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc))
 
@@ -113,8 +113,8 @@ lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (s
               ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩
             lookupM x (fromFunc f)
               ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩
-            lookupM x (tabulate (just ∘ f))
-              ≡⟨ lookup∘tabulate (just ∘ f) x ⟩
+            lookupM x (tabulate (Maybe.just ∘ f))
+              ≡⟨ lookup∘tabulate (Maybe.just ∘ f) x ⟩
             just (f x) ∎
           lemma-inner (t ∷ ts) x with x ≟ t
           lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))
index 81292ff..748a49a 100644 (file)
@@ -36,7 +36,7 @@ mapMV-cong {f = f} {g = g} f≗g (x ∷V xs) with f x | g x | f≗g x
 mapMV-cong f≗g (x ∷V xs) | just y | .(just y) | refl = cong (_<$>_ (_∷V_ y)) (mapMV-cong f≗g xs)
 mapMV-cong f≗g (x ∷V xs) | nothing | .nothing | refl = refl
 
-mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (just ∘ f) v ≡ just (map f v)
+mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v)
 mapMV-purity f []V = refl
 mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl
 
@@ -80,7 +80,7 @@ toList-subst v refl = refl
 VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀
 VecISetoid S = record
   { Carrier = Vec (Setoid.Carrier S)
-  ; _≈_ = λ x → S VecEq.≈ x
+  ; _≈_ = λ x → VecEq._≈_ S x
   ; isEquivalence = record
     { refl = VecEq.refl S _
     ; sym = VecEq.sym S
index 2be3f3a..afb77d8 100644 (file)
@@ -18,7 +18,7 @@ import Data.List.All
 open import Data.List.Any using (here ; there)
 open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
-open import Data.Product using (∃ ; _,_ ; proj₂)
+open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
@@ -29,7 +29,8 @@ open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; ins
 import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
-open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
+import Bidir
+open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
 import GetTypes
 open GetTypes.VecVec using (Get ; module Get)
 open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
@@ -54,7 +55,7 @@ lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin
   tabulate (λ f → just (maybe′ id (lookup f g) (lookup f h)))
     ≡⟨ tabulate-∘ just (λ f → maybe′ id (lookup f g) (lookup f h)) ⟩
   map just (tabulate (λ f → maybe′ id (lookup f g) (lookup f h))) ∎)
-lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Data.List.All.∷ ps) = _ , (begin
+lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin
   union h (delete i (delete-many is (map just g)))
     ≡⟨ lemma-tabulate-∘ inner ⟩
   union h (delete-many is (map just g))
@@ -71,24 +72,25 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Da
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i)
 
 assoc-enough : (G : Get) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (Get.getlen G m)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u
-assoc-enough G s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin
+assoc-enough G s v (h , p) = _ , (begin
   bff G s v
     ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩
   mapMV (flip lookupM (union h g′)) s′
     ≡⟨ sym (sequence-map (flip lookupM (union h g′)) s′) ⟩
   sequenceV (map (flip lookupM (union h g′)) s′)
-    ≡⟨ cong (sequenceV ∘ flip map s′ ∘ flip lookupM) pw ⟩
-  sequenceV (map (flip lookupM (map just w)) s′)
-    ≡⟨ cong sequenceV (map-cong (λ f → lemma-lookup-map-just f w) s′) ⟩
-  sequenceV (map (Maybe.just ∘ flip lookup w) s′)
-    ≡⟨ cong sequenceV (map-∘ just (flip lookup w) s′) ⟩
-  sequenceV (map Maybe.just (map (flip lookup w) s′))
-    ≡⟨ lemma-just-sequence (map (flip lookup w) s′) ⟩
-  just (map (flip lookup w) s′) ∎)
+    ≡⟨ cong (sequenceV ∘ flip map s′ ∘ flip lookupM) (proj₂ wp) ⟩
+  sequenceV (map (flip lookupM (map just (proj₁ wp))) s′)
+    ≡⟨ cong sequenceV (map-cong (λ f → lemma-lookup-map-just f (proj₁ wp)) s′) ⟩
+  sequenceV (map (Maybe.just ∘ flip lookup (proj₁ wp)) s′)
+    ≡⟨ cong sequenceV (map-∘ just (flip lookup (proj₁ wp)) s′) ⟩
+  sequenceV (map Maybe.just (map (flip lookup (proj₁ wp)) s′))
+    ≡⟨ lemma-just-sequence (map (flip lookup (proj₁ wp)) s′) ⟩
+  just (map (flip lookup (proj₁ wp)) s′) ∎)
   where open Get G
         s′ = enumerate s
         g  = fromFunc (denumerate s)
         g′ = delete-many (get s′) g
+        wp = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p)
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []