Merge branch master into feature-shape-update

For building on the sieve example.

4 files changed, 17 insertions, 13 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 9765392..f0b7bc1 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -178,8 +178,8 @@ 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-just-sequence []       = refl
+lemma-just-sequence (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequence xs)
 
 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
diff --git a/Examples.agda b/Examples.agda
index 70628a5..5971460 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -1,6 +1,6 @@
 module Examples where
 
-open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_)
+open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
 
 import GetTypes
@@ -37,3 +37,10 @@ drop' n = assume-get (f n)
         f zero    xs       = xs
         f (suc n) []       = []
         f (suc n) (x ∷ xs) = f n xs
+
+sieve' : Get
+sieve' = assume-get f
+  where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
+        f []           = []
+        f (x ∷ [])     = x ∷ []
+        f (x ∷ _ ∷ xs) = x ∷ f xs
diff --git a/FinMap.agda b/FinMap.agda
index 34e2fc1..240bbe1 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -108,8 +108,7 @@ lemma-fromFunc-tabulate {zero}  f = refl
 lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc))
 
 lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
-lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p with p refl
-...                                                      | ()
+lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p = contradiction refl p
 lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = refl
 lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = refl
 lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc)
diff --git a/Generic.agda b/Generic.agda
index 748a49a..b29f47d 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -8,12 +8,12 @@ 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 Data.Vec.Equality using () renaming (module Equality to VecEq)
-open import Function using (_∘_ ; id)
+open import Function using (_∘_ ; id ; flip)
 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.Indexed using (_at_) renaming (Setoid to ISetoid)
-open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) renaming (setoid to PropEq)
+open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans ; cong₂) renaming (setoid to PropEq)
 
 open Setoid using () renaming (_≈_ to _∋_≈_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
@@ -31,14 +31,12 @@ mapMV f []V = just []V
 mapMV f (x ∷V xs) = (f x) >>= (λ y → (_∷V_ y) <$> (mapMV f xs))
 
 mapMV-cong : {A B : Set} {f g : A → Maybe B} → f ≗ g → {n : ℕ} → mapMV {n = n} f ≗ mapMV g
-mapMV-cong f≗g []V = refl
-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-cong f≗g []V       = refl
+mapMV-cong f≗g (x ∷V xs) = cong₂ _>>=_ (f≗g x) (cong (flip (_<$>_ ∘ _∷V_)) (mapMV-cong f≗g xs))
 
 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
+mapMV-purity f []V       = refl
+mapMV-purity f (x ∷V xs) = cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs)
 
 maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (PropEq A) ∋ a ≈ b
 maybeEq-from-≡ {a = just x}  {b = .(just x)} refl = just refl