diff options
| -rw-r--r-- | Bidir.agda | 88 |
1 files changed, 69 insertions, 19 deletions
@@ -7,11 +7,12 @@ open import Data.List using (List ; [] ; _∷_ ; map ; length) open import Data.List.Properties using (map-cong) renaming (map-compose to map-∘) open import Data.Vec using (toList ; fromList ; tabulate) renaming (lookup to lookupVec ; _∷_ to _∷V_) open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate) +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 (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_ ; _≗_) +open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; Reveal_is_ ; _≗_ ; trans) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap @@ -36,13 +37,54 @@ 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 with lookupM i (restrict f is) | inspect (lookupM i) (restrict f is) -lemma-checkInsert-restrict eq f i is | nothing | _ = refl -lemma-checkInsert-restrict eq f i is | just x | Reveal_is_.[_] prf with lemma-lookupM-restrict i f is x prf -lemma-checkInsert-restrict eq f i is | just .(f i) | Reveal_is_.[_] prf | refl with eq (f i) (f i) -lemma-checkInsert-restrict eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | yes refl = cong just (lemma-insert-same (restrict f is) i (f i) prf) -lemma-checkInsert-restrict eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | no ¬p = contradiction refl ¬p +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 @@ -57,19 +99,27 @@ lemma-1 eq f (i ∷ is′) = begin ≡⟨ lemma-checkInsert-restrict eq f i is′ ⟩ just (restrict f (i ∷ is′)) ∎ +lemma-just-nothing : {A : Set} → {a : A} → ¬ (_≡_ {_} {Maybe A} (just a) nothing) +lemma-just-nothing () + lemma-lookupM-assoc : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (is : List (Fin n)) → (x : A) → (xs : List A) → (h : FinMapMaybe n A) → assoc eq (i ∷ is) (x ∷ xs) ≡ just h → lookupM i h ≡ just x lemma-lookupM-assoc eq i is x xs h p with assoc eq is xs -lemma-lookupM-assoc eq i is x xs h () | nothing -lemma-lookupM-assoc eq i is x xs h p | just h' with lookupM i h' | inspect (lookupM i) h' -lemma-lookupM-assoc eq i is x xs .(insert i x h') refl | just h' | nothing | _ = lemma-lookupM-insert i x h' -lemma-lookupM-assoc eq i is x xs h p | just h' | just y | _ with eq x y -lemma-lookupM-assoc eq i is x xs h () | just h' | just y | _ | no ¬prf -lemma-lookupM-assoc eq i is x xs h p | just h' | just .x | Reveal_is_.[_] p' | yes refl = begin - lookupM i h - ≡⟨ cong (lookupM i) (lemma-from-just (sym p)) ⟩ - lookupM i h' - ≡⟨ p' ⟩ - just x ∎ +lemma-lookupM-assoc eq i is x xs h () | nothing +lemma-lookupM-assoc eq i is x xs h p | just h' = apply-checkInsertProof eq i x h' record + { same = λ lookupM≡justx → begin + lookupM i h + ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym p) (lemma-checkInsert-same eq i x h' lookupM≡justx))) ⟩ + lookupM i h' + ≡⟨ lookupM≡justx ⟩ + just x ∎ + ; new = λ lookupM≡nothing → begin + lookupM i h + ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym p) (lemma-checkInsert-new eq i x h' lookupM≡nothing))) ⟩ + lookupM i (insert i x h') + ≡⟨ lemma-lookupM-insert i x h' ⟩ + just x ∎ + ; wrong = λ x' x≢x' lookupM≡justx' → ⊥-elim (lemma-just-nothing (trans (sym p) (lemma-checkInsert-wrong eq i x h' x' x≢x' lookupM≡justx'))) + } lemma-2 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (is : List (Fin n)) → (v : List τ) → (h : FinMapMaybe n τ) → assoc eq is v ≡ just h → map (flip lookupM h) is ≡ map just v lemma-2 eq [] [] h p = refl |