diff options
| -rw-r--r-- | Bidir.agda | 18 | ||||
| -rw-r--r-- | CheckInsert.agda | 2 | ||||
| -rw-r--r-- | FinMap.agda | 6 |
3 files changed, 13 insertions, 13 deletions
@@ -48,13 +48,13 @@ 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) (lemma-from-just (trans (sym p) (lemma-checkInsert-same i x h' lookupM≡justx))) ⟩ + ≡⟨ 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) (lemma-from-just (trans (sym p) (lemma-checkInsert-new i x h' lookupM≡nothing))) ⟩ + ≡⟨ 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 ∎ @@ -64,7 +64,7 @@ lemma-lookupM-assoc i is x xs h p | just h' = apply-checkInsertProof i x h' r 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 [] [] h ph i∉is = begin lookupM i h - ≡⟨ cong (lookupM i) (sym (lemma-from-just ph)) ⟩ + ≡⟨ cong (lookupM i) (sym (just-injective ph)) ⟩ lookupM i empty ≡⟨ lemma-lookupM-empty i ⟩ nothing ∎ @@ -73,13 +73,13 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | [ ph lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | [ ph' ] = apply-checkInsertProof i' x' h' record { same = λ lookupM-i'-h'≡just-x' → begin lookupM i h - ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym ph) (lemma-checkInsert-same i' x' h' lookupM-i'-h'≡just-x'))) ⟩ + ≡⟨ cong (lookupM i) (just-injective (trans (sym ph) (lemma-checkInsert-same i' x' h' lookupM-i'-h'≡just-x'))) ⟩ lookupM i h' ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩ nothing ∎ ; new = λ lookupM-i'-h'≡nothing → begin lookupM i h - ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym ph) (lemma-checkInsert-new i' x' h' lookupM-i'-h'≡nothing))) ⟩ + ≡⟨ cong (lookupM i) (just-injective (trans (sym ph) (lemma-checkInsert-new i' x' h' lookupM-i'-h'≡nothing))) ⟩ lookupM i (insert i' x' h') ≡⟨ sym (lemma-lookupM-insert-other i i' x' h' (i∉is ∘ here)) ⟩ lookupM i h' @@ -97,10 +97,10 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph with assoc is' xs' | inspect ( 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') (lemma-from-just (trans (sym ph) (lemma-checkInsert-same i' x' h' lookupM-i'-h'≡just-x')))) lookupM-i'-h'≡just-x')) + (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') (lemma-from-just (trans (sym ph) (lemma-checkInsert-new i' x' h' lookupM-i'-h'≡nothing)))) (lemma-lookupM-insert i' x' h'))) + (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')) @@ -126,7 +126,7 @@ lemma-map-lookupM-assoc i (i' ∷ is') x (x' ∷ xs') h .h ph' refl | yes p | (. lemma-map-lookupM-assoc i (i' ∷ is') x (x' ∷ xs') h h' ph' () | yes p | (x'' , refl) | .(just x'') | no ¬p lemma-map-lookupM-assoc i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | no ¬p rewrite lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h' ph' ¬p = begin map (flip lookupM h) (i' ∷ is') - ≡⟨ map-cong (λ i'' → cong (lookupM i'') (lemma-from-just (sym ph))) (i' ∷ is') ⟩ + ≡⟨ map-cong (λ i'' → cong (lookupM i'') (just-injective (sym ph))) (i' ∷ is') ⟩ map (flip lookupM (insert i x h')) (i' ∷ is') ≡⟨ lemma-map-lookupM-insert i (i' ∷ is') x h' ¬p (lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h' ph') ⟩ map (flip lookupM h') (i' ∷ is') ∎ @@ -225,7 +225,7 @@ theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (v theorem-2 get v s u p with lemma-fmap-just (assoc (get (enumerate s)) v) (proj₂ (lemma-fmap-just (fmap (flip union (fromFunc (denumerate s))) (assoc (get (enumerate s)) v)) p)) theorem-2 get v s u p | h , ph = begin get u - ≡⟨ lemma-from-just (begin + ≡⟨ just-injective (begin just (get u) ≡⟨ refl ⟩ fmap get (just u) diff --git a/CheckInsert.agda b/CheckInsert.agda index 01f1302..6b5473a 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -84,7 +84,7 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no lemma-lookupM-checkInsert i j x y h h' pl ph' | just z | pl' with deq y z lemma-lookupM-checkInsert 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')) ⟩ + ≡⟨ cong (lookupM i) (just-injective (sym ph')) ⟩ lookupM i h ≡⟨ pl ⟩ just x ∎ diff --git a/FinMap.agda b/FinMap.agda index 4fc3e18..c085b24 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -68,13 +68,13 @@ lemma-lookupM-insert-other zero (suc j) a (x ∷ xs) p = refl lemma-lookupM-insert-other (suc i) zero a (x ∷ xs) p = refl lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (contraposition (cong suc) p) -lemma-from-just : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y -lemma-from-just refl = refl +just-injective : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y +just-injective refl = refl lemma-lookupM-restrict : {A : Set} {n : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : List (Fin n)) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a lemma-lookupM-restrict i f [] a p = lemma-just≢nothing (trans (sym p) (lemma-lookupM-empty i)) lemma-lookupM-restrict i f (i' ∷ is) a p with i ≟ i' -lemma-lookupM-restrict i f (.i ∷ is) a p | yes refl = lemma-from-just (begin +lemma-lookupM-restrict i f (.i ∷ is) a p | yes refl = just-injective (begin just (f i) ≡⟨ sym (lemma-lookupM-insert i (f i) (restrict f is)) ⟩ lookupM i (insert i (f i) (restrict f is)) |