make more parameters implicit

All of these changes were applied to functions of type

... -> (x : ...) -> ... == x -> ...

where x could be preceded by just making the x implicit, because it can
be uniquely deduced from the equality proof.

4 files changed, 56 insertions, 56 deletions

diff --git a/Bidir.agda b/Bidir.agda
index edf9e98..067b9a5 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -61,39 +61,39 @@ lemma-1 f (i ∷ is′) = begin
   just (restrict f (i ∷ is′)) ∎
   where open ≡-Reasoning
 
-lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x
-lemma-lookupM-checkInserted i x h h' p with checkInsert i x h | insertionresult i x h
-lemma-lookupM-checkInserted i x h .h refl | ._ | same x' x≈x' pl = begin
+lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x
+lemma-lookupM-checkInserted i x h p with checkInsert i x h | insertionresult i x h
+lemma-lookupM-checkInserted i x h refl | ._ | same x' x≈x' pl = begin
   lookupM i h
     ≡⟨ pl ⟩
   just x'
     ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩
   just x ∎
   where open EqR (MaybeSetoid A.setoid)
-lemma-lookupM-checkInserted i x h ._ refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lemma-lookupM-insert i x h)
-lemma-lookupM-checkInserted i x h h' () | ._ | wrong _ _ _
+lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lemma-lookupM-insert i x h)
+lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _
 
 _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set
 _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is)
 
-lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is xs ≡ just h → is in-domain-of h
-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' ] 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' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' h ph')
-lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ._ refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
+lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → is in-domain-of h
+lemma-assoc-domain []         []         ph = Data.List.All.[]
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs'
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ]
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') 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') refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph')
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ cI≡ ] | 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' ] | ._ | _ | wrong _ _ _
+    (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡)
+    (lemma-assoc-domain is' xs' ph'))
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _
 
-lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → (h' : FinMapMaybe m Carrier) → checkInsert i x h' ≡ just h → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h' → map (flip lookupM h) js ≡ map (flip lookupM h') js
-lemma-map-lookupM-assoc i x h h' ph [] pj = refl
-lemma-map-lookupM-assoc i x h h' ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = cong₂ _∷_
-  (trans (lemma-lookupM-checkInsert j i x' x h' h pl ph) (sym pl))
-  (lemma-map-lookupM-assoc i x h h' ph js pj)
+lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js
+lemma-map-lookupM-assoc i x h ph [] pj = refl
+lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = cong₂ _∷_
+  (trans (lemma-lookupM-checkInsert j i h pl x ph) (sym pl))
+  (lemma-map-lookupM-assoc i x h ph js pj)
 
 lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → VecISetoid (MaybeSetoid A.setoid) at _ ∋ map (flip lookupM h) is ≈ map just v
 lemma-2 []       []       h p = ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))
@@ -101,9 +101,9 @@ lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs
 lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _
 lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
   lookupM i h ∷ map (flip lookupM h) is
-    ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' h p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩
+    ≈⟨ VecEq._∷-cong_ (lemma-lookupM-checkInserted i x h' p) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩
   just x ∷ map (flip lookupM h) is
-    ≡⟨  cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h h' p is (lemma-assoc-domain is xs h' ir)) ⟩
+    ≡⟨  cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h' p is (lemma-assoc-domain is xs ir)) ⟩
   just x ∷ map (flip lookupM h') is
     ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩
   just x ∷ map just xs ∎
@@ -281,7 +281,7 @@ theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = refl , (begin⟨ VecISetoid
   content (fmapV (flip lookupM (h↦h′ h)) (get t))
     ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
   map (flip lookupM (h↦h′ h)) (content (get t))
-    ≡⟨ lemma-union-not-used h (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))) (content (get t)) (lemma-assoc-domain (content (get t)) (content v) h ph) ⟩
+    ≡⟨ lemma-union-not-used h (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))) (content (get t)) (lemma-assoc-domain (content (get t)) (content v) ph) ⟩
   map (flip lookupM h) (content (get t))
     ≈⟨ lemma-2 (content (get t)) (content v) h ph ⟩
   map just (content v)
diff --git a/CheckInsert.agda b/CheckInsert.agda
index 62ec6c8..86d7144 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -58,16 +58,16 @@ lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl
 
 lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is))
 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 | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (f i) (trans p (cong just (sym (lemma-lookupM-restrict i f is x p)))))
+lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (trans p (cong just (sym (lemma-lookupM-restrict i f is p)))))
 lemma-checkInsert-restrict f i is | ._ | new _ = refl
-lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is x p)) fi≉x
+lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is 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 checkInsert j y h | insertionresult j y h
-lemma-lookupM-checkInsert i j x y h .h pl refl | ._ | same _ _ _ = pl
-lemma-lookupM-checkInsert i j x y h h' pl ph'  | ._ | new _ with i ≟ j
-lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ())
-lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i≢j = begin
+lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (h : FinMapMaybe n Carrier) → {x : Carrier} → lookupM i h ≡ just x → (y : Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x
+lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h
+lemma-lookupM-checkInsert i j h pl y refl | ._ | same _ _ _ = pl
+lemma-lookupM-checkInsert i j h pl y ph'  | ._ | new _ with i ≟ j
+lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ())
+lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin
   lookupM i (insert j y h)
     ≡⟨ lemma-lookupM-insert-other i j y h i≢j ⟩
   lookupM i h
@@ -75,11 +75,11 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i�
   just x ∎
   where open Relation.Binary.PropositionalEquality.≡-Reasoning
 
-lemma-lookupM-checkInsert i j x y h h' pl () | ._ | wrong _ _ _
+lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _
 
-lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h
-lemma-lookupM-checkInsert-other i j i≢j x h h' ph' with lookupM j h
-lemma-lookupM-checkInsert-other i j i≢j x h h' ph' | just y with deq x y
-lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just y | yes x≈y = refl
-lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≉y
-lemma-lookupM-checkInsert-other i j i≢j x h .(insert j x h) refl | nothing = lemma-lookupM-insert-other i j x h i≢j
+lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h
+lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h
+lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y
+lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl
+lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y
+lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lemma-lookupM-insert-other i j x h i≢j
diff --git a/FinMap.agda b/FinMap.agda
index ccd522e..d1ffa24 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -56,10 +56,10 @@ delete i m = m [ i ]≔ nothing
 delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A
 delete-many = flip (foldr (const _) delete)
 
-lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → (a : A) → lookupM f m ≡ just a → m ≡ insert f a m
-lemma-insert-same         []       ()      a p
-lemma-insert-same {suc n} (x ∷ xs) zero    a p = cong (flip _∷_ xs) p
-lemma-insert-same         (x ∷ xs) (suc i) a p = cong (_∷_ x) (lemma-insert-same xs i a p)
+lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → {a : A} → lookupM f m ≡ just a → m ≡ insert f a m
+lemma-insert-same         []       ()      p
+lemma-insert-same {suc n} (x ∷ xs) zero    p = cong (flip _∷_ xs) p
+lemma-insert-same         (x ∷ xs) (suc i) p = cong (_∷_ x) (lemma-insert-same xs i p)
 
 lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing
 lemma-lookupM-empty zero    = refl
@@ -75,16 +75,16 @@ 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 (p ∘ cong suc)
 
-lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a
-lemma-lookupM-restrict i f []        a p = contradiction (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 = just-injective (begin
+lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a
+lemma-lookupM-restrict i f []            p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ())
+lemma-lookupM-restrict i f (i' ∷ is)     p with i ≟ i'
+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))
      ≡⟨ p ⟩
    just a ∎)
-lemma-lookupM-restrict i f (i' ∷ is) a p | no i≢i' = lemma-lookupM-restrict i f is a (begin
+lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin
   lookupM i (restrict f is)
     ≡⟨ sym (lemma-lookupM-insert-other i i' (f i') (restrict f is) i≢i') ⟩
   lookupM i (insert i' (f i') (restrict f is))
diff --git a/Precond.agda b/Precond.agda
index 31ac04b..ffbe0e7 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -88,21 +88,21 @@ assoc-enough′ G {i} s v (h , p) = _ , (begin
         g  = fromFunc (denumerate SourceShapeT s)
         g′ = delete-many (Shaped.content ViewShapeT (get s′)) g
         t  = enumerate SourceShapeT (|gl₁| i)
-        wp = lemma-union-delete-fromFunc (lemma-assoc-domain (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) h p)
+        wp = lemma-union-delete-fromFunc (lemma-assoc-domain (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) p)
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []
   different-∷  : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs)
 
-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
-lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc is' xs' | inspect (assoc is') xs'
-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' ] = begin
+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 []         []         refl i∉is = lemma-lookupM-empty i
+lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') ph i∉is with assoc is' xs' | inspect (assoc is') xs'
+lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') () i∉is | nothing | [ ph' ]
+lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [ ph' ] = begin
   lookupM i h
-    ≡⟨ lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' h ph ⟩
+    ≡⟨ lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' ph ⟩
   lookupM i h'
-    ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩
+    ≡⟨ lemma-∉-lookupM-assoc i is' xs' ph' (i∉is ∘ there) ⟩
   nothing ∎
 
 different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → All-different (toList u) → ∃ λ h → assoc u v ≡ just h
@@ -114,5 +114,5 @@ different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) | h , p' =
   (assoc us vs >>= checkInsert u v)
     ≡⟨ cong (flip _>>=_ (checkInsert u v)) p' ⟩
   checkInsert u v h
-    ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs h p' u∉us) ⟩
+    ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs p' u∉us) ⟩
   just (insert u v h) ∎)