diff options
| -rw-r--r-- | BFF.agda | 3 | ||||
| -rw-r--r-- | Bidir.agda | 28 | ||||
| -rw-r--r-- | CheckInsert.agda | 67 | ||||
| -rw-r--r-- | Precond.agda | 4 |
4 files changed, 62 insertions, 40 deletions
@@ -12,6 +12,7 @@ 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.PropositionalEquality using (decSetoid) open import FinMap import CheckInsert @@ -19,7 +20,7 @@ import FreeTheorems module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where open FreeTheorems.VecVec public using (get-type) - open CheckInsert Carrier deq + open CheckInsert (decSetoid deq) assoc : {n m : ℕ} → Vec (Fin n) m → Vec Carrier m → Maybe (FinMapMaybe n Carrier) assoc []V []V = just empty @@ -7,42 +7,56 @@ open import Data.Fin using (Fin) import Level import Category.Monad import Category.Functor -open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) +open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) renaming (setoid to MaybeSetoid) 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) open import Data.List.All using (All) open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; tabulate) renaming (lookup to lookupVec) +open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) open import Relation.Binary.Core using (refl) -open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂) +open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid) renaming (setoid to ≡-setoid) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) +open import Relation.Binary using (module Setoid) import FreeTheorems open FreeTheorems.VecVec using (get-type ; free-theorem) -open import Generic using (just-injective ; map-just-injective) +open import Generic using (just-injective ; map-just-injective ; vecIsSetoid) open import FinMap import CheckInsert -open CheckInsert Carrier deq +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′)) - ≡⟨ lemma-checkInsert-restrict f i (toList is′) ⟩ + ≡⟨ maybeVecMaybeSetoid-to-≡ (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 lemma-lookupM-assoc i is x xs h p with assoc is xs lemma-lookupM-assoc i is x xs h () | nothing lemma-lookupM-assoc i is x xs h p | just h' with checkInsert i x h' | insertionresult i x h' -lemma-lookupM-assoc i is x xs .h refl | just h | ._ | same pl = pl +lemma-lookupM-assoc i is x xs .h refl | just h | ._ | same x' x≡x' pl = trans pl (cong just (sym x≡x')) lemma-lookupM-assoc i is x xs ._ refl | just h' | ._ | new _ = lemma-lookupM-insert i x h' lemma-lookupM-assoc i is x xs h () | just h' | ._ | wrong _ _ _ @@ -54,7 +68,7 @@ lemma-assoc-domain [] [] h ph = Data.List.All.[] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph with assoc is' xs' | inspect (assoc is') xs' lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h () | nothing | [ ph' ] lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h' -lemma-assoc-domain (i' ∷ is') (x' ∷ xs') .h refl | just h | [ ph' ] | ._ | _ | same pl = All._∷_ (x' , pl) (lemma-assoc-domain is' xs' h ph') +lemma-assoc-domain (i' ∷ is') (x' ∷ xs') .h refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' h ph') lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ._ refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_ (x' , lemma-lookupM-insert i' x' h') (Data.List.All.map diff --git a/CheckInsert.agda b/CheckInsert.agda index d82c40b..9302fc7 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -1,73 +1,78 @@ -open import Relation.Binary.Core using (Decidable ; _≡_) +open import Level using () renaming (zero to ℓ₀) +open import Relation.Binary using (DecSetoid) -module CheckInsert (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where +module CheckInsert (A : DecSetoid ℓ₀ ℓ₀) where open import Data.Nat using (ℕ) open import Data.Fin using (Fin) open import Data.Fin.Props using (_≟_) -open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeEq) +open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq) open import Data.List using (List ; [] ; _∷_) open import Data.Vec using () renaming (_∷_ to _∷V_) open import Data.Vec.Equality using () renaming (module Equality to VecEq) -open import Relation.Nullary using (Dec ; yes ; no) +open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary using (Setoid) -open import Relation.Binary.Core using (refl ; _≢_) -open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans) renaming (setoid to PropEq) -open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) +open import Relation.Binary using (Setoid ; IsPreorder ; module DecSetoid) +open import Relation.Binary.Core using (refl ; _≡_ ; _≢_) +import Relation.Binary.EqReasoning as EqR +open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans) open import FinMap -open import Generic using (maybeEq-from-≡ ; vecIsSetoid) +open import Generic using (vecIsSetoid) + +private + open module A = DecSetoid A using (Carrier ; _≈_) renaming (_≟_ to deq) checkInsert : {n : ℕ} → Fin n → Carrier → FinMapMaybe n Carrier → Maybe (FinMapMaybe n Carrier) checkInsert i b m with lookupM i m ... | nothing = just (insert i b m) ... | just c with deq b c -... | yes b≡c = just m -... | no b≢c = nothing +... | yes b≈c = just m +... | no b≉c = nothing data InsertionResult {n : ℕ} (i : Fin n) (x : Carrier) (h : FinMapMaybe n Carrier) : Maybe (FinMapMaybe n Carrier) → Set where - same : lookupM i h ≡ just x → InsertionResult i x h (just h) + same : (x' : Carrier) → x ≈ x' → lookupM i h ≡ just x' → InsertionResult i x h (just h) new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h)) - wrong : (x' : Carrier) → x ≢ x' → lookupM i h ≡ just x' → InsertionResult i x h nothing + wrong : (x' : Carrier) → ¬ (x ≈ x') → lookupM i h ≡ just x' → InsertionResult i x h nothing insertionresult : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → InsertionResult i x h (checkInsert i x h) insertionresult i x h with lookupM i h | inspect (lookupM i) h insertionresult i x h | just x' | _ with deq x x' -insertionresult i x h | just .x | [ il ] | yes refl = same il -insertionresult i x h | just x' | [ il ] | no x≢x' = wrong x' x≢x' il +insertionresult i x h | just x' | [ il ] | yes x≈x' = same x' x≈x' il +insertionresult i x h | just x' | [ il ] | no x≉x' = wrong x' x≉x' il insertionresult i x h | nothing | [ il ] = new il lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m lemma-checkInsert-same i x m p with lookupM i m lemma-checkInsert-same i x m refl | .(just x) with deq x x -lemma-checkInsert-same i x m refl | .(just x) | yes refl = refl -lemma-checkInsert-same i x m refl | .(just x) | no x≢x = contradiction refl x≢x +lemma-checkInsert-same i x m refl | .(just x) | yes x≈x = refl +lemma-checkInsert-same i x m refl | .(just x) | no x≉x = contradiction A.refl x≉x lemma-checkInsert-new : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ nothing → checkInsert i x m ≡ just (insert i x m) lemma-checkInsert-new i x m p with lookupM i m lemma-checkInsert-new i x m refl | .nothing = refl -lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → x ≢ x' → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing +lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → ¬ (x ≈ x') → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing lemma-checkInsert-wrong i x m x' d p with lookupM i m 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 -vecSetoidToProp : {A : Set} {n : ℕ} {x y : Setoid.Carrier (vecIsSetoid (MaybeEq (PropEq A)) n)} → Setoid._≈_ (vecIsSetoid (MaybeEq (PropEq A)) n) x y → x ≡ y -vecSetoidToProp VecEq.[]-cong = refl -vecSetoidToProp (just refl VecEq.∷-cong p) = cong (_∷V_ _) (vecSetoidToProp p) -vecSetoidToProp (nothing VecEq.∷-cong p) = cong (_∷V_ _) (vecSetoidToProp p) - -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 : {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 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 p = cong just (vecSetoidToProp (lemma-insert-same _ i (f i) (maybeEq-from-≡ p))) -lemma-checkInsert-restrict f i is | ._ | new _ = refl -lemma-checkInsert-restrict f i is | ._ | wrong x fi≢x p = contradiction (lemma-lookupM-restrict i f is x p) fi≢x +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 | ._ | 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 lemma-lookupM-checkInsert i j x y h h' pl ph' with checkInsert j y h | insertionresult j y h -lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ = pl +lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ _ _ = pl lemma-lookupM-checkInsert i j x y h h' pl ph' | ._ | new _ with i ≟ j lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = lemma-just≢nothing pl pl' lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i≢j = begin @@ -76,11 +81,13 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i lookupM i h ≡⟨ pl ⟩ just x ∎ + where open Relation.Binary.PropositionalEquality.≡-Reasoning + lemma-lookupM-checkInsert i j x y h h' pl () | ._ | wrong _ _ _ lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert j x h ≡ just h' → lookupM i h ≡ lookupM i h' lemma-lookupM-checkInsert-other i j i≢j x h h' ph' with lookupM j h lemma-lookupM-checkInsert-other i j i≢j x h h' ph' | just y with deq x y -lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just .x | yes refl = refl -lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≢y +lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just y | yes x≈y = refl +lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≉y lemma-lookupM-checkInsert-other i j i≢j x h .(insert j x h) refl | nothing = lemma-lookupM-insert-other i j x h i≢j diff --git a/Precond.agda b/Precond.agda index e4699dc..41e3407 100644 --- a/Precond.agda +++ b/Precond.agda @@ -17,12 +17,12 @@ open Data.List.Any.Membership-≡ using (_∉_) open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_) open import Function using (flip ; _∘_) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym) +open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) import CheckInsert -open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) +open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF import Bidir |