diff options
| -rw-r--r-- | Bidir.agda | 38 | ||||
| -rw-r--r-- | CheckInsert.agda | 43 |
2 files changed, 26 insertions, 55 deletions
@@ -40,21 +40,10 @@ lemma-1 f (i ∷ is′) = begin 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' = apply-checkInsertProof i x h' record - { same = λ lookupM≡justx → begin - lookupM i h - ≡⟨ cong (lookupM i) (just-injective (trans (sym p) (lemma-checkInsert-same i x h' lookupM≡justx))) ⟩ - lookupM i h' - ≡⟨ lookupM≡justx ⟩ - just x ∎ - ; new = λ lookupM≡nothing → begin - lookupM i h - ≡⟨ cong (lookupM i) (just-injective (trans (sym p) (lemma-checkInsert-new 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' → lemma-just≢nothing (trans (sym p) (lemma-checkInsert-wrong i x h' x' x≢x' lookupM≡justx')) - } +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 | ._ | insert-same pl = pl +lemma-lookupM-assoc i is x xs ._ refl | just h' | ._ | insert-new _ = lemma-lookupM-insert i x h' +lemma-lookupM-assoc i is x xs h () | just h' | ._ | insert-wrong _ _ _ lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing lemma-∉-lookupM-assoc i [] [] .empty refl i∉is = lemma-lookupM-empty i @@ -74,17 +63,14 @@ lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin n) m) → (xs : Vec Carrier 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' ] = apply-checkInsertProof i' x' h' record { - same = λ lookupM-i'-h'≡just-x' → Data.List.All._∷_ - (x' , (trans (cong (lookupM i') (just-injective (trans (sym ph) (lemma-checkInsert-same i' x' h' lookupM-i'-h'≡just-x')))) lookupM-i'-h'≡just-x')) - (lemma-assoc-domain is' xs' h (trans ph' (trans (sym (lemma-checkInsert-same i' x' h' lookupM-i'-h'≡just-x')) ph))) - ; new = λ lookupM-i'-h'≡nothing → Data.List.All._∷_ - (x' , (trans (cong (lookupM i') (just-injective (trans (sym ph) (lemma-checkInsert-new i' x' h' lookupM-i'-h'≡nothing)))) (lemma-lookupM-insert i' x' h'))) - (Data.List.All.map - (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' (proj₁ p) x' h' h (proj₂ p) ph) - (lemma-assoc-domain is' xs' h' ph')) - ; wrong = λ x'' x'≢x'' lookupM-i'-h'≡just-x'' → lemma-just≢nothing (trans (sym ph) (lemma-checkInsert-wrong i' x' h' x'' x'≢x'' lookupM-i'-h'≡just-x'')) - } +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' ] | ._ | _ | insert-same pl = All._∷_ (x' , pl) (lemma-assoc-domain is' xs' h ph') +lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ._ refl | just h' | [ ph' ] | ._ | [ cI≡ ] | insert-new _ = All._∷_ + (x' , lemma-lookupM-insert i' x' h') + (Data.List.All.map + (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' (proj₁ p) x' h' (insert i' x' h') (proj₂ p) cI≡) + (lemma-assoc-domain is' xs' h' ph')) +lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h () | just h' | [ ph' ] | ._ | _ | insert-wrong _ _ _ lemma-map-lookupM-insert : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (h : FinMapMaybe n Carrier) → i ∉ (toList is) → map (flip lookupM (insert i x h)) is ≡ map (flip lookupM h) is lemma-map-lookupM-insert i [] x h i∉is = refl diff --git a/CheckInsert.agda b/CheckInsert.agda index 4083720..17228f2 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -22,18 +22,17 @@ checkInsert i b m with lookupM i m ... | yes b≡c = just m ... | no b≢c = nothing -record checkInsertProof {n : ℕ} (i : Fin n) (x : Carrier) (m : FinMapMaybe n Carrier) (P : Set) : Set where - field - same : lookupM i m ≡ just x → P - new : lookupM i m ≡ nothing → P - wrong : (x' : Carrier) → x ≢ x' → lookupM i m ≡ just x' → P +data InsertionResult {n : ℕ} (i : Fin n) (x : Carrier) (h : FinMapMaybe n Carrier) : Maybe (FinMapMaybe n Carrier) → Set where + insert-same : lookupM i h ≡ just x → InsertionResult i x h (just h) + insert-new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h)) + insert-wrong : (x' : Carrier) → x ≢ x' → lookupM i h ≡ just x' → InsertionResult i x h nothing -apply-checkInsertProof : {P : Set} {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → checkInsertProof i x m P → P -apply-checkInsertProof i x m rp with lookupM i m | inspect (lookupM i) m -apply-checkInsertProof i x m rp | just x' | il with deq x x' -apply-checkInsertProof i x m rp | just .x | [ il ] | yes refl = checkInsertProof.same rp il -apply-checkInsertProof i x m rp | just x' | [ il ] | no x≢x' = checkInsertProof.wrong rp x' x≢x' il -apply-checkInsertProof i x m rp | nothing | [ il ] = checkInsertProof.new rp il +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 = insert-same il +insertionresult i x h | just x' | [ il ] | no x≢x' = insert-wrong x' x≢x' il +insertionresult i x h | nothing | [ il ] = insert-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 @@ -51,25 +50,11 @@ 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 -record checkInsertEqualProof {n : ℕ} (i : Fin n) (x : Carrier) (m : FinMapMaybe n Carrier) (e : Maybe (FinMapMaybe n Carrier)) : 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' : Carrier) → x ≢ x' → lookupM i m ≡ just x' → nothing ≡ e - -lift-checkInsertProof : {n : ℕ} {i : Fin n} {x : Carrier} {m : FinMapMaybe n Carrier} {e : Maybe (FinMapMaybe n Carrier)} → checkInsertEqualProof i x m e → checkInsertProof i x m (checkInsert i x m ≡ e) -lift-checkInsertProof {_} {i} {x} {m} o = record - { same = λ p → trans (lemma-checkInsert-same i x m p) (checkInsertEqualProof.same o p) - ; new = λ p → trans (lemma-checkInsert-new i x m p) (checkInsertEqualProof.new o p) - ; wrong = λ x' q p → trans (lemma-checkInsert-wrong i x m x' q p) (checkInsertEqualProof.wrong o x' q 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 f i is = apply-checkInsertProof 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-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 | ._ | insert-same p = cong just (lemma-insert-same _ i (f i) p) +lemma-checkInsert-restrict f i is | ._ | insert-new _ = refl +lemma-checkInsert-restrict f i is | ._ | insert-wrong x fi≢x p = contradiction (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 lookupM j h | inspect (lookupM j) h |