diff options
| -rw-r--r-- | Bidir.agda | 32 | ||||
| -rw-r--r-- | FinMap.agda | 50 |
2 files changed, 41 insertions, 41 deletions
@@ -36,26 +36,26 @@ assoc _ [] [] = just empty assoc eq (i ∷ is) (b ∷ bs) = (assoc eq is bs) >>= (checkInsert eq i b) assoc _ _ _ = nothing -lemma-checkInsert-generate : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (i : Fin n) → (is : List (Fin n)) → checkInsert eq i (f i) (generate f is) ≡ just (generate f (i ∷ is)) -lemma-checkInsert-generate eq f i is with lookupM i (generate f is) | inspect (lookupM i) (generate f is) -lemma-checkInsert-generate eq f i is | nothing | _ = refl -lemma-checkInsert-generate eq f i is | just x | Reveal_is_.[_] prf with lemma-lookupM-generate i f is x prf -lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl with eq (f i) (f i) -lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | yes refl = cong just (lemma-insert-same (generate f is) i (f i) prf) -lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] prf | refl | no ¬p = contradiction refl ¬p - -lemma-1 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (generate f is) +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-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 (assoc eq (i ∷ is′) (map f (i ∷ is′))) ≡⟨ refl ⟩ (assoc eq is′ (map f is′) >>= checkInsert eq i (f i)) ≡⟨ cong (λ m → m >>= checkInsert eq i (f i)) (lemma-1 eq f is′) ⟩ - (just (generate f is′) >>= (checkInsert eq i (f i))) + (just (restrict f is′) >>= (checkInsert eq i (f i))) ≡⟨ refl ⟩ - (checkInsert eq i (f i) (generate f is′)) - ≡⟨ lemma-checkInsert-generate eq f i is′ ⟩ - just (generate f (i ∷ is′)) ∎ + (checkInsert eq i (f i) (restrict f is′)) + ≡⟨ lemma-checkInsert-restrict eq f i is′ ⟩ + just (restrict f (i ∷ is′)) ∎ 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 @@ -140,10 +140,10 @@ theorem-1 get eq s = begin ≡⟨ refl ⟩ fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (denumerate s))) (assoc eq (get (enumerate s)) (map (denumerate s) (get (enumerate s))))) ≡⟨ cong (fmap (flip map (enumerate s) ∘ flip lookup) ∘ fmap (flip union (fromFunc (denumerate s)))) (lemma-1 eq (denumerate s) (get (enumerate s))) ⟩ - fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (flip lookupVec (fromList s)))) (just (generate (denumerate s) (get (enumerate s))))) + fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (flip lookupVec (fromList s)))) (just (restrict (denumerate s) (get (enumerate s))))) ≡⟨ refl ⟩ - just ((flip map (enumerate s) ∘ flip lookup) (union (generate (denumerate s) (get (enumerate s))) (fromFunc (denumerate s)))) - ≡⟨ cong just (cong (flip map (enumerate s) ∘ flip lookup) (lemma-union-generate (denumerate s) (get (enumerate s)))) ⟩ + just ((flip map (enumerate s) ∘ flip lookup) (union (restrict (denumerate s) (get (enumerate s))) (fromFunc (denumerate s)))) + ≡⟨ cong just (cong (flip map (enumerate s) ∘ flip lookup) (lemma-union-restrict (denumerate s) (get (enumerate s)))) ⟩ just ((flip map (enumerate s) ∘ flip lookup) (fromFunc (denumerate s))) ≡⟨ refl ⟩ just (map (flip lookup (fromFunc (denumerate s))) (enumerate s)) diff --git a/FinMap.agda b/FinMap.agda index ef444ae..376adff 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -43,8 +43,8 @@ fromFunc = tabulate union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMap n A → FinMap n A union m1 m2 = tabulate (λ f → maybe′ id (lookup f m2) (lookupM f m1)) -generate : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A -generate f is = fromAscList (zip is (map f is)) +restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A +restrict f is = fromAscList (zip is (map f is)) lemma-insert-same : {τ : Set} {n : ℕ} → (m : FinMapMaybe n τ) → (f : Fin n) → (a : τ) → lookupM f m ≡ just a → m ≡ insert f a m @@ -69,31 +69,31 @@ lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert lemma-from-just : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y lemma-from-just refl = refl -lemma-lookupM-generate : {A : Set} {n : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : List (Fin n)) → (a : A) → lookupM i (generate f is) ≡ just a → f i ≡ a -lemma-lookupM-generate {A} i f [] a p with begin +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 {A} i f [] a p with begin just a ≡⟨ sym p ⟩ - lookupM i (generate f []) + lookupM i (restrict f []) ≡⟨ refl ⟩ lookupM i empty ≡⟨ lemma-lookupM-empty i ⟩ nothing ∎ -lemma-lookupM-generate i f [] a p | () -lemma-lookupM-generate i f (i' ∷ is) a p with i ≟ i' -lemma-lookupM-generate i f (.i ∷ is) a p | yes refl = lemma-from-just (begin +lemma-lookupM-restrict i f [] a p | () +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 just (f i) - ≡⟨ sym (lemma-lookupM-insert i (f i) (generate f is)) ⟩ - lookupM i (insert i (f i) (generate f is)) + ≡⟨ sym (lemma-lookupM-insert i (f i) (restrict f is)) ⟩ + lookupM i (insert i (f i) (restrict f is)) ≡⟨ refl ⟩ - lookupM i (generate f (i ∷ is)) + lookupM i (restrict f (i ∷ is)) ≡⟨ p ⟩ just a ∎) -lemma-lookupM-generate i f (i' ∷ is) a p | no ¬p2 = lemma-lookupM-generate i f is a (begin - lookupM i (generate f is) - ≡⟨ lemma-lookupM-insert-other i i' (f i') (generate f is) ¬p2 ⟩ - lookupM i (insert i' (f i') (generate f is)) +lemma-lookupM-restrict i f (i' ∷ is) a p | no ¬p2 = lemma-lookupM-restrict i f is a (begin + lookupM i (restrict f is) + ≡⟨ lemma-lookupM-insert-other i i' (f i') (restrict f is) ¬p2 ⟩ + lookupM i (insert i' (f i') (restrict f is)) ≡⟨ refl ⟩ - lookupM i (generate f (i' ∷ is)) + lookupM i (restrict f (i' ∷ is)) ≡⟨ p ⟩ just a ∎) @@ -106,14 +106,14 @@ lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = begin ≡⟨ cong (Vec._∷_ (g zero)) (lemma-tabulate-∘ (f≗g ∘ suc)) ⟩ g zero ∷ tabulate (g ∘ suc) ∎ -lemma-union-generate : {n : ℕ} {A : Set} → (f : Fin n → A) → (is : List (Fin n)) → union (generate f is) (fromFunc f) ≡ fromFunc f -lemma-union-generate f is = begin - union (generate f is) (fromFunc f) +lemma-union-restrict : {n : ℕ} {A : Set} → (f : Fin n → A) → (is : List (Fin n)) → union (restrict f is) (fromFunc f) ≡ fromFunc f +lemma-union-restrict f is = begin + union (restrict f is) (fromFunc f) ≡⟨ refl ⟩ - tabulate (λ j → maybe′ id (lookup j (fromFunc f)) (lookupM j (generate f is))) + tabulate (λ j → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is))) ≡⟨ lemma-tabulate-∘ (lemma-inner f is) ⟩ tabulate f ∎ - where lemma-inner : {n : ℕ} {A : Set} (f : Fin n → A) → (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (generate f is)) ≡ f j + where lemma-inner : {n : ℕ} {A : Set} (f : Fin n → A) → (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡ f j lemma-inner f [] j = begin maybe′ id (lookup j (fromFunc f)) (lookupM j empty) ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-empty j) ⟩ @@ -123,10 +123,10 @@ lemma-union-generate f is = begin ≡⟨ lookup∘tabulate f j ⟩ f j ∎ lemma-inner f (i ∷ is) j with i ≟ j - lemma-inner f (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-insert j (f j) (generate f is)) + lemma-inner f (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-insert j (f j) (restrict f is)) lemma-inner f (i ∷ is) j | no i≢j = begin - maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (generate f is))) - ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (generate f is) (i≢j ∘ sym) )) ⟩ - maybe′ id (lookup j (fromFunc f)) (lookupM j (generate f is)) + maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (restrict f is))) + ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) (i≢j ∘ sym) )) ⟩ + maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡⟨ lemma-inner f is j ⟩ f j ∎ |