diff options
| -rw-r--r-- | Bidir.agda | 14 | ||||
| -rw-r--r-- | CheckInsert.agda | 12 | ||||
| -rw-r--r-- | FinMap.agda | 16 |
3 files changed, 8 insertions, 34 deletions
@@ -31,25 +31,13 @@ open CheckInsert (decSetoid deq) import BFF open BFF.VecBFF Carrier deq using (assoc ; enumerate ; denumerate ; bff) -maybeSetoid-to-≡ : {A : Set} {x y : Setoid.Carrier (MaybeSetoid (≡-setoid A))} → Setoid._≈_ (MaybeSetoid (≡-setoid A)) x y → x ≡ y -maybeSetoid-to-≡ (just refl) = refl -maybeSetoid-to-≡ nothing = refl - -vecMaybeSetoid-to-≡ : {A : Set} {n : ℕ} {x y : Setoid.Carrier (vecIsSetoid (MaybeSetoid (≡-setoid A)) n)} → Setoid._≈_ (vecIsSetoid (MaybeSetoid (≡-setoid A)) n) x y → x ≡ y -vecMaybeSetoid-to-≡ VecEq.[]-cong = refl -vecMaybeSetoid-to-≡ (p₁ VecEq.∷-cong p₂) = cong₂ _∷_ (maybeSetoid-to-≡ p₁) (vecMaybeSetoid-to-≡ p₂) - -maybeVecMaybeSetoid-to-≡ : {A : Set} {n : ℕ} {x y : Setoid.Carrier (MaybeSetoid (vecIsSetoid (MaybeSetoid (≡-setoid A)) n))} → Setoid._≈_ (MaybeSetoid (vecIsSetoid (MaybeSetoid (≡-setoid A)) n)) x y → x ≡ y -maybeVecMaybeSetoid-to-≡ (just p) rewrite vecMaybeSetoid-to-≡ p = refl -maybeVecMaybeSetoid-to-≡ nothing = refl - 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 lemma-1 f (i ∷ is′) = begin (assoc is′ (map f is′) >>= checkInsert i (f i)) ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩ checkInsert i (f i) (restrict f (toList is′)) - ≡⟨ maybeVecMaybeSetoid-to-≡ (lemma-checkInsert-restrict f i (toList is′)) ⟩ + ≡⟨ lemma-checkInsert-restrict f i (toList is′) ⟩ just (restrict f (toList (i ∷ is′))) ∎ lemma-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc (i ∷ is) (x ∷ xs) ≡ just h → lookupM i h ≡ just x diff --git a/CheckInsert.agda b/CheckInsert.agda index 9302fc7..47af215 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -58,16 +58,10 @@ lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x' lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl -lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → Setoid._≈_ (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) n)) (checkInsert i (f i) (restrict f is)) (just (restrict f (i ∷ is))) +lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷ is)) lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is) -lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = MaybeEq.just (lemma-insert-same _ i (f i) (begin - lookupM i (restrict f is) - ≡⟨ p ⟩ - just x - ≈⟨ MaybeEq.just (Setoid.sym A.setoid fi≈x) ⟩ - just (f i) ∎)) - where open EqR (MaybeSetoid A.setoid) -lemma-checkInsert-restrict f i is | ._ | new _ = Setoid.refl (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) _)) +lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (f i) (trans p (cong just (sym (lemma-lookupM-restrict i f is x p))))) +lemma-checkInsert-restrict f i is | ._ | new _ = refl lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (IsPreorder.reflexive (Setoid.isPreorder A.setoid) (lemma-lookupM-restrict i f is x p)) fi≉x lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h ≡ just x → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x diff --git a/FinMap.agda b/FinMap.agda index a85f119..1fc2d16 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -64,18 +64,10 @@ partialize = mapV just lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever lemma-just≢nothing refl () -module Private {S : Setoid ℓ₀ ℓ₀} where - private - open Setoid S - reflMaybe = Setoid.refl (MaybeEq S) - _≈Maybe_ = Setoid._≈_ (MaybeEq S) - - lemma-insert-same : {n : ℕ} → (m : FinMapMaybe n Carrier) → (f : Fin n) → (a : Carrier) → lookupM f m ≈Maybe just a → Setoid._≈_ (vecIsSetoid (MaybeEq S) n) m (insert f a m) - lemma-insert-same [] () a p - lemma-insert-same {suc n} (x ∷ xs) zero a p = p ∷-cong Setoid.refl (vecIsSetoid (MaybeEq S) n) - lemma-insert-same (x ∷ xs) (suc i) a p = reflMaybe ∷-cong lemma-insert-same xs i a p - -open Private public +lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → (a : A) → lookupM f m ≡ just a → m ≡ insert f a m +lemma-insert-same [] () a p +lemma-insert-same {suc n} (x ∷ xs) zero a p = cong (flip _∷_ xs) p +lemma-insert-same (x ∷ xs) (suc i) a p = cong (_∷_ x) (lemma-insert-same xs i a p) lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing lemma-lookupM-empty zero = refl |