diff options
| -rw-r--r-- | Bidir.agda | 81 | ||||
| -rw-r--r-- | CheckInsert.agda | 93 |
2 files changed, 95 insertions, 79 deletions
@@ -14,13 +14,14 @@ open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) open import Data.Empty using (⊥-elim) open import Function using (id ; _∘_ ; flip) -open import Relation.Nullary using (Dec ; yes ; no ; ¬_) +open import Relation.Nullary using (yes ; no ; ¬_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.Core using (_≡_ ; refl) open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; Reveal_is_ ; _≗_ ; trans) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap +open import CheckInsert _>>=_ : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B _>>=_ = flip (flip maybe′ nothing) @@ -28,69 +29,11 @@ _>>=_ = flip (flip maybe′ nothing) fmap : {A B : Set} → (A → B) → Maybe A → Maybe B fmap f = maybe′ (λ a → just (f a)) nothing -EqInst : Set → Set -EqInst A = (x y : A) → Dec (x ≡ y) - -checkInsert : {A : Set} {n : ℕ} → EqInst A → Fin n → A → FinMapMaybe n A → Maybe (FinMapMaybe n A) -checkInsert eq i b m with lookupM i m -checkInsert eq i b m | just c with eq b c -checkInsert eq i b m | just .b | yes refl = just m -checkInsert eq i b m | just c | no ¬p = nothing -checkInsert eq i b m | nothing = just (insert i b m) assoc : {A : Set} {n : ℕ} → EqInst A → List (Fin n) → List A → Maybe (FinMapMaybe n A) assoc _ [] [] = just empty assoc eq (i ∷ is) (b ∷ bs) = (assoc eq is bs) >>= (checkInsert eq i b) assoc _ _ _ = nothing -record checkInsertProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (P : Set) : Set where - field - same : lookupM i m ≡ just x → P - new : lookupM i m ≡ nothing → P - wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → P - -apply-checkInsertProof : {A P : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → checkInsertProof eq i x m P → P -apply-checkInsertProof eq i x m rp with lookupM i m | inspect (lookupM i) m -apply-checkInsertProof eq i x m rp | just x' | il with eq x x' -apply-checkInsertProof eq i x m rp | just .x | Reveal_is_.[_] il | yes refl = checkInsertProof.same rp il -apply-checkInsertProof eq i x m rp | just x' | Reveal_is_.[_] il | no x≢x' = checkInsertProof.wrong rp x' x≢x' il -apply-checkInsertProof eq i x m rp | nothing | Reveal_is_.[_] il = checkInsertProof.new rp il - -lemma-checkInsert-same : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → lookupM i m ≡ just x → checkInsert eq i x m ≡ just m -lemma-checkInsert-same eq i x m p with lookupM i m -lemma-checkInsert-same eq i x m refl | .(just x) with eq x x -lemma-checkInsert-same eq i x m refl | .(just x) | yes refl = refl -lemma-checkInsert-same eq i x m refl | .(just x) | no x≢x = contradiction refl x≢x - -lemma-checkInsert-new : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → lookupM i m ≡ nothing → checkInsert eq i x m ≡ just (insert i x m) -lemma-checkInsert-new eq i x m p with lookupM i m -lemma-checkInsert-new eq i x m refl | .nothing = refl - -lemma-checkInsert-wrong : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → checkInsert eq i x m ≡ nothing -lemma-checkInsert-wrong eq i x m x' d p with lookupM i m -lemma-checkInsert-wrong eq i x m x' d refl | .(just x') with eq x x' -lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | yes q = contradiction q d -lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | no ¬q = refl - -record checkInsertEqualProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (e : Maybe (FinMapMaybe n A)) : Set where - field - same : lookupM i m ≡ just x → just m ≡ e - new : lookupM i m ≡ nothing → just (insert i x m) ≡ e - wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → nothing ≡ e - -lift-checkInsertProof : {A : Set} {n : ℕ} {eq : EqInst A} {i : Fin n} {x : A} {m : FinMapMaybe n A} {e : Maybe (FinMapMaybe n A)} → checkInsertEqualProof eq i x m e → checkInsertProof eq i x m (checkInsert eq i x m ≡ e) -lift-checkInsertProof {_} {_} {eq} {i} {x} {m} o = record - { same = λ p → trans (lemma-checkInsert-same eq i x m p) (checkInsertEqualProof.same o p) - ; new = λ p → trans (lemma-checkInsert-new eq i x m p) (checkInsertEqualProof.new o p) - ; wrong = λ x' q p → trans (lemma-checkInsert-wrong eq i x m x' q p) (checkInsertEqualProof.wrong o x' q p) - } - -lemma-checkInsert-restrict : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (i : Fin n) → (is : List (Fin n)) → checkInsert eq i (f i) (restrict f is) ≡ just (restrict f (i ∷ is)) -lemma-checkInsert-restrict {τ} eq f i is = apply-checkInsertProof eq i (f i) (restrict f is) (lift-checkInsertProof record - { same = λ lookupM≡justx → cong just (lemma-insert-same (restrict f is) i (f i) lookupM≡justx) - ; new = λ lookupM≡nothing → refl - ; wrong = λ x' x≢x' lookupM≡justx' → contradiction (lemma-lookupM-restrict i f is x' lookupM≡justx') x≢x' - }) - lemma-1 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (restrict f is) lemma-1 eq f [] = refl lemma-1 eq f (i ∷ is′) = begin @@ -123,26 +66,6 @@ lemma-lookupM-assoc eq i is x xs h p | just h' = apply-checkInsertProof eq i ; wrong = λ x' x≢x' lookupM≡justx' → lemma-just≢nothing (trans (sym p) (lemma-checkInsert-wrong eq i x h' x' x≢x' lookupM≡justx')) } -lemma-lookupM-checkInsert : {A : Set} {n : ℕ} → (eq : EqInst A) → (i j : Fin n) → (x y : A) → (h h' : FinMapMaybe n A) → lookupM i h ≡ just x → checkInsert eq j y h ≡ just h' → lookupM i h' ≡ just x -lemma-lookupM-checkInsert eq i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h -lemma-lookupM-checkInsert eq i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j -lemma-lookupM-checkInsert eq i .i x y h .(insert i y h) pl refl | nothing | Reveal_is_.[_] pl' | yes refl with begin just x ≡⟨ sym pl ⟩ lookupM i h ≡⟨ pl' ⟩ nothing ∎ -... | () -lemma-lookupM-checkInsert eq i j x y h .(insert j y h) pl refl | nothing | pl' | no ¬p = begin - lookupM i (insert j y h) - ≡⟨ sym (lemma-lookupM-insert-other i j y h ¬p) ⟩ - lookupM i h - ≡⟨ pl ⟩ - just x ∎ -lemma-lookupM-checkInsert eq i j x y h h' pl ph' | just z | pl' with eq y z -lemma-lookupM-checkInsert eq i j x y h h' pl ph' | just .y | pl' | yes refl = begin - lookupM i h' - ≡⟨ cong (lookupM i) (lemma-from-just (sym ph')) ⟩ - lookupM i h - ≡⟨ pl ⟩ - just x ∎ -lemma-lookupM-checkInsert eq i j x y h h' pl () | just z | pl' | no ¬p - lemma-∉-lookupM-assoc : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (is : List (Fin n)) → (xs : List A) → (h : FinMapMaybe n A) → assoc eq is xs ≡ just h → (i ∉ is) → lookupM i h ≡ nothing lemma-∉-lookupM-assoc eq i [] [] h ph i∉is = begin lookupM i h diff --git a/CheckInsert.agda b/CheckInsert.agda new file mode 100644 index 0000000..6c168e2 --- /dev/null +++ b/CheckInsert.agda @@ -0,0 +1,93 @@ +module CheckInsert 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) +open import Data.List using (List ; [] ; _∷_) +open import Relation.Nullary using (Dec ; yes ; no ; ¬_) +open import Relation.Nullary.Negation using (contradiction) +open import Relation.Binary.Core using (_≡_ ; refl) +open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; Reveal_is_ ; trans) +open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) + +open import FinMap + +EqInst : Set → Set +EqInst A = (x y : A) → Dec (x ≡ y) + +checkInsert : {A : Set} {n : ℕ} → EqInst A → Fin n → A → FinMapMaybe n A → Maybe (FinMapMaybe n A) +checkInsert eq i b m with lookupM i m +checkInsert eq i b m | just c with eq b c +checkInsert eq i b m | just .b | yes refl = just m +checkInsert eq i b m | just c | no ¬p = nothing +checkInsert eq i b m | nothing = just (insert i b m) + +record checkInsertProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (P : Set) : Set where + field + same : lookupM i m ≡ just x → P + new : lookupM i m ≡ nothing → P + wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → P + +apply-checkInsertProof : {A P : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → checkInsertProof eq i x m P → P +apply-checkInsertProof eq i x m rp with lookupM i m | inspect (lookupM i) m +apply-checkInsertProof eq i x m rp | just x' | il with eq x x' +apply-checkInsertProof eq i x m rp | just .x | Reveal_is_.[_] il | yes refl = checkInsertProof.same rp il +apply-checkInsertProof eq i x m rp | just x' | Reveal_is_.[_] il | no x≢x' = checkInsertProof.wrong rp x' x≢x' il +apply-checkInsertProof eq i x m rp | nothing | Reveal_is_.[_] il = checkInsertProof.new rp il + +lemma-checkInsert-same : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → lookupM i m ≡ just x → checkInsert eq i x m ≡ just m +lemma-checkInsert-same eq i x m p with lookupM i m +lemma-checkInsert-same eq i x m refl | .(just x) with eq x x +lemma-checkInsert-same eq i x m refl | .(just x) | yes refl = refl +lemma-checkInsert-same eq i x m refl | .(just x) | no x≢x = contradiction refl x≢x + +lemma-checkInsert-new : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → lookupM i m ≡ nothing → checkInsert eq i x m ≡ just (insert i x m) +lemma-checkInsert-new eq i x m p with lookupM i m +lemma-checkInsert-new eq i x m refl | .nothing = refl + +lemma-checkInsert-wrong : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → checkInsert eq i x m ≡ nothing +lemma-checkInsert-wrong eq i x m x' d p with lookupM i m +lemma-checkInsert-wrong eq i x m x' d refl | .(just x') with eq x x' +lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | yes q = contradiction q d +lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | no ¬q = refl + +record checkInsertEqualProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A) (m : FinMapMaybe n A) (e : Maybe (FinMapMaybe n A)) : Set where + field + same : lookupM i m ≡ just x → just m ≡ e + new : lookupM i m ≡ nothing → just (insert i x m) ≡ e + wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → nothing ≡ e + +lift-checkInsertProof : {A : Set} {n : ℕ} {eq : EqInst A} {i : Fin n} {x : A} {m : FinMapMaybe n A} {e : Maybe (FinMapMaybe n A)} → checkInsertEqualProof eq i x m e → checkInsertProof eq i x m (checkInsert eq i x m ≡ e) +lift-checkInsertProof {_} {_} {eq} {i} {x} {m} o = record + { same = λ p → trans (lemma-checkInsert-same eq i x m p) (checkInsertEqualProof.same o p) + ; new = λ p → trans (lemma-checkInsert-new eq i x m p) (checkInsertEqualProof.new o p) + ; wrong = λ x' q p → trans (lemma-checkInsert-wrong eq i x m x' q p) (checkInsertEqualProof.wrong o x' q p) + } + +lemma-checkInsert-restrict : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (i : Fin n) → (is : List (Fin n)) → checkInsert eq i (f i) (restrict f is) ≡ just (restrict f (i ∷ is)) +lemma-checkInsert-restrict {τ} eq f i is = apply-checkInsertProof eq i (f i) (restrict f is) (lift-checkInsertProof record + { same = λ lookupM≡justx → cong just (lemma-insert-same (restrict f is) i (f i) lookupM≡justx) + ; new = λ lookupM≡nothing → refl + ; wrong = λ x' x≢x' lookupM≡justx' → contradiction (lemma-lookupM-restrict i f is x' lookupM≡justx') x≢x' + }) + +lemma-lookupM-checkInsert : {A : Set} {n : ℕ} → (eq : EqInst A) → (i j : Fin n) → (x y : A) → (h h' : FinMapMaybe n A) → lookupM i h ≡ just x → checkInsert eq j y h ≡ just h' → lookupM i h' ≡ just x +lemma-lookupM-checkInsert eq i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h +lemma-lookupM-checkInsert eq i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j +lemma-lookupM-checkInsert eq i .i x y h .(insert i y h) pl refl | nothing | Reveal_is_.[_] pl' | yes refl with begin just x ≡⟨ sym pl ⟩ lookupM i h ≡⟨ pl' ⟩ nothing ∎ +... | () +lemma-lookupM-checkInsert eq i j x y h .(insert j y h) pl refl | nothing | pl' | no ¬p = begin + lookupM i (insert j y h) + ≡⟨ sym (lemma-lookupM-insert-other i j y h ¬p) ⟩ + lookupM i h + ≡⟨ pl ⟩ + just x ∎ +lemma-lookupM-checkInsert eq i j x y h h' pl ph' | just z | pl' with eq y z +lemma-lookupM-checkInsert eq i j x y h h' pl ph' | just .y | pl' | yes refl = begin + lookupM i h' + ≡⟨ cong (lookupM i) (lemma-from-just (sym ph')) ⟩ + lookupM i h + ≡⟨ pl ⟩ + just x ∎ +lemma-lookupM-checkInsert eq i j x y h h' pl () | just z | pl' | no ¬p |