s/generate/restrict/g

The name was deemed misleading. Nothing else changed.

2 files changed, 41 insertions, 41 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 57b77db..b11ed3d 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -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 ∎